Difference between revisions of "Output/Input"
m |
m |
||
(10 intermediate revisions by the same user not shown) | |||
Line 1: | Line 1: | ||
+ | Regarding <code>IO a</code>, Haskell's monadic I/O type: |
||
− | [[Category:Theoretical foundations]] |
||
+ | <blockquote> |
||
− | === <u>Clearing away the smoke and mirrors</u> === |
||
+ | Some operations are primitive actions, |
||
+ | corresponding to conventional I/O operations. Special operations (methods in the class <code>Monad</code>, see Section 6.3.6) |
||
+ | sequentially compose actions, corresponding to sequencing operators (such as the semicolon) in imperative |
||
+ | languages. |
||
+ | :<small>[https://www.haskell.org/definition/haskell2010.pdf The Haskell 2010 Report], (page 107 of 329).</small> |
||
− | <div style="border-left:1px solid lightgray; padding: 1em" alt="blockquote"> |
||
+ | </blockquote> |
||
− | The implementation in GHC uses the following one: |
||
+ | So for I/O, the monadic interface merely provides [[Monad tutorials timeline|an abstract way]] to sequence its actions. However there is another, more direct approach to sequencing: |
||
− | <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> |
||
− | </div> |
||
− | |||
− | ...so what starts out as an I/O action of type: |
||
<haskell> |
<haskell> |
||
+ | Control.Parallel.pseq :: a -> b -> b |
||
− | World -> (a, World) |
||
</haskell> |
</haskell> |
||
+ | (as opposed to the [[seq|<b>non</b>]]-sequential <code>Prelude.seq</code>.) That means a more direct way of preserving [[Referential transparency|referential transparency]] is also needed. For simple teletype I/O: |
||
− | is changed by GHC to approximately: |
||
<haskell> |
<haskell> |
||
+ | data OI |
||
− | () -> (a, ()) |
||
+ | partOI :: OI -> (OI, OI) |
||
+ | getChar :: OI -> Char |
||
+ | putChar :: Char -> OI -> () |
||
</haskell> |
</haskell> |
||
+ | where: |
||
− | ...because <i>"logically"</i> a function in Haskell has no observable effects - being exact requires a change of notation: |
||
+ | * <code>OI</code> isn't an ordinary Haskell type - ordinary Haskell types represent values without (externally-visible) side-effects, hence <code>OI</code> being abstract. |
||
− | <haskell> |
||
− | () --> (a, ()) |
||
− | </haskell> |
||
− | The < |
+ | * The action <code>partOI</code> is needed because each <code>OI</code> value can only be used once. |
+ | * The action <code>getChar</code> obtains the the next character of input. |
||
− | <haskell> |
||
− | () --> a |
||
− | </haskell> |
||
− | <sup> </sup> |
||
+ | * The function <code>putChar</code> expects a character, and returns an action which will output the given character. |
||
− | ---- |
||
− | === <u>Previously seen</u> === |
||
+ | <br> |
||
− | Variants of <code>() --> a</code> have appeared elsewhere - examples include: |
||
+ | Now for a few other I/O interfaces - if <code>seq</code> was actually sequential: |
||
− | * 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"> |
||
+ | * [[Monad|monad]] |
||
− | 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> |
||
− | <sup> </sup> |
||
− | <haskell> |
||
− | (\ () --> …) :: () --> a |
||
− | </haskell> |
||
− | |} |
||
+ | :<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> |
||
− | |} |
||
− | |||
− | * [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> |
||
− | type T a = () --> a |
||
− | </haskell> |
||
− | |} |
||
− | |||
− | * [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> |
||
− | |} |
||
− | |||
− | ==== 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"> |
||
− | 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> |
||
− | type Obs tau = State -> tau |
||
− | </haskell> |
||
− | |} |
||
− | |||
− | * [https://image.slidesharecdn.com/lazyio-120422092926-phpapp01/95/lazy-io-15-728.jpg page 15] of ''Non-Imperative Functional Programming'' by Nobuo Yamashita: |
||
− | :{| |
||
− | <haskell> |
||
− | type a :-> b = OI a -> b |
||
− | </haskell> |
||
− | |} |
||
− | |||
− | * [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> |
||
− | type Create a = Id -> a |
||
− | </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> |
||
− | |} |
||
− | |||
− | 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> |
||
− | type IO a = OI -> a |
||
− | </haskell> |
||
− | |||
− | 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 |
||
− | |||
− | 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> |
||
− | |||
− | 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> |
||
− | data OI |
||
− | part :: OI -> (OI, OI) |
||
− | getChar' :: OI -> Char |
||
− | putChar' :: Char -> OI -> () |
||
− | </haskell> |
||
− | <sup> </sup> |
||
− | |||
− | ---- |
||
− | === <u>Other interfaces</u> === |
||
− | |||
− | In addition to the [[Monad|current]] one: |
||
− | |||
− | <haskell> |
||
type M a = OI -> a |
type M a = OI -> a |
||
Line 318: | Line 52: | ||
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 338: | Line 76: | ||
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 346: | Line 90: | ||
arr :: (b -> c) -> A b c |
arr :: (b -> c) -> A b c |
||
− | arr 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 353: | Line 97: | ||
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 |
||
− | + | 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> |
||
− | + | The <code>OI</code> interface can also be used to implement [https://web.archive.org/web/20210414160729/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[https://www.haskell.org/definition/haskell-report-1.2.ps.gz <span></span>][https://dl.acm.org/doi/pdf/10.1145/130697.130699 <span></span>]: |
||
− | * dialogues: |
||
:<haskell> |
:<haskell> |
||
Line 371: | Line 126: | ||
respond :: Request -> OI -> Response |
respond :: Request -> OI -> Response |
||
− | respond Getq u = let !c = getChar |
+ | respond Getq u = let !c = getChar u in Getp c |
− | respond (Putq c) u = let !_ = putChar |
+ | respond (Putq c) u = let !_ = putChar c u in Putp |
data Request = Getq | Putq Char |
data Request = Getq | Putq Char |
||
Line 378: | Line 133: | ||
</haskell> |
</haskell> |
||
− | * continuations: |
+ | * [[Continuation|continuations]]: |
:<haskell> |
:<haskell> |
||
type Answer = OI -> () |
type Answer = OI -> () |
||
− | runK :: Answer -> |
+ | runK :: Answer -> OI -> () |
runK a u = a u |
runK a u = a u |
||
Line 391: | Line 146: | ||
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 |
+ | let !c = getChar u1 in |
let !a = k c in |
let !a = k c in |
||
a u2 |
a u2 |
||
Line 397: | Line 152: | ||
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 |
+ | let !_ = putChar c u1 in |
a u2 |
a u2 |
||
</haskell> |
</haskell> |
||
− | and even that <s><i> |
+ | ...and even <i>that</i> <s><i>world</i></s> state-passing style used in GHC, and by [https://web.archive.org/web/20130607204300/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 408: | Line 163: | ||
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 |
+ | 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 |
+ | let !_ = putChar c u1 in |
W u2 |
W u2 |
||
</haskell> |
</haskell> |
||
− | <sup> </sup> |
||
+ | (Rewriting those examples to use <code>pseq</code> is left as an exercise.) |
||
− | ---- |
||
+ | |||
− | === <u>See also</u> === |
||
+ | See also: |
||
* [[Plainly partible]] |
* [[Plainly partible]] |
||
* [[Disposing of dismissives]] |
* [[Disposing of dismissives]] |
||
* [[IO then abstraction]] |
* [[IO then abstraction]] |
||
+ | |||
− | * [https://pqnelson.github.io/2021/07/29/monadic-io-in-ml.html Monadic IO in Standard ML] |
||
+ | [[Category:Theoretical foundations]] |
Latest revision as of 22:02, 16 September 2024
Regarding IO a
, Haskell's monadic I/O type:
Some operations are primitive actions, corresponding to conventional I/O operations. Special operations (methods in the class
Monad
, see Section 6.3.6) sequentially compose actions, corresponding to sequencing operators (such as the semicolon) in imperative languages.
- The Haskell 2010 Report, (page 107 of 329).
So for I/O, the monadic interface merely provides an abstract way to sequence its actions. However there is another, more direct approach to sequencing:
Control.Parallel.pseq :: a -> b -> b
(as opposed to the non-sequential Prelude.seq
.) That means a more direct way of preserving referential transparency is also needed. For simple teletype I/O:
data OI
partOI :: OI -> (OI, OI)
getChar :: OI -> Char
putChar :: Char -> OI -> ()
where:
OI
isn't an ordinary Haskell type - ordinary Haskell types represent values without (externally-visible) side-effects, henceOI
being abstract.
- The action
partOI
is needed because eachOI
value can only be used once.
- The action
getChar
obtains the the next character of input.
- The function
putChar
expects a character, and returns an action which will output the given character.
Now for a few other I/O interfaces - if seq
was actually sequential:
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:
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
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, and 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 c u1 in
W u2
(Rewriting those examples to use pseq
is left as an exercise.)
See also: