Difference between revisions of "Output/Input"

From HaskellWiki
Jump to navigation Jump to search
m (Extra example added)
m
 
(26 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>
 
<haskell>
  +
Control.Parallel.pseq :: a -> b -> b
type IO a = 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:
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>
  +
data OI
World -> (a, World)
 
  +
partOI :: OI -> (OI, OI)
  +
getChar :: OI -> Char
  +
putChar :: Char -> OI -> ()
 
</haskell>
 
</haskell>
   
  +
where:
is changed by GHC to approximately:
 
   
  +
* <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>
 
   
As the returned unit-value <code>()</code> contains no useful information, that type can be simplified further:
+
* 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>
 
   
  +
* The function <code>putChar</code> expects a character, and returns an action which will output the given character.
<sub>Why "approximately"? Because "logically" a function in Haskell has no observable effects.</sub>
 
   
  +
<br>
----
 
=== <u>Previously seen</u> ===
 
   
  +
Now for a few other I/O interfaces - if <code>seq</code> was actually sequential:
The type <code>() -> a</code> (or variations of it) have appeared elsewhere - examples include:
 
   
  +
* [[Monad|monad]]
* 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:
 
:{|
 
|<div style="border-left:1px solid lightgray; padding: 1em" alt="blockquote">
 
   
  +
:<haskell>
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.
 
  +
type M a = OI -> a
</div>
 
<sup> </sup>
 
<haskell>
 
(\ () -> …) :: () -> a
 
</haskell>
 
|}
 
   
  +
unit :: a -> M a
* page 148 of 168 in [[IO Semantics|Functional programming and Input/Output]] by Andrew Gordon:
 
  +
unit x = \ u -> let !_ = partOI u in x
:{|
 
|<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>
 
|}
 
   
  +
bind :: M a -> (a -> M b) -> M b
* 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:
 
  +
bind m k = \ u -> let !(u1, u2) = partOI u in
:{|
 
  +
let !x = m u1 in
|<div style="border-left:1px solid lightgray; padding: 1em" alt="blockquote">
 
  +
let !y = k x u2 in
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>.
 
  +
y
</div>
 
<sup> </sup>
 
<haskell>
 
type Obs tau = State -> tau
 
</haskell>
 
|}
 
   
  +
getcharM :: M Char
* [https://image.slidesharecdn.com/lazyio-120422092926-phpapp01/95/lazy-io-15-728.jpg page 15] of ''Non-Imperative Functional Programming'' by Nobuo Yamashita:
 
  +
getcharM = getChar
   
  +
putcharM :: Char -> M ()
:{|
 
  +
putcharM = putChar
<haskell>
 
type a :-> b = OI a -> b
 
 
</haskell>
 
</haskell>
|}
 
   
  +
* [[Comonad|comonad]]:
* [http://h2.jaguarpaw.co.uk/posts/mtl-style-for-free MTL style for free] by Tom Ellis:
 
   
  +
:<haskell>
:{|
 
  +
type C a = (OI, a)
<haskell>
 
data Time_ a = GetCurrentTime (UTCTime -> a)
 
</haskell>
 
|}
 
   
  +
extract :: C a -> a
* [http://h2.jaguarpaw.co.uk/posts/impure-lazy-language An impure lazy programming language], also by Tom Ellis:
 
  +
extract (u, x) = let !_ = partOI u in x
   
  +
duplicate :: C a -> C (C a)
:{|
 
  +
duplicate (u, x) = let !(u1, u2) = partOI u in
<haskell>
 
data IO a = IO (() -> a)
+
(u2, (u1, x))
</haskell>
 
|}
 
   
  +
extend :: (C a -> b) -> C a -> C b
* 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:
 
  +
extend h (u, x) = let !(u1, u2) = partOI u in
:{|
 
  +
let !y = h (u1, x) in
|<div style="border-left:1px solid lightgray; padding: 1em" alt="blockquote">
 
  +
(u2, y)
[...] 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>
 
|}
 
   
  +
getcharC :: C () -> Char
* 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:
 
  +
getcharC (u, ()) = getChar u
:{|
 
|<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>
 
|}
 
   
  +
putcharC :: C Char -> ()
* 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:
 
  +
putcharC (u, c) = putChar c u
:{|
 
|<div style="border-left: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>
|}
 
   
  +
* [[Arrow|arrow]]:
* The [https://www.vex.net/~trebla/haskell/IO.xhtml Haskell I/O Tutorial] by Albert Lai:
 
:{|
 
|<div style="border-left: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>
 
|}
 
   
  +
:<haskell>
* [http://comonad.com/reader/2011/free-monads-for-less-3 Free Monads for Less (Part 3 of 3): Yielding IO] by Edward Kmett:
 
  +
type A b c = (OI -> b) -> (OI -> c)
:{|
 
|<div style="border-left: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>
 
|}
 
   
  +
arr :: (b -> c) -> A b c
* page 27 of [https://blog.higher-order.com/assets/scalaio.pdf Purely Functional I/O in Scala] by Rúnar Bjarnason:
 
  +
arr f = \ c' u -> let !x = c' u in f x
:{|
 
|<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>
 
|}
 
   
  +
both :: A b c -> A b' c' -> A (b, b') (c, c')
* [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]:
 
  +
f' `both` g' = \ c' u -> let !(u1:u2:u3:_) = partsOI u in
:{|
 
  +
let !(x, x') = c' u1 in
|<div style="border-left:1px solid lightgray; padding: 1em" alt="blockquote">
 
  +
let !y = f' (unit x) u2 in
Let's say you want to implement <code>IO</code> in SML :
 
  +
let !y' = g' (unit x') u3 in
<pre>
 
  +
(y, y')
structure Io : MONAD =
 
  +
where
struct
 
type 'a t = unit -> 'a
+
unit x u = let !_ = partOI u in x
 
end
 
</pre>
 
</div>
 
<sup> </sup>
 
<haskell>
 
type T a = () -> a
 
</haskell>
 
|}
 
   
  +
getcharA :: A () 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]:
 
  +
getcharA = \ c' u -> let !(u1, u2) = partOI u in
:{|
 
  +
let !_ = c' u1 in
|<haskell>
 
  +
let !ch = getChar u2 in
newtype IO a = IO { runIO :: () -> a }
 
  +
ch
</haskell>
 
|}
 
   
  +
putcharA :: A Char ()
* [https://stackoverflow.com/questions/15418075/the-reader-monad/15419592#15419592 luqui's answer] to [https://stackoverflow.com/questions/15418075/the-reader-monad this SO question]:
 
  +
putcharA = \ c' u -> let !(u1, u2) = partOI u in
:{|
 
  +
let !ch = c' u1 in
|<haskell>
 
  +
let !z = putChar ch u2 in
newtype Supply r a = Supply { runSupply :: r -> a }
 
  +
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:
* [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>
 
|}
 
   
  +
* 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>]:
* [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>
 
|}
 
   
  +
:<haskell>
* [https://mperry.github.io/2014/01/03/referentially-transparent-io.html Referentially Transparent Input/Output in Groovy] by Mark Perry:
 
  +
runD :: ([Response] -> [Request]) -> OI -> ()
:{|
 
  +
runD d u = foldr (\ (!_) -> id) () $ yet $ \ l -> zipWith respond (d l) (partsOI u)
|<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>
 
|}
 
   
  +
yet :: (a -> a) -> a
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].
 
  +
yet f = f (yet f)
   
  +
respond :: Request -> OI -> Response
----
 
  +
respond Getq u = let !c = getChar u in Getp c
=== <code>IO</code><u>, redefined</u> ===
 
  +
respond (Putq c) u = let !_ = putChar c u in Putp
   
  +
data Request = Getq | Putq Char
Based on these and other observations, a reasonable distillment of these examples would be <code>OI -> a</code>, which then implies:
 
  +
data Response = Getp Char | Putp
 
<haskell>
 
type IO a = OI -> a
 
 
</haskell>
 
</haskell>
   
  +
* [[Continuation|continuations]]:
Using Burton's ''pseudodata'' approach:
 
   
<haskell>
+
:<haskell>
  +
type Answer = OI -> ()
-- abstract; single-use I/O-access mediator
 
data Exterior
 
getchar :: Exterior -> Char
 
putchar :: Char -> Exterior -> ()
 
   
  +
runK :: Answer -> OI -> ()
-- from section 2 of Burton's paper
 
  +
runK a u = a u
data Tree a = Node { contents :: a,
 
left :: Tree a,
 
right :: Tree a }
 
   
  +
doneK :: Answer
-- utility definitions
 
  +
doneK = \ u -> let !_ = partOI u in ()
type OI = Tree Exterior
 
   
getChar' :: OI -> Char
+
getcharK :: (Char -> Answer) -> Answer
  +
getcharK k = \ u -> let !(u1, u2) = partOI u in
getChar' = getchar . contents
 
  +
let !c = getChar u1 in
  +
let !a = k c in
  +
a u2
   
putChar' :: Char -> OI -> ()
+
putcharK :: Char -> Answer -> Answer
  +
putcharK c a = \ u -> let !(u1, u2) = partOI u in
putChar' c = putchar c . contents
 
  +
let !_ = putChar c u1 in
  +
a u2
  +
</haskell>
   
  +
...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:
part :: OI -> (OI, OI)
 
parts :: OI -> [OI]
 
   
  +
<haskell>
part t = (left t, right t)
 
  +
newtype World = W OI
parts t = let !(t1, t2) = part t in
 
t1 : parts t2
 
</haskell>
 
   
  +
getcharL :: World -> (Char, World)
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:
 
  +
getcharL (W u) = let !(u1, u2) = partOI u in
  +
let !c = getChar u1 in
  +
(c, W u2)
   
  +
putcharL :: Char -> World -> World
<haskell>
 
  +
putcharL c (W u) = let !(u1, u2) = partOI u in
data OI
 
  +
let !_ = putChar c u1 in
part :: OI -> (OI, OI)
 
  +
W u2
getChar' :: OI -> Char
 
putChar' :: Char -> OI -> ()
 
 
</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]]
* [https://pqnelson.github.io/2021/07/29/monadic-io-in-ml.html Monadic IO in Standard ML]
 
 
* [[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]]

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, hence OI being abstract.
  • The action partOI is needed because each OI 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:

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