Difference between revisions of "Output/Input"

From HaskellWiki
Jump to: navigation, search
m (Reference replaced)
m
 
(13 intermediate revisions by the same user not shown)
Line 1: Line 1:
[[Category:Theoretical foundations]]
+
<div style="border-left:1px solid lightgray; padding: 1em" alt="blockquote">
 +
There is a world of difference between the value <code>echoML</code> which has no side effects when evaluated, and the computation <code>echoML ()</code>, which does.
  
=== <u>Clearing away the smoke and mirrors</u> ===
+
<tt>[https://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.91.3579&rep=rep1&type=pdf How to Declare an Imperative], Philip Wadler (page 25 of 33).</tt>
 +
</div>
  
<div style="border-left:1px solid lightgray; padding: 1em" alt="blockquote">
+
Of course, that assumes everything in the program's <i>“world”</i> required by <code>echoML</code> actually <b>works as intended</b>: reality isn't always so obliging! To then define Haskell's I/O type as:
The implementation in GHC uses the following one:
 
  
 +
<div style="border-left:1px solid lightgray; padding: 1em" alt="blockquote">                                                                         
 
<haskell>
 
<haskell>
 
type IO a  =  World -> (a, World)
 
type IO a  =  World -> (a, World)
 
</haskell>
 
</haskell>
  
An <code>IO</code> computation is a function that (logically) takes the state of the world, and returns a modified world as well as the return value. Of course, GHC does not actually pass the world around; instead, it passes a dummy “token,” to ensure proper sequencing of actions in the presence of lazy evaluation, and performs input and output as actual side effects!
+
[where an] <code>IO</code> computation is a function that (logically) takes the state of the world, and returns a modified world as well as the return value.
  
 
<tt>[https://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.168.4008&rep=rep1&type=pdf A History of Haskell: Being Lazy With Class], Paul Hudak, John Hughes, Simon Peyton Jones and Philip Wadler.</tt>
 
<tt>[https://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.168.4008&rep=rep1&type=pdf A History of Haskell: Being Lazy With Class], Paul Hudak, John Hughes, Simon Peyton Jones and Philip Wadler.</tt>
 
</div>
 
</div>
  
...so what starts out as an I/O action of type:
+
...seems rather optimistic.
 +
<sup> </sup>
 +
 
 +
----
 +
=== <u>The determining of </u><code>IO</code> ===
  
<haskell>
+
Since reality isn't always so deterministic in behaviour, perhaps the study of <i>nondeterminism</i> can provide a more plausible implementation:
World -> (a, World)
+
 
</haskell>
+
<div style="border-left:1px solid lightgray; padding: 1em" alt="blockquote">
 +
We propose to solve this problem [existing constructs for nondeterminism not being compatible with the mathematical foundations of functional programming] by placing the nondeterminism in pseudo-data. A program is passed an infinite tree of two-valued <tt>decisions</tt>, along with its input. These <tt>decisions</tt> may be fixed at runtime, thereby permitting nondeterminism. Once fixed, a <tt>decision</tt> remains unchanged so equivalent expression must always have the same value.
 +
 
 +
<tt>[https://academic.oup.com/comjnl/article-pdf/31/3/243/1157325/310243.pdf Nondeterminism with Referential Transparency in Functional Programming Languages], F. Warren Burton (front page).</tt>
 +
</div>
 +
 
 +
There's more:
 +
 
 +
<div style="border-left:1px solid lightgray; padding: 1em" alt="blockquote">
 +
The approach generalizes so that a program can make use of other run-time information such as the current time or current amount of available storage.
 +
</div>
  
is changed by GHC to approximately:
+
Using this <i>pseudo-data</i> approach:
  
 
<haskell>
 
<haskell>
() -> (a, ())
+
-- abstract; single-use I/O-access mediator
</haskell>
+
data Exterior
 +
getchar :: Exterior -> Char
 +
putchar :: Char -> Exterior -> ()
  
As the returned unit-value <code>()</code> contains no useful information, that type can be simplified further:
+
-- from section 2 of Burton's paper
 +
data Tree a = Node { contents :: a,
 +
                    left    :: Tree a,
 +
                    right    :: Tree a }
  
<haskell>
+
-- utility definitions
() -> a
+
type OI  =  Tree Exterior
</haskell>
 
  
<sub>Why <i>"approximately"</i>? Because <i>"logically"</i> a function in Haskell has no observable effects.</sub>
+
main'    :: OI -> ()
 +
main'    =  ...
  
----
+
getChar' :: OI -> Char
=== <u>Previously seen</u> ===
+
getChar' = getchar . contents
  
The type <code>() -> a</code>  (or variations of it) have appeared elsewhere - examples include:
+
putChar' :: Char -> OI -> ()
 +
putChar' c = putchar c . contents
  
* page 2 of 13 in [https://fi.ort.edu.uy/innovaportal/file/20124/1/22-landin_correspondence-between-algol-60-and-churchs-lambda-notation.pdf A Correspondence Between ALGOL 60 and Church's Lambda-Notation: Part I] by Peter Landin:
+
part    :: OI -> (OI, OI)
:{|
+
parts    :: OI -> [OI]
|<div style="border-left:1px solid lightgray; padding: 1em" alt="blockquote">
 
  
The use of <code>λ</code>, and in particular (to avoid an irrelevant bound variable) of <code>λ()</code> , to delay and possibly avoid evaluation is exploited repeatedly in our model of ALGOL 60. A function that requires an argument-list of length zero is called a ''none-adic'' function.
+
part t  =  (left t, right t)
</div>
+
parts t  =  let !(t1, t2) = part t in
<sup> </sup>
+
            t1 : parts t2
<haskell>
 
(\ () -> …) :: () -> a
 
 
</haskell>
 
</haskell>
|}
 
  
* page 148 of 168 in [https://web.archive.org/web/20021107080915/https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-285.pdf Functional programming and Input/Output] by Andrew Gordon:
+
To avoid the visible use of trees, the single-use property can instead be applied directly to <code>OI</code> values. This permits an abstract definition of the <code>OI</code> type:
:{|
+
 
|<div style="border-left:1px solid lightgray; padding: 1em" alt="blockquote">
 
<pre>
 
abstype 'a Job = JOB of unit -> 'a
 
</pre>
 
</div>
 
<sup> </sup>
 
 
<haskell>
 
<haskell>
data Job a = JOB (() -> a)
+
data OI
 +
partOI  :: OI -> (OI, OI)
 +
getChar :: OI -> Char
 +
putChar :: Char -> OI -> ()
 
</haskell>
 
</haskell>
|}
 
  
* page 3 of [https://www.cs.bham.ac.uk/~udr/papers/assign.pdf Assignments for Applicative Languages] by Vipin Swarup, Uday S. Reddy and Evan Ireland:
+
The choice to use (theoretically) infinite structured values (binary trees or otherwise) is then an implementation matter.
:{|
 
|<div style="border-left:1px solid lightgray; padding: 1em" alt="blockquote">
 
A value of type <code>Obs 𝜏</code> is called an ''observer''.  Such a value observes (i.e. views or inspects) a state and returns a value of type <code>𝜏</code>. [...] An observer type <code>Obs 𝜏</code> may be viewed as an implicit function space from the set of states to the type <code>𝜏</code>.
 
</div>
 
 
<sup> </sup>
 
<sup> </sup>
<haskell>
 
type Obs tau = State -> tau
 
</haskell>
 
|}
 
  
* [https://image.slidesharecdn.com/lazyio-120422092926-phpapp01/95/lazy-io-15-728.jpg page 15] of ''Non-Imperative Functional Programming'' by Nobuo Yamashita:
+
----
 +
=== <u>Other interfaces</u> ===
 +
 
 +
In addition to the [[Monad|current]] one:
  
:{|
 
 
<haskell>
 
<haskell>
type a :-> b = OI a -> b
+
type M a   = OI -> a
</haskell>
 
|}
 
  
* [http://h2.jaguarpaw.co.uk/posts/mtl-style-for-free MTL style for free] by Tom Ellis:
+
unit      :: a -> M a
 +
unit x    =  \ u -> let !_ = partOI u in x
  
:{|
+
bind      :: M a -> (a -> M b) -> M b
<haskell>
+
bind m k  = \ u -> let !(u1, u2) = partOI u in
data Time_ a = GetCurrentTime (UTCTime -> a)
+
                    let !x = m u1 in
</haskell>
+
                    let !y = k x u2 in
|}
+
                    y
  
* [http://h2.jaguarpaw.co.uk/posts/impure-lazy-language An impure lazy programming language], also by Tom Ellis:
+
getcharM  :: M Char
 +
getcharM  =  getChar
  
:{|
+
putcharM  :: Char -> M ()
<haskell>
+
putcharM  = putChar
data IO a = IO (() -> a)
 
 
</haskell>
 
</haskell>
|}
 
  
* page 2 of [https://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.128.9269&rep=rep1&type=pdf Unique Identifiers in Pure Functional Languages] by Péter Diviánszky:
+
the <code>OI</code> interface can be used to implement other models of I/O:
:{|
 
|<div style="border-left:1px solid lightgray; padding: 1em" alt="blockquote">
 
[...] The type <code>Id</code> can be hidden by the synonym data type
 
<pre>
 
:: Create a  :==  Id -> a
 
</pre>
 
</div>
 
<sup> </sup>
 
<haskell>
 
type Create a = Id -> a
 
</haskell>
 
|}
 
  
* page 7 of [https://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.701.930&rep=rep1&type=pdf Functional Reactive Animation] by Conal Elliott and Paul Hudak:
+
* [[Comonad|comonad]]:
:{|
 
|<div style="border-left:1px solid lightgray; padding: 1em" alt="blockquote">
 
An early implementation of Fran represented behaviors as implied in the formal semantics:
 
<haskell>
 
data Behavior a = Behavior (Time -> a)
 
</haskell>
 
</div>
 
|}
 
  
* page 26 of [https://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.91.3579&rep=rep1&type=pdf How to Declare an Imperative] by Philip Wadler:
+
:<haskell>
:{|
+
type C a         = (OI, a)
|<div style="border-left:1px solid lightgray; padding: 1em" alt="blockquote">
 
The type <code>'a io</code> is represented by a function expecting a dummy argument of type <code>unit</code> and returning a value of type <code>'a</code>.
 
<pre>
 
type 'a io = unit -> a
 
</pre>
 
</div>
 
<sup> </sup>
 
<haskell>
 
type Io a = () -> a
 
</haskell>
 
|}
 
  
* The [https://www.vex.net/~trebla/haskell/IO.xhtml Haskell I/O Tutorial] by Albert Lai:
+
extract          :: C a -> a
:{|
+
extract (u, x)   =  let !_ = partOI u in x
|<div style="border-left:1px solid lightgray; padding: 1em" alt="blockquote">
 
But I can already tell you why we cannot follow other languages and use simply <code>X</code> or <code>() -> X</code>.
 
</div>
 
|}
 
  
* [http://comonad.com/reader/2011/free-monads-for-less-3 Free Monads for Less (Part 3 of 3): Yielding IO] by Edward Kmett:
+
duplicate        :: C a -> C (C a)
:{|
+
duplicate (u, x) = let !(u1, u2) = partOI u in
|<div style="border-left:1px solid lightgray; padding: 1em" alt="blockquote">
+
                    (u2, (u1, x))
<haskell>
 
newtype OI a = forall o i. OI (FFI o i) o (i -> a) deriving Functor
 
</haskell>
 
</div>
 
<sup> </sup>
 
<haskell>
 
type Oi a = forall i . i -> a
 
</haskell>
 
|}
 
  
* page 27 of [https://blog.higher-order.com/assets/scalaio.pdf Purely Functional I/O in Scala] by Rúnar Bjarnason:
+
extend          :: (C a -> b) -> C a -> C b
:{|
+
extend h (u, x) = let !(u1, u2) = partOI u in
|<div style="border-left:1px solid lightgray; padding: 1em" alt="blockquote">
+
                    let !y        = h (u1, x) in
<pre>
+
                    (u2, y)
class IO[A](run: () => A)
 
</pre>
 
</div>
 
<sup> </sup>
 
<haskell>
 
class Io a where run :: () -> a
 
</haskell>
 
|}
 
 
 
* [http://www.fssnip.net/6i/title/Tiny-IO-Monad igeta's snippet]:
 
:{|
 
|<div style="border-left:1px solid lightgray; padding: 1em" alt="blockquote">
 
<pre>
 
type IO<'T> = private | Action of (unit -> 'T)
 
</pre>
 
</div>
 
<sup> </sup>
 
<haskell>
 
data IO t = Action (() -> t)
 
</haskell>
 
|}
 
  
* [https://stackoverflow.com/questions/6647852/haskell-actual-io-monad-implementation-in-different-language/6706442#6706442 ysdx's answer] to [https://stackoverflow.com/questions/6647852/haskell-actual-io-monad-implementation-in-different-language this SO question]:
+
getcharC        :: C () -> Char
:{|
+
getcharC (u, ()) =  getChar u
|<div style="border-left:1px solid lightgray; padding: 1em" alt="blockquote">
 
Let's say you want to implement <code>IO</code> in SML :
 
<pre>
 
structure Io : MONAD =
 
struct
 
  type 'a t = unit -> 'a
 
        ⋮
 
end
 
</pre>
 
</div>
 
<sup> </sup>
 
<haskell>
 
type T a = () -> a
 
</haskell>
 
|}
 
  
* [https://stackoverflow.com/questions/45136398/is-the-monadic-io-construct-in-haskell-just-a-convention/45141523#45141523 luqui's answer] to [https://stackoverflow.com/questions/45136398/is-the-monadic-io-construct-in-haskell-just-a-convention this SO question]:
+
putcharC        :: C Char -> ()
:{|
+
putcharC (u, c) =  putChar c u
|<haskell>
 
newtype IO a = IO { runIO :: () -> a }
 
</haskell>
 
|}
 
  
* [https://stackoverflow.com/questions/15418075/the-reader-monad/15419592#15419592 luqui's answer] to [https://stackoverflow.com/questions/15418075/the-reader-monad this SO question]:
 
:{|
 
|<haskell>
 
newtype Supply r a = Supply { runSupply :: r -> a }
 
 
</haskell>
 
</haskell>
|}
 
  
* [https://stackoverflow.com/questions/51770808/how-exactly-does-ios-work-under-the-hood/51772273#51772273 chi's answer] to [https://stackoverflow.com/questions/51770808/how-exactly-does-ios-work-under-the-hood this SO question]:
+
* [[Arrow|arrow]]:
:{|
 
|<div style="border-left:1px solid lightgray; padding: 1em" alt="blockquote">
 
As long as we have its special case <code>IO c = () ~> c</code>, we can represent (up to isomorphism) […] <code>a ~> c</code> […]
 
</div>
 
|}
 
  
* [https://luxlang.blogspot.com/2016/01/monads-io-and-concurrency-in-lux.html Monads, I/O and Concurrency in Lux] by Eduardo Julián:
+
:<haskell>
:{|
+
type A b c   (OI -> b) -> (OI -> c)
|<div style="border-left:1px solid lightgray; padding: 1em" alt="blockquote">
 
<pre>
 
(deftype #export (IO a)
 
   (-> Void a))
 
</pre>
 
</div>
 
<sup> </sup>
 
<haskell>
 
type IO a = (->) Void a
 
</haskell>
 
|}
 
  
* [https://mperry.github.io/2014/01/03/referentially-transparent-io.html Referentially Transparent Input/Output in Groovy] by Mark Perry:
+
arr          :: (b -> c) -> A b c
:{|
+
arr f        =  \ c' u -> let !x = c' u in f x
|<div style="border-left:1px solid lightgray; padding: 1em" alt="blockquote">
 
<pre>
 
abstract class SimpleIO<A> {
 
    abstract A run()
 
}
 
</pre>
 
</div>
 
<sup> </sup>
 
<haskell>
 
class SimpleIO a where
 
    run :: () -> a
 
</haskell>
 
|}
 
  
* [https://github.com/php-fp/php-fp-io#readme The <code>IO</code> Monad for PHP] by Tom Harding:
+
both        :: A b c -> A b' c' -> A (b, b') (c, c')
:{|
+
f' `both` g' = \ c' u -> let !(u1:u2:u3:_) = partsOI u in
|<div style="border-left:1px solid lightgray; padding: 1em" alt="blockquote">
+
                          let !(x, x')      = c' u1 in
<pre>
+
                          let !y            = f' (unit x) u2 in
__construct :: (-> a) -> IO a
+
                          let !y'          = g' (unit x') u3 in
</pre>
+
                          (y, y')
[...]  The parameter to the constructor must be a zero-parameter [none-adic] function that returns a value.
+
                where
</div>
+
                  unit x u = let !_ = partOI u in x
<sup> </sup>
 
<haskell>
 
data IO a = IO (() -> a)
 
__construct :: (() -> a) -> IO a
 
__construct = IO
 
</haskell>
 
|}
 
  
* [https://medium.com/@luijar/the-observable-disguised-as-an-io-monad-c89042aa8f31 The Observable disguised as an IO Monad] by Luis Atencio:
+
getcharA    :: A () Char
:{|
+
getcharA    = \ c' u -> let !(u1, u2) = partOI u in
|<div style="border-left:1px solid lightgray; padding: 1em" alt="blockquote">
+
                          let !_        = c' u1 in
<code>IO</code> is a very simple monad that implements a slightly modified version of our abstract interface with the difference that instead of wrapping a value <code>a</code>, it wraps a side effect function <code>() -> a</code>.
+
                          let !ch      = getChar u2 in
</div>
+
                          ch   
<sup> </sup>
 
<haskell>
 
data IO a = Wrap (() -> a)
 
</haskell>
 
|}
 
  
* [https://weblogs.asp.net/dixin/category-theory-via-c-sharp-18-more-monad-io-monad More Monad: <code>IO<></code> Monad], from [https://weblogs.asp.net/dixin/Tags/Category%20Theory dixin's Category Theory via C#] series:
+
putcharA    :: A Char ()
:{|
+
putcharA    = \ c' u -> let !(u1, u2) = partOI u in
|<div style="border-left:1px solid lightgray; padding: 1em" alt="blockquote">
+
                          let !ch      = c' u1 in
The definition of <code>IO<></code> is simple:
+
                          let !z        = putChar ch u2 in
<pre>
+
                          z
public delegate T IO<out T>();
 
</pre>
 
[...]
 
* <code>IO<T></code> is used to represent a impure function. When a <code>IO<T></code> function is applied, it returns a <code>T</code> value, with side effects.
 
</div>
 
<sup> </sup>
 
<haskell>
 
type IO t = () -> t
 
 
</haskell>
 
</haskell>
|}
 
  
* [https://discuss.ocaml.org/t/io-monad-for-ocaml/4618/11 ivg's post] in [https://discuss.ocaml.org/t/io-monad-for-ocaml/4618 <code>IO</code> Monad for OCaml]
+
including [https://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.91.3579&rep=rep1&type=pdf those used in earlier versions] of Haskell:
:{|
 
|<div style="border-left:1px solid lightgray; padding: 1em" alt="blockquote">
 
So let’s implement the <code>IO</code> Monad right now and here. Given that OCaml is strict and that the order of function applications imposes the order of evaluation, the <code>IO</code> Monad is just a thunk, e.g.,
 
<pre>
 
type 'a io = unit -> 'a
 
</pre>
 
</div>
 
<sup> </sup>
 
<haskell>
 
type Io a = () -> a
 
</haskell>
 
|}
 
  
* [https://arrow-kt.io/docs/effects/io Why <code>suspend</code> over <code>IO</code>] in [https://arrow-kt.io/docs/fx Arrow Fx]:
+
* dialogues:
:{|
 
|<div style="border-left:1px solid lightgray; padding: 1em" alt="blockquote">
 
[...] So <code>suspend () -> A</code> offers us the exact same guarantees as <code>IO<A></code>.
 
</div>
 
|}
 
  
Of these, it is the [https://hackage.haskell.org/package/oi/docs/src/Data-OI-Internal.html#OI implementation of <code>OI a</code>] in Yamashita's [https://hackage.haskell.org/package/oi oi] package which is most interesting as its values are ''monousal'' - once used, their contents remain constant. This single-use property also appears in the implementation of the abstract <code>decision</code> type described by F. Warren Burton in [https://academic.oup.com/comjnl/article-pdf/31/3/243/1157325/310243.pdf Nondeterminism with Referential Transparency in Functional Programming Languages].
+
:<haskell>
 +
runD :: ([Response] -> [Request]) -> OI -> ()
 +
runD d u = foldr (\ (!_) -> id) () $ yet $ \ l -> zipWith respond (d l) (partsOI u)
  
----
+
yet :: (a -> a) -> a
=== <code>IO</code><u>, redefined</u> ===
+
yet f = f (yet f)
  
Based on these and other observations, a reasonable distillment of these examples would be <code>OI -> a</code>, which then implies:
+
respond :: Request -> OI -> Response
 +
respond Getq    u = let !c = getChar u in Getp c
 +
respond (Putq c) u = let !_ = putChar c u in Putp
  
<haskell>
+
data Request  = Getq | Putq Char
type IO a = OI -> a
+
data Response = Getp Char | Putp
 
</haskell>
 
</haskell>
  
Using Burton's ''pseudodata'' approach:
+
* continuations:
 
 
<haskell>
 
-- abstract; single-use I/O-access mediator
 
data Exterior
 
getchar :: Exterior -> Char
 
putchar :: Char -> Exterior -> ()
 
 
 
-- from section 2 of Burton's paper
 
data Tree a = Node { contents :: a,
 
                    left    :: Tree a,
 
                    right    :: Tree a }
 
  
-- utility definitions
+
:<haskell>
type OI =  Tree Exterior
+
type Answer = OI -> ()
  
getChar' :: OI -> Char
+
runK :: Answer -> IO -> ()
getChar' = getchar . contents
+
runK a u = a u
  
putChar' :: Char -> OI -> ()
+
doneK :: Answer
putChar' c = putchar c . contents
+
doneK = \ u -> let !_ = partOI u in ()
  
part    :: OI -> (OI, OI)
+
getcharK :: (Char -> Answer) -> Answer
parts    :: OI -> [OI]
+
getcharK k  = \ u -> let !(u1, u2) = partOI u in
 +
                      let !c        = getChar u1 in
 +
                      let !a        = k c in
 +
                      a u2
  
part t  = (left t, right t)
+
putcharK :: Char -> Answer -> Answer
parts t  =  let !(t1, t2) = part t in
+
putcharK c a = \ u -> let !(u1, u2) = partOI u in
            t1 : parts t2
+
                      let !_        = putChar c u1 in
 +
                      a u2
 
</haskell>
 
</haskell>
  
Of course, in an actual implementation <code>OI</code> would be abstract like <code>World</code>, and for similar reasons. This permits a simpler implementation for <code>OI</code> and its values, instead of being based on (theoretically) infinite structured values like binary trees. That simplicity has benefits for the <code>OI</code> interface, in this case:
+
and even <i>that</i> <s><i>world</i></s> state-passing style, which is also used by [https://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.17.935&rep=rep1&type=pdf Clean], [https://staff.science.uva.nl/c.u.grelck/publications/HerhSchoGrelDAMP09.pdf Single-Assignment C] and as part of the I/O model used for the verification of interactive programs in [https://cakeml.org/vstte18.pdf CakeML], remembering that <code>OI</code> values can only be used once:
  
 
<haskell>
 
<haskell>
data OI
+
newtype World = W OI
part :: OI -> (OI, OI)
+
 
getChar' :: OI -> Char
+
getcharL :: World -> (Char, World)
putChar' :: Char -> OI -> ()
+
getcharL (W u) = let !(u1, u2) = partOI u in
 +
                let !c = getChar u1 in
 +
                (c, W u2)
 +
 
 +
putcharL :: Char -> World -> World
 +
putcharL c (W u) = let !(u1, u2) = partOI u in
 +
                  let !_ = putChar u1 in
 +
                  W u2
 
</haskell>
 
</haskell>
 
<sup> </sup>
 
<sup> </sup>
  
 
----
 
----
 
 
=== <u>See also</u> ===
 
=== <u>See also</u> ===
  
* [https://pqnelson.github.io/2021/07/29/monadic-io-in-ml.html Monadic IO in Standard ML]
+
* [[Plainly partible]]
 
* [[Disposing of dismissives]]
 
* [[Disposing of dismissives]]
 
* [[IO then abstraction]]
 
* [[IO then abstraction]]
* [https://okmij.org/ftp/Computation/IO-monad-history.html The IO monad in 1965]
+
 
 +
[[Category:Theoretical foundations]]

Latest revision as of 12:12, 5 December 2022

There is a world of difference between the value echoML which has no side effects when evaluated, and the computation echoML (), which does.

How to Declare an Imperative, Philip Wadler (page 25 of 33).

Of course, that assumes everything in the program's “world” required by echoML actually works as intended: reality isn't always so obliging! To then define Haskell's I/O type as:

type IO a  =  World -> (a, World)

[where an] IO computation is a function that (logically) takes the state of the world, and returns a modified world as well as the return value.

A History of Haskell: Being Lazy With Class, Paul Hudak, John Hughes, Simon Peyton Jones and Philip Wadler.

...seems rather optimistic.


The determining of IO

Since reality isn't always so deterministic in behaviour, perhaps the study of nondeterminism can provide a more plausible implementation:

We propose to solve this problem [existing constructs for nondeterminism not being compatible with the mathematical foundations of functional programming] by placing the nondeterminism in pseudo-data. A program is passed an infinite tree of two-valued decisions, along with its input. These decisions may be fixed at runtime, thereby permitting nondeterminism. Once fixed, a decision remains unchanged so equivalent expression must always have the same value.

Nondeterminism with Referential Transparency in Functional Programming Languages, F. Warren Burton (front page).

There's more:

The approach generalizes so that a program can make use of other run-time information such as the current time or current amount of available storage.

Using this pseudo-data approach:

 -- abstract; single-use I/O-access mediator
data Exterior
getchar :: Exterior -> Char
putchar :: Char -> Exterior -> ()

 -- from section 2 of Burton's paper
data Tree a = Node { contents :: a,
                     left     :: Tree a,
                     right    :: Tree a }

 -- utility definitions
type OI  =  Tree Exterior

main'    :: OI -> ()
main'    =  ...

getChar' :: OI -> Char
getChar' =  getchar . contents

putChar' :: Char -> OI -> ()
putChar' c = putchar c . contents

part     :: OI -> (OI, OI)
parts    :: OI -> [OI]

part t   =  (left t, right t)
parts t  =  let !(t1, t2) = part t in
            t1 : parts t2

To avoid the visible use of trees, the single-use property can instead be applied directly to OI values. This permits an abstract definition of the OI type:

data OI
partOI  :: OI -> (OI, OI)
getChar :: OI -> Char
putChar :: Char -> OI -> ()

The choice to use (theoretically) infinite structured values (binary trees or otherwise) is then an implementation matter.


Other interfaces

In addition to the current one:

type M a   =  OI -> a

unit       :: a -> M a
unit x     =  \ u -> let !_ = partOI u in x 

bind       :: M a -> (a -> M b) -> M b
bind m k   =  \ u -> let !(u1, u2) = partOI u in
                     let !x = m u1 in
                     let !y = k x u2 in
                     y

getcharM   :: M Char
getcharM   =  getChar

putcharM   :: Char -> M () 
putcharM   =  putChar

the OI interface can be used to implement other models of I/O:

type C a         =  (OI, a)

extract          :: C a -> a
extract (u, x)   =  let !_ = partOI u in x

duplicate        :: C a -> C (C a)
duplicate (u, x) =  let !(u1, u2) = partOI u in
                    (u2, (u1, x))

extend           :: (C a -> b) -> C a -> C b
extend h (u, x)  =  let !(u1, u2) = partOI u in
                    let !y        = h (u1, x) in
                    (u2, y)

getcharC         :: C () -> Char
getcharC (u, ()) =  getChar u

putcharC         :: C Char -> ()
putcharC (u, c)  =  putChar c u
type A b c   =  (OI -> b) -> (OI -> c)

arr          :: (b -> c) -> A b c
arr f        =  \ c' u -> let !x = c' u in f x

both         :: A b c -> A b' c' -> A (b, b') (c, c')
f' `both` g' =  \ c' u -> let !(u1:u2:u3:_) = partsOI u in
                          let !(x, x')      = c' u1 in
                          let !y            = f' (unit x) u2 in
                          let !y'           = g' (unit x') u3 in
                          (y, y')
                where
                  unit x u = let !_ = partOI u in x

getcharA     :: A () Char
getcharA     =  \ c' u -> let !(u1, u2) = partOI u in
                          let !_        = c' u1 in
                          let !ch       = getChar u2 in
                          ch     

putcharA     :: A Char ()
putcharA     =  \ c' u -> let !(u1, u2) = partOI u in
                          let !ch       = c' u1 in
                          let !z        = putChar ch u2 in
                          z

including those used in earlier versions of Haskell:

  • dialogues:
runD :: ([Response] -> [Request]) -> OI -> ()
runD d u = foldr (\ (!_) -> id) () $ yet $ \ l -> zipWith respond (d l) (partsOI u)

yet :: (a -> a) -> a
yet f = f (yet f)

respond :: Request -> OI -> Response
respond Getq     u = let !c = getChar u in Getp c
respond (Putq c) u = let !_ = putChar c u in Putp

data Request  = Getq | Putq Char
data Response = Getp Char | Putp
  • continuations:
type Answer = OI -> ()

runK :: Answer -> IO -> ()
runK a u = a u

doneK :: Answer
doneK = \ u -> let !_ = partOI u in ()

getcharK :: (Char -> Answer) -> Answer
getcharK k   = \ u -> let !(u1, u2) = partOI u in
                      let !c        = getChar u1 in
                      let !a        = k c in
                      a u2

putcharK :: Char -> Answer -> Answer
putcharK c a = \ u -> let !(u1, u2) = partOI u in
                      let !_        = putChar c u1 in
                      a u2

and even that world state-passing style, which is also used by Clean, Single-Assignment C and as part of the I/O model used for the verification of interactive programs in CakeML, remembering that OI values can only be used once:

newtype World = W OI

getcharL :: World -> (Char, World)
getcharL (W u) = let !(u1, u2) = partOI u in
                 let !c = getChar u1 in
                 (c, W u2)

putcharL :: Char -> World -> World
putcharL c (W u) = let !(u1, u2) = partOI u in
                   let !_ = putChar u1 in
                   W u2


See also