Output/Input

There is a world of difference between the value echoML which has no side effects when evaluated, and the computation echoML (), which does.

How to Declare an Imperative, Philip Wadler (page 25 of 33).

Of course, that assumes everything in the program's “world” required by echoML actually works as intended: reality isn't always so obliging! To then define Haskell's I/O type as:

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

[where an] IO computation is a function that (logically) takes the state of the world, and returns a modified world as well as the return value.

A History of Haskell: Being Lazy With Class, Paul Hudak, John Hughes, Simon Peyton Jones and Philip Wadler.

...seems rather optimistic.

---

The determining of IO

Since reality isn't always so deterministic in behaviour, perhaps the study of nondeterminism can provide a more plausible implementation:

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 decisions, along with its input. These decisions may be fixed at runtime, thereby permitting nondeterminism. Once fixed, a decision remains unchanged so equivalent expression must always have the same value.

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

There's more:

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.

Using this pseudo-data approach:

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

To avoid the visible use of trees, the single-use property can instead be applied directly to OI values. This permits an abstract definition of the OI type:

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

The choice to use (theoretically) infinite structured values (binary trees or otherwise) is then an implementation matter.

---

Other interfaces

In addition to the current one:

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

the OI interface can be used to implement other models of I/O:

• comonad:

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

• arrow:

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

including those 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 -> IO -> ()
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, 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

• Plainly partible
• Disposing of dismissives
• IO then abstraction