Difference between revisions of "Output/Input"
m (Reference replaced) 
m 

(17 intermediate revisions by the same user not shown)  
Line 1:  Line 1:  
+  <div style="borderleft:1px solid lightgray; padding: 1em" alt="blockquote"> 

−  [[Category:Theoretical foundations]] 

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

+  <small>[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 foreignlanguage calls in Haskell], Simon Peyton Jones (pages 34 of 60). </small> 

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

+  </div> 

+  
+  One technique has been used for similar tasks: 

<div style="borderleft:1px solid lightgray; padding: 1em" alt="blockquote"> 
<div style="borderleft:1px solid lightgray; padding: 1em" alt="blockquote"> 

+  This is discussed by Burton[https://academic.oup.com/comjnl/articlepdf/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 nondeterminism <i>entirely</i> outside the software [...] 

−  The implementation in GHC uses the following one: 

+  <small>[https://academic.oup.com/comjnl/articlepdf/32/2/162/1445725/320162.pdf Functional Programming and Operating Systems], Simon B. Jones and A. F. Sinclair (page 10 of 13).</small> 

−  <haskell> 

+  </div> 

−  type IO a = World > (a, World) 

−  </haskell> 

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

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

+  <div style="borderleft:1px solid lightgray; padding: 1em" alt="blockquote"> 

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

+  The approach generalizes so that a program can make use of other runtime information such as the current time or current amount of available storage. 

+  
+  <small>[https://academic.oup.com/comjnl/articlepdf/31/3/243/1157325/310243.pdf Nondeterminism with Referential Transparency in Functional Programming Languages], F. Warren Burton (front page).</small> 

</div> 
</div> 

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

−  ...so what starts out as an I/O action of type: 

+  <br> 

+  
+  __TOC__ 

+  <sup> <sup> 

+   

−  <haskell> 

+  === <u>Details, details</u> === 

−  World > (a, World) 

−  </haskell> 

+  How does it work? 

−  is changed by GHC to approximately: 

+  
+  <div style="borderleft:1px solid lightgray; padding: 1em" alt="blockquote"> 

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

+  
+  ...<i>“a special function”</i>: only one? More will definitely be needed! To keep matters [https://www.interactiondesign.org/literature/article/kisskeepitsimplestupidadesignprinciple simple], each value shall only be used <b>once</b> (if at all) as an argument to any such function. 

<haskell> 
<haskell> 

+  main' :: Tree Exterior > ... 

−  () > (a, ()) 

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

</haskell> 
</haskell> 

+  Avoiding gratuitous repetition: 

−  As the returned unitvalue <code>()</code> contains no useful information, that type can be simplified further: 

<haskell> 
<haskell> 

+  type OI = Tree Exterior 

−  () > a 

−  </haskell> 

+  getChar' :: OI > Char 

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

+  getChar' = getchar . contents 

+  putChar' :: Char > OI > () 

−   

+  putChar' c = putchar c . contents 

−  === <u>Previously seen</u> === 

+  </haskell> 

+  <sup> </sup> 

+  ==== An alternative abstraction ==== 

−  The type <code>() > a</code> (or variations of it) have appeared elsewhere  examples include: 

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

−  * page 2 of 13 in [https://fi.ort.edu.uy/innovaportal/file/20124/1/22landin_correspondencebetweenalgol60andchurchslambdanotation.pdf A Correspondence Between ALGOL 60 and Church's LambdaNotation: Part I] by Peter Landin: 

−  :{ 

−  <div style="borderleft: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 argumentlist of length zero is called a ''noneadic'' function. 

−  </div> 

−  <sup> </sup> 

<haskell> 
<haskell> 

+  data OI 

−  (\ () > …) :: () > a 

+  getChar' :: OI > Char 

+  putChar' :: Char > OI > () 

</haskell> 
</haskell> 

−  } 

+  ...provided that singleuse 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: 

−  * page 148 of 168 in [https://web.archive.org/web/20021107080915/https://www.cl.cam.ac.uk/techreports/UCAMCLTR285.pdf Functional programming and Input/Output] by Andrew Gordon: 

−  :{ 

−  <div style="borderleft: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="borderleft: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' :: OI > ... 

</haskell> 
</haskell> 

−  } 

+  But most Haskell programs will need more: 

−  * [https://image.slidesharecdn.com/lazyio120422092926phpapp01/95/lazyio15728.jpg page 15] of ''NonImperative Functional Programming'' by Nobuo Yamashita: 

−  :{ 

<haskell> 
<haskell> 

−  +  part :: OI > (OI, OI) 

+  part t = (left t, right t) 

</haskell> 
</haskell> 

−  } 

+  ...than two <code>OI</code> values: 

−  * [http://h2.jaguarpaw.co.uk/posts/mtlstyleforfree MTL style for free] by Tom Ellis: 

−  :{ 

<haskell> 
<haskell> 

+  parts :: OI > [OI] 

−  data Time_ a = GetCurrentTime (UTCTime > a) 

+  parts t = let (t1, t2) = part t in t1 : parts t2 

</haskell> 
</haskell> 

−  } 

+  So <code>OI</code> can be a treefree abstract data type after all: 

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

−  :{ 

<haskell> 
<haskell> 

−  data 
+  data OI 
+  partOI :: OI > (OI, OI) 

+  getChar :: OI > Char 

+  putChar :: Char > OI > () 

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

−  :{ 

−  <div style="borderleft: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> 
<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: 

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

−  :{ 

−  <div style="borderleft: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> 

−  } 

+  * [[Monadmonad]] 

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

−  :{ 

−  <div style="borderleft:1px solid lightgray; padding: 1em" alt="blockquote"> 

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

−  } 

+  :<haskell> 

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

+  type M a = OI > a 

−  :{ 

−  <div style="borderleft: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> 

−  } 

+  unit :: a > M a 

−  * [http://comonad.com/reader/2011/freemonadsforless3 Free Monads for Less (Part 3 of 3): Yielding IO] by Edward Kmett: 

+  unit x = \ u > let !_ = partOI u in x 

−  :{ 

−  <div style="borderleft: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> 

−  } 

+  bind :: M a > (a > M b) > M b 

−  * page 27 of [https://blog.higherorder.com/assets/scalaio.pdf Purely Functional I/O in Scala] by Rúnar Bjarnason: 

+  bind m k = \ u > let !(u1, u2) = partOI u in 

−  :{ 

+  let !x = m u1 in 

−  <div style="borderleft:1px solid lightgray; padding: 1em" alt="blockquote"> 

+  let !y = k x u2 in 

−  <pre> 

+  y 

−  class IO[A](run: () => A) 

−  </pre> 

−  </div> 

−  <sup> </sup> 

−  <haskell> 

−  class Io a where run :: () > a 

−  </haskell> 

−  } 

+  getcharM :: M Char 

−  * [http://www.fssnip.net/6i/title/TinyIOMonad igeta's snippet]: 

+  getcharM = getChar 

−  :{ 

−  <div style="borderleft: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> 

−  } 

+  putcharM :: Char > M () 

−  * [https://stackoverflow.com/questions/6647852/haskellactualiomonadimplementationindifferentlanguage/6706442#6706442 ysdx's answer] to [https://stackoverflow.com/questions/6647852/haskellactualiomonadimplementationindifferentlanguage this SO question]: 

+  putcharM = putChar 

−  :{ 

−  <div style="borderleft: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> 
</haskell> 

−  } 

+  * [[Comonadcomonad]]: 

−  * [https://stackoverflow.com/questions/45136398/isthemonadicioconstructinhaskelljustaconvention/45141523#45141523 luqui's answer] to [https://stackoverflow.com/questions/45136398/isthemonadicioconstructinhaskelljustaconvention this SO question]: 

−  :{ 

−  <haskell> 

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

−  </haskell> 

−  } 

+  :<haskell> 

−  * [https://stackoverflow.com/questions/15418075/thereadermonad/15419592#15419592 luqui's answer] to [https://stackoverflow.com/questions/15418075/thereadermonad this SO question]: 

+  type C a = (OI, a) 

−  :{ 

−  <haskell> 

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

−  </haskell> 

−  } 

+  extract :: C a > a 

−  * [https://stackoverflow.com/questions/51770808/howexactlydoesiosworkunderthehood/51772273#51772273 chi's answer] to [https://stackoverflow.com/questions/51770808/howexactlydoesiosworkunderthehood this SO question]: 

+  extract (u, x) = let !_ = partOI u in x 

−  :{ 

−  <div style="borderleft: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> 

−  } 

+  duplicate :: C a > C (C a) 

−  * [https://luxlang.blogspot.com/2016/01/monadsioandconcurrencyinlux.html Monads, I/O and Concurrency in Lux] by Eduardo Julián: 

+  duplicate (u, x) = let !(u1, u2) = partOI u in 

−  :{ 

+  (u2, (u1, x)) 

−  <div style="borderleft: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> 

−  } 

+  extend :: (C a > b) > C a > C b 

−  * [https://mperry.github.io/2014/01/03/referentiallytransparentio.html Referentially Transparent Input/Output in Groovy] by Mark Perry: 

+  extend h (u, x) = let !(u1, u2) = partOI u in 

−  :{ 

+  let !y = h (u1, x) in 

−  <div style="borderleft:1px solid lightgray; padding: 1em" alt="blockquote"> 

+  (u2, y) 

−  <pre> 

−  abstract class SimpleIO<A> { 

−  abstract A run() 

−  } 

−  </pre> 

−  </div> 

−  <sup> </sup> 

−  <haskell> 

−  class SimpleIO a where 

−  run :: () > a 

−  </haskell> 

−  } 

+  getcharC :: C () > Char 

−  * [https://github.com/phpfp/phpfpio#readme The <code>IO</code> Monad for PHP] by Tom Harding: 

+  getcharC (u, ()) = getChar u 

−  :{ 

−  <div style="borderleft:1px solid lightgray; padding: 1em" alt="blockquote"> 

−  <pre> 

−  __construct :: (> a) > IO a 

−  </pre> 

−  [...] The parameter to the constructor must be a zeroparameter [noneadic] function that returns a value. 

−  </div> 

−  <sup> </sup> 

−  <haskell> 

−  data IO a = IO (() > a) 

−  __construct :: (() > a) > IO a 

−  __construct = IO 

−  </haskell> 

−  } 

+  putcharC :: C Char > () 

−  * [https://medium.com/@luijar/theobservabledisguisedasaniomonadc89042aa8f31 The Observable disguised as an IO Monad] by Luis Atencio: 

+  putcharC (u, c) = putChar c u 

−  :{ 

−  <div style="borderleft: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/categorytheoryviacsharp18moremonadiomonad More Monad: <code>IO<></code> Monad], from [https://weblogs.asp.net/dixin/Tags/Category%20Theory dixin's Category Theory via C#] series: 

−  :{ 

−  <div style="borderleft: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> 
</haskell> 

−  } 

+  * [[Arrowarrow]]: 

−  * [https://discuss.ocaml.org/t/iomonadforocaml/4618/11 ivg's post] in [https://discuss.ocaml.org/t/iomonadforocaml/4618 <code>IO</code> Monad for OCaml] 

−  :{ 

−  <div style="borderleft: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> 

−  } 

+  :<haskell> 

−  * [https://arrowkt.io/docs/effects/io Why <code>suspend</code> over <code>IO</code>] in [https://arrowkt.io/docs/fx Arrow Fx]: 

+  type A b c = (OI > b) > (OI > c) 

−  :{ 

−  <div style="borderleft:1px solid lightgray; padding: 1em" alt="blockquote"> 

−  [...] So <code>suspend () > A</code> offers us the exact same guarantees as <code>IO<A></code>. 

−  </div> 

−  } 

+  arr :: (b > c) > A b c 

−  Of these, it is the [https://hackage.haskell.org/package/oi/docs/src/DataOIInternal.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 singleuse property also appears in the implementation of the abstract <code>decision</code> type described by F. Warren Burton in [https://academic.oup.com/comjnl/articlepdf/31/3/243/1157325/310243.pdf Nondeterminism with Referential Transparency in Functional Programming Languages]. 

+  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 

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

+  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 

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

+  getcharA = \ c' u > let !(u1, u2) = partOI u in 

+  let !_ = c' u1 in 

+  let !ch = getChar u2 in 

+  ch 

+  putcharA :: A Char () 

−  <haskell> 

+  putcharA = \ c' u > let !(u1, u2) = partOI u in 

−  type IO a = OI > a 

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

−  Using Burton's ''pseudodata'' approach: 

+  * dialogues: 

−  <haskell> 

−   abstract; singleuse I/Oaccess mediator 

−  data Exterior 

−  getchar :: Exterior > Char 

−  putchar :: Char > Exterior > () 

+  :<haskell> 

−   from section 2 of Burton's paper 

+  runD :: ([Response] > [Request]) > OI > () 

−  data Tree a = Node { contents :: a, 

−  +  runD d u = foldr (\ (!_) > id) () $ yet $ \ l > zipWith respond (d l) (partsOI u) 

−  right :: Tree a } 

+  yet :: (a > a) > a 

−   utility definitions 

−  +  yet f = f (yet f) 

−  +  respond :: Request > OI > Response 

+  respond Getq u = let !c = getChar u in Getp c 

−  getChar' = getchar . contents 

+  respond (Putq c) u = let !_ = putChar c u in Putp 

+  data Request = Getq  Putq Char 

−  putChar' :: Char > OI > () 

+  data Response = Getp Char  Putp 

−  putChar' c = putchar c . contents 

+  </haskell> 

+  
+  * continuations: 

+  
+  :<haskell> 

+  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 

−  parts :: OI > [OI] 

+  let !c = getChar u1 in 

+  let !a = k c in 

+  a u2 

+  putcharK :: Char > Answer > Answer 

−  part t = (left t, right t) 

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

−  +  let !_ = putChar c u1 in 

+  a u2 

</haskell> 
</haskell> 

+  ...and even <i>that</i> <s><i>world</i></s> statepassing 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 SingleAssignment 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: 

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

+  newtype World = W OI 

−  data OI 

+  
−  part :: OI > (OI, OI) 

−  +  getcharL :: World > (Char, World) 

+  getcharL (W u) = let !(u1, u2) = partOI u in 

−  putChar' :: Char > OI > () 

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

−  * [https://pqnelson.github.io/2021/07/29/monadicioinml.html Monadic IO in Standard ML] 

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

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

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

+  [[Category:Theoretical foundations]] 
Latest revision as of 07:59, 12 June 2023
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 foreignlanguage calls in Haskell, Simon Peyton Jones (pages 34 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 nondeterminism 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 runtime 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 singleuse 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 treefree 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 statepassing style used in GHC, which is also used by Clean, SingleAssignment 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
^{ }