# Difference between revisions of "Output/Input"

(New content) |
m (Reference replaced) |
||

(39 intermediate revisions by the same user not shown) | |||

Line 1: | Line 1: | ||

+ | [[Category:Theoretical foundations]] | ||

+ | |||

=== <u>Clearing away the smoke and mirrors</u> === | === <u>Clearing away the smoke and mirrors</u> === | ||

Line 8: | Line 10: | ||

</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! | + | 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! |

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

Line 31: | Line 33: | ||

</haskell> | </haskell> | ||

− | Why "approximately"? Because "logically" a function in Haskell has no observable effects. | + | <sub>Why <i>"approximately"</i>? Because <i>"logically"</i> a function in Haskell has no observable effects.</sub> |

---- | ---- | ||

=== <u>Previously seen</u> === | === <u>Previously seen</u> === | ||

− | + | The type <code>() -> a</code> (or variations of it) 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://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: | ||

Line 47: | Line 49: | ||

<haskell> | <haskell> | ||

(\ () -> …) :: () -> a | (\ () -> …) :: () -> a | ||

+ | </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: | ||

+ | :{| | ||

+ | |<div style="border-left:1px solid lightgray; padding: 1em" alt="blockquote"> | ||

+ | <pre> | ||

+ | abstype 'a Job = JOB of unit -> 'a | ||

+ | </pre> | ||

+ | </div> | ||

+ | <sup> </sup> | ||

+ | <haskell> | ||

+ | data Job a = JOB (() -> a) | ||

</haskell> | </haskell> | ||

|} | |} | ||

Line 61: | Line 76: | ||

|} | |} | ||

− | * [https://image.slidesharecdn.com/lazyio-120422092926-phpapp01/95/lazy-io-15-728.jpg page 15] of ''Non-Imperative Functional Programming | + | * [https://image.slidesharecdn.com/lazyio-120422092926-phpapp01/95/lazy-io-15-728.jpg page 15] of ''Non-Imperative Functional Programming'' by Nobuo Yamashita: |

:{| | :{| | ||

Line 74: | Line 89: | ||

<haskell> | <haskell> | ||

data Time_ a = GetCurrentTime (UTCTime -> a) | data Time_ a = GetCurrentTime (UTCTime -> a) | ||

+ | </haskell> | ||

+ | |} | ||

+ | |||

+ | * [http://h2.jaguarpaw.co.uk/posts/impure-lazy-language An impure lazy programming language], also by Tom Ellis: | ||

− | data | + | :{| |

− | + | <haskell> | |

− | + | 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 | + | * 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"> | ||

Line 93: | Line 112: | ||

type Create a = Id -> a | type Create a = Id -> a | ||

</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: | ||

+ | :{| | ||

+ | |<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> | ||

|} | |} | ||

Line 98: | Line 127: | ||

:{| | :{| | ||

|<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 unit and returning a value of type <code>'a</code>. | + | 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> | <pre> | ||

type 'a io = unit -> a | type 'a io = unit -> a | ||

Line 106: | Line 135: | ||

<haskell> | <haskell> | ||

type Io a = () -> a | type Io a = () -> a | ||

+ | </haskell> | ||

+ | |} | ||

+ | |||

+ | * The [https://www.vex.net/~trebla/haskell/IO.xhtml Haskell I/O Tutorial] by Albert Lai: | ||

+ | :{| | ||

+ | |<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: | ||

+ | :{| | ||

+ | |<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> | ||

+ | <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: | ||

+ | :{| | ||

+ | |<div style="border-left:1px solid lightgray; padding: 1em" alt="blockquote"> | ||

+ | <pre> | ||

+ | 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> | </haskell> | ||

|} | |} | ||

Line 141: | Line 216: | ||

|} | |} | ||

− | Of these, it is the 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]. | + | * [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]: |

+ | :{| | ||

+ | |<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: | ||

+ | :{| | ||

+ | |<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: | ||

+ | :{| | ||

+ | |<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: | ||

+ | :{| | ||

+ | |<div style="border-left:1px solid lightgray; padding: 1em" alt="blockquote"> | ||

+ | <pre> | ||

+ | __construct :: (-> a) -> IO a | ||

+ | </pre> | ||

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

+ | </div> | ||

+ | <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: | ||

+ | :{| | ||

+ | |<div style="border-left:1px solid lightgray; padding: 1em" alt="blockquote"> | ||

+ | <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> | ||

+ | 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: | ||

+ | :{| | ||

+ | |<div style="border-left:1px solid lightgray; padding: 1em" alt="blockquote"> | ||

+ | The definition of <code>IO<></code> is simple: | ||

+ | <pre> | ||

+ | 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> | ||

+ | |} | ||

+ | |||

+ | * [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"> | ||

+ | 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]: | ||

+ | :{| | ||

+ | |<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]. | ||

---- | ---- | ||

=== <code>IO</code><u>, redefined</u> === | === <code>IO</code><u>, redefined</u> === | ||

− | Based on these and other observations, a reasonable | + | Based on these and other observations, a reasonable distillment of these examples would be <code>OI -> a</code>, which then implies: |

<haskell> | <haskell> | ||

Line 182: | Line 358: | ||

</haskell> | </haskell> | ||

− | Of course, in an actual implementation <code>OI</code> would be abstract like <code>World</code>, and for similar reasons. This | + | 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: |

<haskell> | <haskell> | ||

Line 194: | Line 370: | ||

---- | ---- | ||

− | See also | + | === <u>See also</u> === |

− | * [[ | + | * [https://pqnelson.github.io/2021/07/29/monadic-io-in-ml.html Monadic IO in Standard ML] |

+ | * [[Disposing of dismissives]] | ||

* [[IO then abstraction]] | * [[IO then abstraction]] | ||

− | * [ | + | * [https://okmij.org/ftp/Computation/IO-monad-history.html The IO monad in 1965] |

## Latest revision as of 05:27, 28 April 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, ())
```

As the returned unit-value `()`

contains no useful information, that type can be simplified further:

```
() -> a
```

_{Why "approximately"? Because "logically" a function in Haskell has no observable effects.}

__Previously seen__

The type `() -> a`

(or variations of it) have appeared elsewhere - examples include:

- page 2 of 13 in A Correspondence Between ALGOL 60 and Church's Lambda-Notation: Part I by Peter Landin:

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

- page 148 of 168 in Functional programming and Input/Output by Andrew Gordon:

abstype 'a Job = JOB of unit -> 'a

^{ }data Job a = JOB (() -> a)

- page 3 of Assignments for Applicative Languages by Vipin Swarup, Uday S. Reddy and Evan Ireland:

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

- MTL style for free by Tom Ellis:

data Time_ a = GetCurrentTime (UTCTime -> a)

- An impure lazy programming language, also by Tom Ellis:

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

- page 2 of Unique Identifiers in Pure Functional Languages by Péter Diviánszky:

[...] The type

`Id`

can be hidden by the synonym data type:: Create a :== Id -> a

^{ }type Create a = Id -> a

- page 7 of Functional Reactive Animation by Conal Elliott and Paul Hudak:

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

data Behavior a = Behavior (Time -> a)

- page 26 of How to Declare an Imperative by Philip Wadler:

The type

`'a io`

is represented by a function expecting a dummy argument of type`unit`

and returning a value of type`'a`

.type 'a io = unit -> a

^{ }type Io a = () -> a

- The Haskell I/O Tutorial by Albert Lai:

But I can already tell you why we cannot follow other languages and use simply

`X`

or`() -> X`

.

- Free Monads for Less (Part 3 of 3): Yielding IO by Edward Kmett:

newtype OI a = forall o i. OI (FFI o i) o (i -> a) deriving Functor

^{ }type Oi a = forall i . i -> a

- page 27 of Purely Functional I/O in Scala by Rúnar Bjarnason:

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

newtype IO a = IO { runIO :: () -> a }

newtype Supply r a = Supply { runSupply :: r -> a }

As long as we have its special case

`IO c = () ~> c`

, we can represent (up to isomorphism) […]`a ~> c`

[…]

- Monads, I/O and Concurrency in Lux by Eduardo Julián:

(deftype #export (IO a) (-> Void a))

^{ }type IO a = (->) Void a

- Referentially Transparent Input/Output in Groovy by Mark Perry:

abstract class SimpleIO<A> { abstract A run() }

^{ }class SimpleIO a where run :: () -> a

- The
`IO`

Monad for PHP by Tom Harding:

__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

- The Observable disguised as an IO Monad by Luis Atencio:

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

- More Monad:
`IO<>`

Monad, from dixin's Category Theory via C# series:

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>`

.

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
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 -> ()
```

^{ }