Difference between revisions of "Output/Input"

From HaskellWiki
Jump to: navigation, search
m (Extra example added)
m
 
(17 intermediate revisions by the same user not shown)
Line 27: Line 27:
 
</haskell>
 
</haskell>
  
As the returned unit-value <code>()</code> contains no useful information, that type can be simplified further:
+
...because <i>"logically"</i> a function in Haskell has no observable effects - being exact requires a change of notation:
  
 
<haskell>
 
<haskell>
() -> a
+
() --> (a, ())
 
</haskell>
 
</haskell>
  
<sub>Why "approximately"? Because "logically" a function in Haskell has no observable effects.</sub>
+
The <i>"result"</i> (of type <code>a</code>) can then be <i>"returned"</i> directly:
 +
 
 +
<haskell>
 +
() --> a
 +
</haskell>
 +
<sup> </sup>
  
 
----
 
----
 
=== <u>Previously seen</u> ===
 
=== <u>Previously seen</u> ===
  
The type <code>() -> a</code> (or variations of it) have appeared elsewhere - examples include:
+
Variants of <code>() --> a</code> have appeared elsewhere - examples include:
  
* 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:
+
* page 2 of 13 in [https://dl.acm.org/doi/pdf/10.1145/363744.363749 A Correspondence Between ALGOL 60 and Church's Lambda-Notation: Part I] by Peter Landin:
 
:{|
 
:{|
 
|<div style="border-left:1px solid lightgray; padding: 1em" alt="blockquote">
 
|<div style="border-left:1px solid lightgray; padding: 1em" alt="blockquote">
Line 48: Line 53:
 
<sup> </sup>
 
<sup> </sup>
 
<haskell>
 
<haskell>
(\ () -> …) :: () -> a
+
(\ () --> …) :: () --> a
 
</haskell>
 
</haskell>
 
|}
 
|}
  
* page 148 of 168 in [[IO Semantics|Functional programming and Input/Output]] by Andrew Gordon:
+
* page 27 of [https://blog.higher-order.com/assets/scalaio.pdf Purely Functional I/O in Scala] by Rúnar Bjarnason:
 
:{|
 
:{|
 
|<div style="border-left:1px solid lightgray; padding: 1em" alt="blockquote">
 
|<div style="border-left:1px solid lightgray; padding: 1em" alt="blockquote">
 
<pre>
 
<pre>
abstype 'a Job = JOB of unit -> 'a
+
class IO[A](run: () => A)
 
</pre>
 
</pre>
 
</div>
 
</div>
 
<sup> </sup>
 
<sup> </sup>
 
<haskell>
 
<haskell>
data Job a = JOB (() -> a)
+
class Io a where run :: () --> a
 
</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:
+
* [http://www.fssnip.net/6i/title/Tiny-IO-Monad igeta's snippet]:
 
:{|
 
:{|
 
|<div style="border-left:1px solid lightgray; padding: 1em" alt="blockquote">
 
|<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>.
+
<pre>
 +
type IO<'T> = private | Action of (unit -> 'T)
 +
</pre>
 
</div>
 
</div>
 
<sup> </sup>
 
<sup> </sup>
 
<haskell>
 
<haskell>
type Obs tau = State -> tau
+
data IO t = Action (() --> t)
 
</haskell>
 
</haskell>
 
|}
 
|}
  
* [https://image.slidesharecdn.com/lazyio-120422092926-phpapp01/95/lazy-io-15-728.jpg page 15] of ''Non-Imperative Functional Programming'' by Nobuo Yamashita:
+
* [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]:
 
 
 
:{|
 
:{|
 +
|<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>
 
<haskell>
type a :-> b = OI a -> b
+
type T a = () --> a
 
</haskell>
 
</haskell>
 
|}
 
|}
  
* [http://h2.jaguarpaw.co.uk/posts/mtl-style-for-free MTL style for free] by Tom Ellis:
+
* [https://luxlang.blogspot.com/2016/01/monads-io-and-concurrency-in-lux.html Monads, I/O and Concurrency in Lux] by Eduardo Julián:
 
+
:{|
:{|
+
|<div style="border-left:1px solid lightgray; padding: 1em" alt="blockquote">
 +
<pre>
 +
(deftype #export (IO a)
 +
  (-> Void a))
 +
</pre>
 +
</div>
 +
<sup> </sup>
 
<haskell>
 
<haskell>
data Time_ a = GetCurrentTime (UTCTime -> a)
+
type IO a = (-->) Void a
 
</haskell>
 
</haskell>
 
|}
 
|}
  
* [http://h2.jaguarpaw.co.uk/posts/impure-lazy-language An impure lazy programming language], also by Tom Ellis:
+
* [https://mperry.github.io/2014/01/03/referentially-transparent-io.html Referentially Transparent Input/Output in Groovy] by Mark Perry:
 
 
 
:{|
 
:{|
 +
|<div style="border-left:1px solid lightgray; padding: 1em" alt="blockquote">
 +
<pre>
 +
abstract class SimpleIO<A> {
 +
    abstract A run()
 +
}
 +
</pre>
 +
</div>
 +
<sup> </sup>
 
<haskell>
 
<haskell>
data IO a = IO (() -> a)
+
class SimpleIO a where
 +
    run :: () --> 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:
+
* [https://github.com/php-fp/php-fp-io#readme The <code>IO</code> Monad for PHP] by Tom Harding:
 
:{|
 
:{|
 
|<div style="border-left:1px solid lightgray; padding: 1em" alt="blockquote">
 
|<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>
 
<pre>
:: Create a :==  Id -> a
+
__construct :: (-> a) -> IO a
 
</pre>
 
</pre>
 +
[...]  The parameter to the constructor must be a zero-parameter [none-adic] function that returns a value.
 
</div>
 
</div>
 
<sup> </sup>
 
<sup> </sup>
 
<haskell>
 
<haskell>
type Create a = Id -> a
+
data IO a = IO (() --> a)
 +
__construct :: (() --> a) -> IO a
 +
__construct = IO
 
</haskell>
 
</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:
+
* [https://medium.com/@luijar/the-observable-disguised-as-an-io-monad-c89042aa8f31 The Observable disguised as an IO Monad] by Luis Atencio:
 
:{|
 
:{|
 
|<div style="border-left:1px solid lightgray; padding: 1em" alt="blockquote">
 
|<div style="border-left:1px solid lightgray; padding: 1em" alt="blockquote">
An early implementation of Fran represented behaviors as implied in the formal semantics:
+
<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>.
 +
</div>
 +
<sup> </sup>
 
<haskell>
 
<haskell>
data Behavior a = Behavior (Time -> a)
+
data IO a = Wrap (() --> a)
 
</haskell>
 
</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:
+
* [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:  
 
:{|
 
:{|
 
|<div style="border-left:1px solid lightgray; padding: 1em" alt="blockquote">
 
|<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>.
+
The definition of <code>IO<></code> is simple:
 
<pre>
 
<pre>
type 'a io = unit -> a
+
public delegate T IO<out T>();
 
</pre>
 
</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>
 
</div>
 
<sup> </sup>
 
<sup> </sup>
 
<haskell>
 
<haskell>
type Io a = () -> a
+
type IO t = () --> t
 
</haskell>
 
</haskell>
 
|}
 
|}
  
* The [https://www.vex.net/~trebla/haskell/IO.xhtml Haskell I/O Tutorial] by Albert Lai:
+
* [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]
 
:{|
 
:{|
 
|<div style="border-left:1px solid lightgray; padding: 1em" alt="blockquote">
 
|<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>.
+
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.,
</div>
+
<pre>
|}
+
type 'a io = unit -> 'a
 
+
</pre>
* [http://comonad.com/reader/2011/free-monads-for-less-3 Free Monads for Less (Part 3 of 3): Yielding IO] by Edward Kmett:
 
:{|
 
|<div style="border-left:1px solid lightgray; padding: 1em" alt="blockquote">
 
<haskell>
 
newtype OI a = forall o i. OI (FFI o i) o (i -> a) deriving Functor
 
</haskell>
 
 
</div>
 
</div>
 
<sup> </sup>
 
<sup> </sup>
 
<haskell>
 
<haskell>
type Oi a = forall i . i -> a
+
type Io a = () --> a
 
</haskell>
 
</haskell>
 
|}
 
|}
  
* page 27 of [https://blog.higher-order.com/assets/scalaio.pdf Purely Functional I/O in Scala] by Rúnar Bjarnason:
+
* [https://arrow-kt.io/docs/effects/io Why <code>suspend</code> over <code>IO</code>] in [https://arrow-kt.io/docs/fx Arrow Fx]:
 
:{|
 
:{|
 
|<div style="border-left:1px solid lightgray; padding: 1em" alt="blockquote">
 
|<div style="border-left:1px solid lightgray; padding: 1em" alt="blockquote">
<pre>
+
[...] So <code>suspend () -> A</code> offers us the exact same guarantees as <code>IO<A></code>.
class IO[A](run: () => A)
 
</pre>
 
 
</div>
 
</div>
<sup> </sup>
 
<haskell>
 
class Io a where run :: () -> a
 
</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]:
+
==== Avoiding alternate annotations ====
 +
 
 +
Having to deal with both <code>-></code> and <code>--></code> is annoying - another option is to use a different argument type, instead of <code>()</code>:
 +
 
 +
* 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:
 
:{|
 
:{|
 
|<div style="border-left:1px solid lightgray; padding: 1em" alt="blockquote">
 
|<div style="border-left:1px solid lightgray; padding: 1em" alt="blockquote">
Let's say you want to implement <code>IO</code> in SML :
+
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>.
<pre>
 
structure Io : MONAD =
 
struct
 
  type 'a t = unit -> 'a
 
        ⋮
 
end
 
</pre>
 
 
</div>
 
</div>
 
<sup> </sup>
 
<sup> </sup>
 
<haskell>
 
<haskell>
type T a = () -> a
+
type Obs tau = State -> tau
 
</haskell>
 
</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]:
+
* [https://image.slidesharecdn.com/lazyio-120422092926-phpapp01/95/lazy-io-15-728.jpg page 15] of ''Non-Imperative Functional Programming'' by Nobuo Yamashita:
 
:{|
 
:{|
|<haskell>
+
<haskell>
newtype IO a = IO { runIO :: () -> a }
+
type a :-> b = OI a -> b
 
</haskell>
 
</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]:
+
* [http://h2.jaguarpaw.co.uk/posts/mtl-style-for-free MTL style for free] by Tom Ellis:
 
:{|
 
:{|
|<haskell>
+
<haskell>
newtype Supply r a = Supply { runSupply :: r -> a }
+
data Time_ a = GetCurrentTime (UTCTime -> 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]:
+
* 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:
 
:{|
 
:{|
 
|<div style="border-left:1px solid lightgray; padding: 1em" alt="blockquote">
 
|<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> […]
+
[...] The type <code>Id</code> can be hidden by the synonym data type
 +
<pre>
 +
:: Create a :==  Id -> a
 +
</pre>
 
</div>
 
</div>
 +
<sup> </sup>
 +
<haskell>
 +
type Create a = Id -> a
 +
</haskell>
 
|}
 
|}
  
* [https://mperry.github.io/2014/01/03/referentially-transparent-io.html Referentially Transparent Input/Output in Groovy] by Mark Perry:
+
* 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:
 
:{|
 
:{|
 
|<div style="border-left:1px solid lightgray; padding: 1em" alt="blockquote">
 
|<div style="border-left:1px solid lightgray; padding: 1em" alt="blockquote">
<pre>
+
An early implementation of Fran represented behaviors as implied in the formal semantics:
abstract class SimpleIO<A> {
 
    abstract A run()
 
}
 
</pre>
 
</div>
 
<sup> </sup>
 
 
<haskell>
 
<haskell>
class SimpleIO a where
+
data Behavior a = Behavior (Time -> a)
    run :: () -> a
 
 
</haskell>
 
</haskell>
 +
</div>
 
|}
 
|}
  
Line 252: Line 274:
 
  -- utility definitions
 
  -- utility definitions
 
type OI  =  Tree Exterior
 
type OI  =  Tree Exterior
 +
 +
main'    :: OI -> ()
 +
main'    =  ...
  
 
getChar' :: OI -> Char
 
getChar' :: OI -> Char
Line 278: Line 303:
  
 
----
 
----
 +
=== <u>Other interfaces</u> ===
 +
 +
In addition to the [[Monad|current]] one:
 +
 +
<haskell>
 +
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
 +
</haskell>
 +
 +
the <code>OI</code> interface can be used to implement other models of I/O:
 +
 +
* [[Comonad|comonad]]:
 +
 +
:<haskell>
 +
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)
 +
</haskell>
 +
 +
* [[Arrow|arrow]]:
 +
 +
:<haskell>
 +
type A b c  =  (OI -> b) -> (OI -> c)
 +
 +
arr          :: (b -> c) -> A b c
 +
arr f        =  \ c' u -> f $! c' u
 +
 +
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')                         
 +
 +
unit        :: a -> OI -> a
 +
unit x u    = let !_ = partOI u in x
 +
</haskell>
 +
 +
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:
 +
 +
* dialogues:
 +
 +
:<haskell>
 +
runD :: ([Response] -> [Request]) -> OI -> ()
 +
runD d u = foldr (\ (!_) -> id) () $ yet $ \ l -> zipWith respond (d l) (partsOI u)
  
=== <u>Various questions</u> ===
+
yet :: (a -> a) -> a
 +
yet f = f (yet f)
  
* Is the C language "purely functional"?
+
respond :: Request -> OI -> Response
 +
respond Getq    u = let !c = getChar' u in Getp c
 +
respond (Putq c) u = let !_ = putChar' c u in Putp
  
::No:
+
data Request  = Getq | Putq Char
::* C isn't "pure" - it allows unrestricted access to observable effects, including those of I/O.
+
data Response = Getp Char | Putp
::* C isn't "functional" - it was never intended to be [[Referential transparency|referentially transparent]], which severely restricts the ability to use [[Equational reasoning examples|equational reasoning]].
+
</haskell>
  
* Is the Haskell language "purely functional"?
+
* continuations:
  
::[https://chadaustin.me/2015/09/haskell-is-not-a-purely-functional-language Haskell is not a purely functional language], but is often described as being referentially transparent.
+
:<haskell>
 +
type Answer = OI -> ()
  
* Can functional programming be liberated from the von Neumann paradigm?
+
runK :: Answer -> IO -> ()
 +
runK a u = a u
  
::That remains an [[Open research problems|open research problem]].
+
doneK :: Answer
 +
doneK = \ u -> let !_ = partOI u in ()
  
* Can a language be "purely functional" or "denotative"?
+
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
  
::Conditionally, yes - the condition being the language is restricted in what domains it can be used in:
+
putcharK :: Char -> Answer -> Answer
 +
putcharK c a = \ u -> let !(u1, u2) = partOI u in
 +
                      let !_        = putChar' c u1 in
 +
                      a u2
 +
</haskell>
  
::* If a language is free of observable effects, including those of I/O, then the only other place where those effects can reside is within its implementation.
+
and even that <s><i>pass-the-planet</i></s> state-based 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:
::* There is no bound on the ways in which observable effects can be usefully combined, leading to a similarly-unlimited variety of imperative computations.
 
::* A finite implementation cannot possibly accommodate all of those computations, so a subset of them must be chosen. This restricts the implementation and language to those domains supported by the chosen computations.
 
  
* Why do our programs need to read input and write output?
+
<haskell>
 +
newtype World = W OI
  
::Because programs are usually written for [https://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.628.7053&rep=rep1&type=pdf practical] purposes, such as implementing domain-specific [https://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.7.2089&rep=rep1&type=pdf little languages] like [https://dhall-lang.org Dhall].
+
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
 +
</haskell>
 +
<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]
+
* [https://pqnelson.github.io/2021/07/29/monadic-io-in-ml.html Monadic IO in Standard ML]

Latest revision as of 12:45, 27 September 2022


Clearing away the smoke and mirrors

The implementation in GHC uses the following one:

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

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. 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!

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

...so what starts out as an I/O action of type:

World -> (a, World)

is changed by GHC to approximately:

() -> (a, ())

...because "logically" a function in Haskell has no observable effects - being exact requires a change of notation:

() --> (a, ())

The "result" (of type a) can then be "returned" directly:

() --> a


Previously seen

Variants of () --> a have appeared elsewhere - examples include:

The use of λ, and in particular (to avoid an irrelevant bound variable) of λ() , 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.

(\ () --> ) :: () --> a
class IO[A](run: () => A)

class Io a where run :: () --> a
type IO<'T> = private | Action of (unit -> 'T)

data IO t = Action (() --> t)

Let's say you want to implement IO in SML :

structure Io : MONAD =
struct
  type 'a t = unit -> 'a
         ⋮
end

type T a = () --> a
(deftype #export (IO a)
  (-> Void a))

type IO a = (-->) Void a
abstract class SimpleIO<A> {
    abstract A run()
}

class SimpleIO a where
    run :: () --> a
__construct :: (-> a) -> IO a

[...] The parameter to the constructor must be a zero-parameter [none-adic] function that returns a value.

data IO a = IO (() --> a)
__construct :: (() --> a) -> IO a
__construct = IO

IO is a very simple monad that implements a slightly modified version of our abstract interface with the difference that instead of wrapping a value a, it wraps a side effect function () -> a.

data IO a = Wrap (() --> a)

The definition of IO<> is simple:

public delegate T IO<out T>();

[...]

  • IO<T> is used to represent a impure function. When a IO<T> function is applied, it returns a T value, with side effects.

type IO t = () --> t

So let’s implement the IO Monad right now and here. Given that OCaml is strict and that the order of function applications imposes the order of evaluation, the IO Monad is just a thunk, e.g.,

type 'a io = unit -> 'a

type Io a = () --> a

[...] So suspend () -> A offers us the exact same guarantees as IO<A>.

Avoiding alternate annotations

Having to deal with both -> and --> is annoying - another option is to use a different argument type, instead of ():

A value of type Obs 𝜏 is called an observer. Such a value observes (i.e. views or inspects) a state and returns a value of type 𝜏. [...] An observer type Obs 𝜏 may be viewed as an implicit function space from the set of states to the type 𝜏.

type Obs tau = State -> tau
  • page 15 of Non-Imperative Functional Programming by Nobuo Yamashita:
type a :-> b = OI a -> b
data Time_ a = GetCurrentTime (UTCTime -> a)

[...] The type Id can be hidden by the synonym data type

:: Create a  :==  Id -> a

type Create a = Id -> a

An early implementation of Fran represented behaviors as implied in the formal semantics:

data Behavior a = Behavior (Time -> a)

Of these, it is the implementation of OI a in Yamashita's 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 decision type described by F. Warren Burton in Nondeterminism with Referential Transparency in Functional Programming Languages.


IO, redefined

Based on these and other observations, a reasonable distillment of these examples would be OI -> a, which then implies:

type IO a = OI -> a

Using Burton's pseudodata 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

Of course, in an actual implementation OI would be abstract like World, and for similar reasons. This permits a simpler implementation for OI and its values, instead of being based on (theoretically) infinite structured values like binary trees. That simplicity has benefits for the OI interface, in this case:

data OI
part :: OI -> (OI, OI)
getChar' :: OI -> Char
putChar' :: Char -> OI -> ()


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

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)
type A b c   =  (OI -> b) -> (OI -> c)

arr          :: (b -> c) -> A b c
arr f        =  \ c' u -> f $! c' u

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')                           

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

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 pass-the-planet state-based 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