IO: A Free Approach
The following is inspired by Luke Palmer's post on the topic. This only describes one possible semantics of
IO a; your actual implementation may vary.
The idea is to define
data IO a = Done a | PutChar Char (IO a) | GetChar (Char -> IO a)
For simplicity, this an example of
IO that only gives semantics for teletype I/O.
IO a as a tree whose leaves are
Done a that holds the result of the program:
PutCharis a node that has one child tree and the node holds one character of data.
GetCharis a node that has many children; it has one child for every
GetCharholds no data itself.
This tree contains all the information needed to execute teletype interactions. One interprets (or executes) an
IO a by tracing a route from root of the tree to a leaf:
- If a
PutCharnode is encountered, the character data contained at that node is output to the terminal and then its subtree is executed. It is at this point that Haskell code is evaluated in order to determine what character should be displayed before continuing.
- If a
GetCharnode is encountered, a character is read from the terminal (blocking if necessary) and the subtree corresponding to the character received is executed.
Doneis encountered, the program ends.
Done holds the result of the computation, but in the case of
Main.main :: IO () the data is of type
() and thus contains no information and is ignored.
This execution is not done anywhere in a Haskell program, rather it is done by the run-time system.
The monadic operations are defined as follows:
return :: a -> IO a return x = Done x (>>=) :: IO a -> (a -> IO b) -> IO b Done x >>= f = f x PutChar c x >>= f = PutChar c (x >>= f) GetChar g >>= f = GetChar (\c -> g c >>= f)
As you can see
return is just another name for
Done. The bind operation
(>>=) takes a tree
x and a function
f and replaces the
Done nodes (the leaves) of
x by a new tree produced by applying
f to the data held in the
The primitive I/O commands are defined using these constructors.
putChar :: Char -> IO () putChar x = PutChar x (Done ()) getChar :: IO Char getChar = GetChar (\c -> Done c)
- The function
putCharbuilds a small
IO ()tree that contains one
PutCharnode holding the character data followed by
- The function
getCharbuilds a short
IO Chartree that begins with a
GetCharnode that holds one
Donenode for every character.
Other teletype commands can be defined in terms of these primitives:
putStr :: String -> IO () putStr = mapM_ putChar
More generally speaking,
IO a will represent the desired interaction with the operating system. For every system call there will be a corresponding I/O-tree constructor of the form:
| SysCallName p1 p2 ... pn (r -> IO a)
pn are the parameters for the system call, and
r is the result of the system call. (Thus
GetChar will not occur as constructors for I/O trees if they don't correspond to system calls).
- Wouter Swierstra, Thorsten Altenkirch (2007).
- Levent Erkök, John Launchbury, Andrew Moran. In Fixed Points in Computer Science Workshop, FICS'01 (2001).
- Tackling the awkward squad: monadic input/output, concurrency, exceptions, and foreign-language calls in Haskell
- Simon Peyton Jones. In "Engineering theories of software construction", ed. Tony Hoare, Manfred Broy, Ralf Steinbruggen, IOS Press, ISBN 1 58603 1724, 2001, pages 47-96.
- Roy L. Crole, Andrew D. Gordon. Mathematical Structures in Computer Science 9(2): 125-158 (1999).
- Andrew Gordon. In International Workshop on Computer Science Logic, January 1995. Springer Berlin Heidelberg.
- Andrew Gordon. In FPCA '93: Conference on Functional Programming Languages and Computer Architecture, Copenhagen, June 1993. ACM Press.
- Andrew Gordon. Cambridge University Press. Revision of 1992 PhD dissertation.