Difference between revisions of "Output/Input"

From HaskellWiki
Jump to navigation Jump to search
(Article rewritten)
m
 
(8 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>
<div style="border-left:1px solid lightgray; padding: 1em" alt="blockquote">
 
  +
Some operations are primitive actions,
There is a world of difference between the value <code>echoML</code> which has no side effects when evaluated, and the computation <code>echoML ()</code>, which does.
 
  +
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.
   
<tt>[https://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.91.3579&rep=rep1&type=pdf How to Declare an Imperative], Philip Wadler (page 25 of 33).</tt>
+
:<small>[https://www.haskell.org/definition/haskell2010.pdf The Haskell 2010 Report], (page 107 of 329).</small>
</div>
+
</blockquote>
   
  +
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:
Of course, that assumes everything in the program's <i>“world”</i> required by <code>echoML</code> actually <b>works as intended</b>: reality isn't always so obliging! To then define Haskell's I/O type as:
 
   
<div style="border-left:1px solid lightgray; padding: 1em" alt="blockquote">
 
 
<haskell>
 
<haskell>
  +
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:
[where an] <code>IO</code> computation is a function that (logically) takes the state of the world, and returns a modified world as well as the return value.
 
 
<tt>[https://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.168.4008&rep=rep1&type=pdf A History of Haskell: Being Lazy With Class], Paul Hudak, John Hughes, Simon Peyton Jones and Philip Wadler.</tt>
 
</div>
 
 
...seems rather optimistic.
 
<sup> </sup>
 
 
----
 
=== <u>The determining of <code>IO</code></u> ===
 
 
Since reality isn't always so deterministic in behaviour, perhaps the study of <i>nondeterminism</i> can provide a more plausible implementation:
 
 
<div style="border-left:1px solid lightgray; padding: 1em" alt="blockquote">
 
We propose to solve this problem [existing constructs for nondeterminism not being compatible with the mathematical foundations of functional programming] by placing the nondeterminism in pseudo-data. A program is passed an infinite tree of two-valued <code>decisions</code>, along with its input. These <code>decisions</code> may be fixed at runtime, thereby permitting nondeterminism. Once fixed, a <code>decision</code> remains unchanged so equivalent expression must always have the same value.
 
 
<tt>[https://academic.oup.com/comjnl/article-pdf/31/3/243/1157325/310243.pdf Nondeterminism with Referential Transparency in Functional Programming Languages], F. Warren Burton (front page).</tt>
 
</div>
 
 
There's more:
 
 
<div style="border-left:1px solid lightgray; padding: 1em" alt="blockquote">
 
The approach generalizes so that a program can make use of other run-time information such as the current time or current amount of available storage.
 
</div>
 
 
Using this <i>pseudo-data</i> approach:
 
   
 
<haskell>
 
<haskell>
  +
data OI
-- abstract; single-use I/O-access mediator
 
  +
partOI :: OI -> (OI, OI)
data Exterior
 
getchar :: Exterior -> Char
+
getChar :: OI -> Char
putchar :: Char -> Exterior -> ()
+
putChar :: Char -> OI -> ()
  +
</haskell>
   
  +
where:
-- from section 2 of Burton's paper
 
data Tree a = Node { contents :: a,
 
left :: Tree a,
 
right :: Tree a }
 
   
  +
* <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.
-- utility definitions
 
type OI = Tree Exterior
 
   
  +
* The action <code>partOI</code> is needed because each <code>OI</code> value can only be used once.
main' :: OI -> ()
 
main' = ...
 
   
  +
* The action <code>getChar</code> obtains the the next character of input.
getChar' :: OI -> Char
 
getChar' = getchar . contents
 
   
  +
* The function <code>putChar</code> expects a character, and returns an action which will output the given character.
putChar' :: Char -> OI -> ()
 
putChar' c = putchar c . contents
 
   
  +
<br>
part :: OI -> (OI, OI)
 
parts :: OI -> [OI]
 
   
  +
Now for a few other I/O interfaces - if <code>seq</code> was actually sequential:
part t = (left t, right t)
 
parts t = let !(t1, t2) = part t in
 
t1 : parts t2
 
</haskell>
 
   
  +
* [[Monad|monad]]
To avoid the visible use of trees, the single-use property can instead be applied directly to <code>OI</code> values. This permits an abstract definition of the <code>OI</code> type:
 
   
<haskell>
+
:<haskell>
data OI
 
partOI :: OI -> (OI, OI)
 
getChar :: OI -> Char
 
putChar :: Char -> OI -> ()
 
</haskell>
 
 
The choice to use (theoretically) infinite structured values (binary trees or otherwise) is then an implementation matter.
 
<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 107: Line 59:
 
putcharM = putChar
 
putcharM = putChar
 
</haskell>
 
</haskell>
 
the <code>OI</code> interface can be used to implement other models of I/O:
 
   
 
* [[Comonad|comonad]]:
 
* [[Comonad|comonad]]:
Line 132: Line 82:
 
putcharC :: C Char -> ()
 
putcharC :: C Char -> ()
 
putcharC (u, c) = putChar c u
 
putcharC (u, c) = putChar c u
 
 
</haskell>
 
</haskell>
   
Line 165: Line 114:
 
</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://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 184: Line 133:
 
</haskell>
 
</haskell>
   
* continuations:
+
* [[Continuation|continuations]]:
   
 
:<haskell>
 
:<haskell>
 
type Answer = OI -> ()
 
type Answer = OI -> ()
   
runK :: Answer -> IO -> ()
+
runK :: Answer -> OI -> ()
 
runK a u = a u
 
runK a u = a u
   
Line 207: Line 156:
 
</haskell>
 
</haskell>
   
and even <i>that</i> <s><i>world</i></s> state-passing style, which is also used by [https://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.17.935&rep=rep1&type=pdf Clean], [https://staff.science.uva.nl/c.u.grelck/publications/HerhSchoGrelDAMP09.pdf Single-Assignment C] and as part of the I/O model used for the verification of interactive programs in [https://cakeml.org/vstte18.pdf CakeML], remembering that <code>OI</code> values can only be used once:
+
...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 219: Line 168:
 
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 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]]
  +
  +
[[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: