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 to to define
as
newtype IO a = IO {runIO :: (a -> IOTree) -> IOTree}
This is equivalent to defining
as
from the
monad template library. The monad functions for
are derived from the monad functions for
.
return x = IO (\k -> k x)
x >>= f = IO (\k -> runIO x (\a -> runIO (f a) (\b -> k b)))
is the ultimate result of a program. For simplicity we will give an example of
that gives semantics for teletype IO.
data IOTree = Done
| PutChar Char IOTree
| GetChar (Char -> IOTree)
(This is a tree because the
node has one subtree for every character)
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 only at this point that Haskell code is ever necessarily 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.
The primitive IO commands are defined using these constructors.
putChar :: Char -> IO ()
putChar x = IO (\k -> PutChar x (k ()))
getChar :: IO Char
getChar = IO (\k -> GetChar (\x -> k x))
If the
constructor was defined (isomorphically) as
| PutChar Char (() -> IOTree)
Then the primitive IO commands could be defined directly in terms of these constructors:
putChar :: Char -> IO ()
putChar = IO . PutChar
getChar :: IO Char
getChar = IO GetChar
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 -> IOTree)
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)
We said that the ultimate result of a program is an
, however the main function has type
. This is isomorphic to
, or equivalently
which is not right.
The simple solution to this is that the runtime system produces an
from main by evaluating
runIO main (\() -> Done) :: IOTree
. Here
represents the "rest of the program", which in this case is nothing.
The sophisticated solution to this problem is that
is passed to the operating system which will bind the next program (perhaps a shell) to
. Thus the semantics of our Haskell program becomes embedded into the semantics of the entire operating system run.
The type for
that we have given contains invalid programs such as
IO (\k -> filterTree (not . isPutChar) k ()) :: IO ()
which would remove the output of any future
commands. However, none of these illegal programs can be generated from the monadic interface and the primitive operations provided.
Category: Theoretical foundations
