Output/Input

Clearing away the smoke and mirrors

The implementation in GHC uses the following one:

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

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

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

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

World -> (a, World)

is changed by GHC to approximately:

() -> (a, ())

...because "logically" a function in Haskell has no observable effects - being exact requires a change of notation:

() --> (a, ())

The "result" (of type a) can then be "returned" directly:

() --> a

---

Previously seen

Variants of () --> a have appeared elsewhere - examples include:

• page 2 of 13 in A Correspondence Between ALGOL 60 and Church's Lambda-Notation: Part I by Peter Landin:

The use of λ, and in particular (to avoid an irrelevant bound variable) of λ() , 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. (\ () --> …) :: () --> a

• page 27 of Purely Functional I/O in Scala by Rúnar Bjarnason:

class IO[A](run: () => A) class Io a where run :: () --> a

• igeta's snippet:

type IO<'T> = private | Action of (unit -> 'T) data IO t = Action (() --> t)

• ysdx's answer to this SO question:

Let's say you want to implement IO in SML : structure Io : MONAD = struct type 'a t = unit -> 'a ⋮ end type T a = () --> a

• Monads, I/O and Concurrency in Lux by Eduardo Julián:

(deftype #export (IO a) (-> Void a)) type IO a = (-->) Void a

• Referentially Transparent Input/Output in Groovy by Mark Perry:

abstract class SimpleIO<A> { abstract A run() } class SimpleIO a where run :: () --> a

• The IO Monad for PHP by Tom Harding:

__construct :: (-> a) -> IO a [...] The parameter to the constructor must be a zero-parameter [none-adic] function that returns a value. data IO a = IO (() --> a) __construct :: (() --> a) -> IO a __construct = IO

• The Observable disguised as an IO Monad by Luis Atencio:

IO is a very simple monad that implements a slightly modified version of our abstract interface with the difference that instead of wrapping a value a, it wraps a side effect function () -> a. data IO a = Wrap (() --> a)

• More Monad: IO<> Monad, from dixin's Category Theory via C# series:

The definition of IO<> is simple: public delegate T IO<out T>(); [...] IO<T> is used to represent a impure function. When a IO<T> function is applied, it returns a T value, with side effects. type IO t = () --> t

• ivg's post in IO Monad for OCaml

So let’s implement the IO Monad right now and here. Given that OCaml is strict and that the order of function applications imposes the order of evaluation, the IO Monad is just a thunk, e.g., type 'a io = unit -> 'a type Io a = () --> a

• Why suspend over IO in Arrow Fx:

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

Avoiding alternate annotations

Having to deal with both -> and --> is annoying - another option is to use a different argument type, instead of ():

• page 3 of Assignments for Applicative Languages by Vipin Swarup, Uday S. Reddy and Evan Ireland:

A value of type Obs 𝜏 is called an observer. Such a value observes (i.e. views or inspects) a state and returns a value of type 𝜏. [...] An observer type Obs 𝜏 may be viewed as an implicit function space from the set of states to the type 𝜏. type Obs tau = State -> tau

• page 15 of Non-Imperative Functional Programming by Nobuo Yamashita:

type a :-> b = OI a -> b

• MTL style for free by Tom Ellis:

data Time_ a = GetCurrentTime (UTCTime -> a)

• page 2 of Unique Identifiers in Pure Functional Languages by Péter Diviánszky:

[...] The type Id can be hidden by the synonym data type :: Create a :== Id -> a type Create a = Id -> a

• page 7 of Functional Reactive Animation by Conal Elliott and Paul Hudak:

An early implementation of Fran represented behaviors as implied in the formal semantics: data Behavior a = Behavior (Time -> a)

Of these, it is the implementation of OI a in Yamashita's 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 decision type described by F. Warren Burton in Nondeterminism with Referential Transparency in Functional Programming Languages.

---

IO, redefined

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

type IO a = OI -> a

Using Burton's pseudodata 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

Of course, in an actual implementation OI would be abstract like World, and for similar reasons. This permits a simpler implementation for OI and its values, instead of being based on (theoretically) infinite structured values like binary trees. That simplicity has benefits for the OI interface, in this case:

data OI
part :: OI -> (OI, OI)
getChar' :: OI -> Char
putChar' :: Char -> OI -> ()

---

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

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)

• arrow:

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

arr          :: (b -> c) -> A b c
arr f        =  \ c' u -> f $! c' u

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

unit         :: a -> OI -> a
unit x u     = let !_ = partOI u in x

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 pass-the-planet state-based 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
• The IO monad in 1965
• Monadic IO in Standard ML