# Difference between revisions of "Output/Input"

m |
m |
||

Line 424: | Line 424: | ||

* [[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] |
* [https://pqnelson.github.io/2021/07/29/monadic-io-in-ml.html Monadic IO in Standard ML] |

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

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

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

.

#### Avoiding alternate annotations

Having to deal with both `->`

and `-->`

is annoying - another option is to use a different argument type, instead of `()`

:

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

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

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 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 *pass-the-planet*`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
```

^{ }