# Difference between revisions of "Output/Input"

m (...) |
(Article rewritten) |
||

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

Line 1: | Line 1: | ||

[[Category:Theoretical foundations]] | [[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. | ||

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

+ | |||

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

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

− | + | [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 | + | ...seems rather optimistic. |

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

+ | |||

+ | ---- | ||

+ | === <u>The determining of <code>IO</code></u> === | ||

+ | |||

+ | Since reality isn't always so deterministic in behaviour, perhaps the study of <i>nondeterminism</i> can provide a more plausible implementation: | ||

+ | |||

+ | <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 <code>decisions</code>, along with its input. These <code>decisions</code> may be fixed at runtime, thereby permitting nondeterminism. Once fixed, a <code>decision</code> 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> |

− | + | Using this <i>pseudo-data</i> approach: | |

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

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

− | |||

− | |||

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

− | |||

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

− | + | ||

− | |||

− | < | ||

− | |||

− | < | ||

− | </ | ||

− | |||

<haskell> | <haskell> | ||

− | data | + | data OI |

+ | partOI :: OI -> (OI, OI) | ||

+ | getChar :: OI -> Char | ||

+ | putChar :: Char -> OI -> () | ||

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

− | |||

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

− | |||

− | |||

− | |||

− | |||

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

− | |||

− | |||

− | |||

− | |||

− | + | ---- | |

+ | === <u>Other interfaces</u> === | ||

+ | |||

+ | In addition to the [[Monad|current]] one: | ||

− | |||

<haskell> | <haskell> | ||

− | type a | + | 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 | |

− | |||

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

− | |||

− | + | the <code>OI</code> interface can be used to implement other models of I/O: | |

− | |||

− | |||

− | |||

− | |||

− | |||

− | |||

− | |||

− | |||

− | |||

− | |||

− | |||

− | |||

− | * | + | * [[Comonad|comonad]]: |

− | |||

− | |||

− | |||

− | |||

− | |||

− | |||

− | |||

− | |||

− | + | :<haskell> | |

− | + | type C a = (OI, a) | |

− | |||

− | |||

− | |||

− | |||

− | |||

− | |||

− | |||

− | <haskell> | ||

− | type | ||

− | |||

− | |||

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

− | |||

− | |||

− | |||

− | |||

− | |||

− | |||

− | |||

− | |||

− | |||

− | |||

− | |||

− | |||

− | |||

− | |||

− | |||

− | |||

− | |||

− | |||

− | |||

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

− | |||

− | * [ | + | * [[Arrow|arrow]]: |

− | |||

− | |||

− | |||

− | |||

− | |||

− | + | :<haskell> | |

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

− | |||

− | |||

− | |||

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

− | |||

− | |||

− | |||

− | |||

− | |||

− | |||

− | |||

− | |||

− | |||

− | |||

− | |||

− | type | ||

− | |||

− | |||

− | * | + | * dialogues: |

− | |||

− | |||

− | |||

− | |||

− | |||

− | |||

− | |||

− | |||

− | |||

− | |||

− | |||

− | |||

− | + | :<haskell> | |

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

− | |||

− | |||

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

− | + | * continuations: | |

− | <haskell> | + | :<haskell> |

− | + | type Answer = OI -> () | |

− | |||

− | |||

− | |||

− | + | runK :: Answer -> IO -> () | |

− | + | runK a u = a u | |

− | |||

− | |||

− | + | doneK :: Answer | |

− | + | doneK = \ u -> let !_ = partOI u in () | |

− | + | getcharK :: (Char -> Answer) -> Answer | |

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

− | putChar | + | putcharK c a = \ u -> let !(u1, u2) = partOI u in |

+ | let !_ = putChar c u1 in | ||

+ | a u2 | ||

+ | </haskell> | ||

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

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

− | |||

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

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

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

− | |||

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

− | * [ | + | * [[Plainly partible]] |

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

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

− |

## Latest revision as of 12:02, 28 November 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`

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

^{ }