Difference between revisions of "Output/Input"

From HaskellWiki
Jump to navigation Jump to search
(Selected content relocated from "IO in action")
m
(12 intermediate revisions by the same user not shown)
Line 1: Line 1:
[[Category:Theoretical foundations]]
 
 
==== <u>Clearing away the smoke and mirrors</u> ====
 
 
 
<div style="border-left:1px solid lightgray; padding: 1em" alt="blockquote">
 
<div style="border-left:1px solid lightgray; padding: 1em" alt="blockquote">
  +
A purely functional program implements a <i>function</i>; it has no side effect. [...] if the side effect can’t be in the functional program, it will have to be outside it.
The implementation in GHC uses the following one:
 
 
<haskell>
 
type IO a = World -> (a, World)
 
</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!
 
   
<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://web.archive.org/web/20210415200634/https://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.13.9123&rep=rep1&type=pdf Tackling the Awkward Squad: monadic input/output, concurrency, exceptions, and foreign-language calls in Haskell], Simon Peyton Jones (pages 3-4 of 60). </tt>
 
</div>
 
</div>
   
  +
One technique has been used for similar tasks:
...so what starts out as an I/O action of type:
 
   
  +
<div style="border-left:1px solid lightgray; padding: 1em" alt="blockquote">
<haskell>
 
  +
This is discussed by Burton[https://academic.oup.com/comjnl/article-pdf/31/3/243/1157325/310243.pdf <span></span>], and is built on by Harrison[https://core.ac.uk/download/9835633.pdf <span></span>]. The effect of this proposal is to place the non-determinism <i>entirely</i> outside the software [...]
World -> (a, World)
 
</haskell>
 
   
  +
<tt>[https://academic.oup.com/comjnl/article-pdf/32/2/162/1445725/320162.pdf Functional Programming and Operating Systems], Simon B. Jones and A. F. Sinclair (page 10 of 13).</tt>
is changed by GHC to approximately:
 
  +
</div>
   
  +
It can also be used to provide access to external resources:
<haskell>
 
() -> (a, ())
 
</haskell>
 
   
  +
<div style="border-left:1px solid lightgray; padding: 1em" alt="blockquote">
...because <i>"logically"</i> a function in Haskell has no observable effects - being exact requires a change of notation:
 
  +
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.
   
  +
<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>
<haskell>
 
  +
</div>
() --> (a, ())
 
</haskell>
 
   
  +
Perhaps it can be used for I/O...
The <i>"result"</i> (of type <code>a</code>) can then be <i>"returned"</i> directly:
 
  +
<br>
   
  +
__TOC__
<haskell>
 
  +
<sup> <sup>
() --> a
 
</haskell>
 
   
 
----
 
----
=== <u>Previously seen</u> ===
+
=== <u>Details, details</u> ===
   
  +
How does it work?
Variants of <code>() --> a</code> have appeared elsewhere - examples include:
 
   
  +
<div style="border-left:1px solid lightgray; padding: 1em" alt="blockquote">
* 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:
 
  +
[...] supply each program with an extra argument consisting of an infinite (lazy) binary tree of values. (We choose a tree [...] since any number of subtrees may be extracted from an infinite tree). In practice, these values will be determined at run time (when used as arguments to a special function [...]), but once fixed will never change.
:{|
 
|<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.
 
 
</div>
 
</div>
<sup> </sup>
 
<haskell>
 
(\ () -> …) :: () --> a
 
</haskell>
 
|}
 
   
  +
...<i>“a special function”</i>: only one? More will definitely be needed! To keep matters [https://www.interaction-design.org/literature/article/kiss-keep-it-simple-stupid-a-design-principle simple], each value shall only be used <b>once</b> (if at all) as an argument to any such function.
* 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>
 
|}
 
   
* 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">
 
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>
 
 
<haskell>
 
<haskell>
  +
main' :: Tree Exterior -> ...
type Obs tau = State --> tau
 
</haskell>
 
|}
 
   
  +
-- section 2
* 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:
 
  +
data Tree a = Node { contents :: a,
:{|
 
  +
left :: Tree a,
|<div style="border-left:1px solid lightgray; padding: 1em" alt="blockquote">
 
  +
right :: Tree a }
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>
 
|}
 
   
  +
data Exterior -- the abstract value type
* page 27 of [https://blog.higher-order.com/assets/scalaio.pdf Purely Functional I/O in Scala] by Rúnar Bjarnason:
 
  +
getchar :: Exterior -> Char -- the special functions
:{|
 
  +
putchar :: Char -> Exterior -> () -- (add more as needed :-)
|<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>
 
</haskell>
|}
 
   
  +
Avoiding gratuitous repetition:
* [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]:
 
:{|
 
|<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 T a = () --> a
+
type OI = Tree Exterior
</haskell>
 
|}
 
   
  +
getChar' :: OI -> Char
* [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]:
 
  +
getChar' = getchar . contents
:{|
 
|<haskell>
 
newtype IO a = IO { runIO :: () --> a }
 
</haskell>
 
|}
 
   
  +
putChar' :: Char -> OI -> ()
* [https://luxlang.blogspot.com/2016/01/monads-io-and-concurrency-in-lux.html Monads, I/O and Concurrency in Lux] by Eduardo Julián:
 
  +
putChar' c = putchar c . contents
:{|
 
|<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>
 
</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>
 
<sup> </sup>
<haskell>
 
class SimpleIO a where
 
run :: () --> a
 
</haskell>
 
|}
 
   
  +
==== An alternative abstraction ====
* [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>
 
|}
 
   
  +
About those trees: are they really necessary? If <code>OI</code> was an abstract data type, the use of trees could at least be confined to the implementation:
* [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>
 
<haskell>
  +
data OI
type IO t = () --> t
 
  +
getChar' :: OI -> Char
  +
putChar' :: Char -> OI -> ()
 
</haskell>
 
</haskell>
|}
 
   
  +
...provided that single-use property applies directly to <code>OI</code> values (thereby deeming <i>“special”</i> any function which uses an <code>OI</code> argument). That includes the initial <code>OI</code> value supplied to each program:
* [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>
 
|}
 
 
* [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>
 
 
where <code>~></code> is used instead of <code>--></code>.
 
|}
 
 
==== 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>:
 
   
* [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>
type a :-> b = OI a -> b
+
main' :: OI -> ...
 
</haskell>
 
</haskell>
|}
 
   
  +
But most Haskell programs will need more:
* [http://h2.jaguarpaw.co.uk/posts/mtl-style-for-free MTL style for free] by Tom Ellis:
 
:{|
 
<haskell>
 
data Time_ a = GetCurrentTime (UTCTime -> a)
 
</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:
 
:{|
 
|<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>
 
<haskell>
type Create a = Id -> a
+
part :: OI -> (OI, OI)
  +
part t = (left t, right t)
 
</haskell>
 
</haskell>
|}
 
   
  +
...than two <code>OI</code> values:
* 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>
 
|}
 
 
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> ===
 
 
Based on these and other observations, a reasonable distillment of these examples would be <code>OI -> a</code>, which then implies:
 
   
 
<haskell>
 
<haskell>
type IO a = OI -> a
+
parts :: OI -> [OI]
  +
parts t = let (t1, t2) = part t in t1 : parts t2
 
</haskell>
 
</haskell>
   
  +
So <code>OI</code> can be a tree-free abstract data type after all:
Using Burton's ''pseudodata'' approach:
 
 
<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
 
 
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>
 
 
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>
 
data OI
 
data OI
part :: OI -> (OI, OI)
+
partOI :: OI -> (OI, OI)
getChar' :: OI -> Char
+
getChar :: OI -> Char
putChar' :: Char -> OI -> ()
+
putChar :: Char -> OI -> ()
 
</haskell>
 
</haskell>
 
<sup> </sup>
 
<sup> </sup>
Line 344: Line 107:
 
=== <u>Other interfaces</u> ===
 
=== <u>Other interfaces</u> ===
   
In addition to the [[Monad|current]] one:
+
* [[Monad|monad]]
   
<haskell>
+
:<haskell>
 
type M a = OI -> a
 
type M a = OI -> a
   
Line 357: Line 120:
 
let !y = k x u2 in
 
let !y = k x u2 in
 
y
 
y
</haskell>
 
   
  +
getcharM :: M Char
the <code>OI</code> interface can be used to implement other models of I/O:
 
  +
getcharM = getChar
  +
  +
putcharM :: Char -> M ()
  +
putcharM = putChar
  +
</haskell>
   
 
* [[Comonad|comonad]]:
 
* [[Comonad|comonad]]:
Line 377: Line 144:
 
let !y = h (u1, x) in
 
let !y = h (u1, x) in
 
(u2, y)
 
(u2, y)
  +
  +
getcharC :: C () -> Char
  +
getcharC (u, ()) = getChar u
  +
  +
putcharC :: C Char -> ()
  +
putcharC (u, c) = putChar c u
  +
 
</haskell>
 
</haskell>
   
Line 385: Line 159:
   
 
arr :: (b -> c) -> A b c
 
arr :: (b -> c) -> A b c
arr f = \ c' u -> f $! c' u
+
arr f = \ c' u -> let !x = c' u in f x
   
 
both :: A b c -> A b' c' -> A (b, b') (c, c')
 
both :: A b c -> A b' c' -> A (b, b') (c, c')
Line 392: Line 166:
 
let !y = f' (unit x) u2 in
 
let !y = f' (unit x) u2 in
 
let !y' = g' (unit x') u3 in
 
let !y' = g' (unit x') u3 in
(y, y')
+
(y, y')
  +
where
  +
unit x u = let !_ = partOI u in x
   
unit :: a -> OI -> a
+
getcharA :: A () Char
unit x u = let !_ = partOI u in x
+
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:
+
The <code>OI</code> interface can also be used to implement [https://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.91.3579&rep=rep1&type=pdf I/O models used in earlier versions] of Haskell:
   
 
* dialogues:
 
* dialogues:
Line 410: Line 195:
   
 
respond :: Request -> OI -> Response
 
respond :: Request -> OI -> Response
respond Getq u = let !c = getChar' u in Getp c
+
respond Getq u = let !c = getChar u in Getp c
respond (Putq c) u = let !_ = putChar' c u in Putp
+
respond (Putq c) u = let !_ = putChar c u in Putp
   
 
data Request = Getq | Putq Char
 
data Request = Getq | Putq Char
Line 422: Line 207:
 
type Answer = OI -> ()
 
type Answer = OI -> ()
   
runK :: Answer -> IO -> ()
+
runK :: Answer -> OI -> ()
 
runK a u = a u
 
runK a u = a u
   
Line 430: Line 215:
 
getcharK :: (Char -> Answer) -> Answer
 
getcharK :: (Char -> Answer) -> Answer
 
getcharK k = \ u -> let !(u1, u2) = partOI u in
 
getcharK k = \ u -> let !(u1, u2) = partOI u in
let !c = getChar' u1 in
+
let !c = getChar u1 in
 
let !a = k c in
 
let !a = k c in
 
a u2
 
a u2
Line 436: Line 221:
 
putcharK :: Char -> Answer -> Answer
 
putcharK :: Char -> Answer -> Answer
 
putcharK c a = \ u -> let !(u1, u2) = partOI u in
 
putcharK c a = \ u -> let !(u1, u2) = partOI u in
let !_ = putChar' c u1 in
+
let !_ = putChar c u1 in
 
a u2
 
a u2
 
</haskell>
 
</haskell>
   
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://www.researchgate.net/publication/220997216_Controlling_chaos_on_safe_side-effects_in_data-parallel_operations 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:
+
...and even <i>that</i> <s><i>world</i></s> state-passing style used in GHC, 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>
Line 447: Line 232:
 
getcharL :: World -> (Char, World)
 
getcharL :: World -> (Char, World)
 
getcharL (W u) = let !(u1, u2) = partOI u in
 
getcharL (W u) = let !(u1, u2) = partOI u in
let !c = getChar' u1 in
+
let !c = getChar u1 in
 
(c, W u2)
 
(c, W u2)
   
 
putcharL :: Char -> World -> World
 
putcharL :: Char -> World -> World
 
putcharL c (W u) = let !(u1, u2) = partOI u in
 
putcharL c (W u) = let !(u1, u2) = partOI u in
let !_ = putChar' u1 in
+
let !_ = putChar u1 in
 
W u2
 
W u2
 
</haskell>
 
</haskell>
  +
<sup> </sup>
   
 
----
 
----
Line 462: Line 248:
 
* [[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]]
* [https://pqnelson.github.io/2021/07/29/monadic-io-in-ml.html Monadic IO in Standard ML]
 

Revision as of 19:38, 16 December 2022

A purely functional program implements a function; it has no side effect. [...] if the side effect can’t be in the functional program, it will have to be outside it.

Tackling the Awkward Squad: monadic input/output, concurrency, exceptions, and foreign-language calls in Haskell, Simon Peyton Jones (pages 3-4 of 60).

One technique has been used for similar tasks:

This is discussed by Burton, and is built on by Harrison. The effect of this proposal is to place the non-determinism entirely outside the software [...]

Functional Programming and Operating Systems, Simon B. Jones and A. F. Sinclair (page 10 of 13).

It can also be used to provide access to external resources:

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.

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

Perhaps it can be used for I/O...


Details, details

How does it work?

[...] supply each program with an extra argument consisting of an infinite (lazy) binary tree of values. (We choose a tree [...] since any number of subtrees may be extracted from an infinite tree). In practice, these values will be determined at run time (when used as arguments to a special function [...]), but once fixed will never change.

...“a special function”: only one? More will definitely be needed! To keep matters simple, each value shall only be used once (if at all) as an argument to any such function.

main' :: Tree Exterior -> ...

 -- section 2
data Tree a = Node { contents :: a,
                     left     :: Tree a,
                     right    :: Tree a }

data Exterior                      -- the abstract value type
getchar :: Exterior -> Char        -- the special functions
putchar :: Char -> Exterior -> ()  -- (add more as needed :-)

Avoiding gratuitous repetition:

type OI  =  Tree Exterior

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

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

An alternative abstraction

About those trees: are they really necessary? If OI was an abstract data type, the use of trees could at least be confined to the implementation:

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

...provided that single-use property applies directly to OI values (thereby deeming “special” any function which uses an OI argument). That includes the initial OI value supplied to each program:

main' :: OI -> ...

But most Haskell programs will need more:

part    :: OI -> (OI, OI)
part t  =  (left t, right t)

...than two OI values:

parts   :: OI -> [OI]
parts t =  let (t1, t2) = part t in t1 : parts t2

So OI can be a tree-free abstract data type after all:

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


Other interfaces

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

The OI interface can also be used to implement I/O models 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 -> OI -> ()
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 used in GHC, 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