From HaskellWiki
Semantics of IO: A Continuation Approach
The following is inspired by
Luke Palmer's post. This only describes one possible semantics of
; your actually implementation may vary.
The idea is to define
as
data IO a = Done a
| PutChar Char (IO a)
| GetChar (Char -> IO a)
For simplicity this an example of
that only gives semantics for teletype IO.
Think of
as a tree whose leaves are
that holds the result of the program.
is a node that has one child tree and the node holds one character of data.
is a node that has many children; it has one child for every
, but
holds no data itself.
This tree contains all the information needed to execute teletype interactions.
One interprets (or executes) an
by tracing a route from root of the tree to a leaf.
If a
node 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 evaluated in order to determine what character should be displayed before continuing. If a
node is encountered, a character is read from the terminal (blocking if necessary) and the subtree corresponding to the character received is executed. If
is encountered the program ends.
holds the result of the computation, but in the case of
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
is just another name for
. The bind operation takes a tree
and a function
and replaces the
nodes (the leaves) of
by a new tree produce by applying
to the data held in the
nodes.
The primitive IO commands are defined using these constructors.
putChar :: Char -> IO ()
putChar x = PutChar x (Done ())
getChar :: IO Char
getChar = GetChar (\c -> Done c)
The function
builds a small
tree that contains one
node holding the character data followed by
.
The function
builds a short
tree that begins with a
that holds one
node holding every character.
Other teletype commands can be defined in terms of these primitives
putStr :: String -> IO ()
putStr = mapM_ putChar
More generally speaking,
will represent the desired interaction with the operating system. For every system call there will be a corresponding constructor in
of the form
| SysCallName p1 p2 ... pn (r -> IO a)
where
...
are the parameters for the system call, and
is the result of the system call. (Thus
and
will not occur as constructors of
if they don't correspond to system calls)
Category: Theoretical foundations
