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