Personal tools

IO Semantics

From HaskellWiki

(Difference between revisions)
Jump to: navigation, search
m
m
Line 25: Line 25:
If a <hask>PutChar</hask> 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 <hask>GetChar</hask> node is encountered, a character is read from the terminal (blocking if necessary) and the subtree corresponding to the character received is executed. If <hask>Done</hask> is encountered the program ends.
If a <hask>PutChar</hask> 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 <hask>GetChar</hask> node is encountered, a character is read from the terminal (blocking if necessary) and the subtree corresponding to the character received is executed. If <hask>Done</hask> is encountered the program ends.
-
The primitive IO commands are defined using these constructors
+
The primitive IO commands are defined using these constructors.
<haskell>
<haskell>
putChar :: Char -> IO ()
putChar :: Char -> IO ()
Line 33: Line 33:
getChar = IO (\k -> GetChar (\x -> k x))
getChar = IO (\k -> GetChar (\x -> k x))
</haskell>
</haskell>
 +
 +
If the <hask>PutChar</hask> constructor was defined (isomorphically) as
 +
<haskell>
 +
| PutChar Char (() -> IOTree)
 +
</haskell>
 +
 +
Then the primitive IO commands could be defined directly in terms of these constructors:
 +
 +
<haskell>
 +
putChar :: Char -> IO ()
 +
putChar = IO . PutChar
 +
 +
getChar :: IO Char
 +
getChar = IO GetChar
 +
</haskell>
 +
 +
Other teletype commands can be defined in terms of these primitives
Other teletype commands can be defined in terms of these primitives
<haskell>
<haskell>

Revision as of 14:47, 18 July 2008

Semantics of IO: A Continuation Approach

The following is inspired by Luke Palmer's post. This only describes one possible semantics of
IO a
; your actually implementation may vary. The idea to to define
IO
as 
newtype IO a = IO {runIO :: (a -> IOTree) -> IOTree}
This is equivalent to defining
IO
as
Cont IOTree
from the monad template library. The monad functions for
IO
are derived from the monad functions for
Cont
. 
return x = IO (\k -> k x)
x >>= f = IO (\k -> runIO x (\a -> runIO (f a) (\b -> k b)))
IOTree
is the ultimate result of a program. For simplicity we will give an example of
IOTree
that gives semantics for teletype IO. 
data IOTree = Done
            | PutChar Char IOTree
            | GetChar (Char -> IOTree)
(This is a tree because the
GetChar
node has one subtree for every character)
IOTree
contains all the information needed to execute teletype interactions. One interprets (or executes) an
IOTree
by tracing a route from root of the tree to a leaf. If a
PutChar
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
GetChar
node is encountered, a character is read from the terminal (blocking if necessary) and the subtree corresponding to the character received is executed. If
Done
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
PutChar
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,
IOTree
will represent the desired interaction with the operating system. For every system call there will be a corresponding constructor in
IOTree
of the form 
| SysCallName p1 p2 ... pn (r -> IOTree)
where
p1
...
pn
are the parameters for the system call, and
r
is the result of the system call. (Thus
PutChar
and
GetChar
will not occur as constructors of
IOTree
if they don't correspond to system calls) We said that the ultimate result of a program is an
IOTree
, however the main function has type
IO ()
. This is isomorphic to
(() -> IOTree) -> IOTree
, or equivalently
IOTree -> IOTree
which is not right. The simple solution to this is that the runtime system produces an
IOTree
from main by evaluating
runIO main (\() -> Done) :: IOTree
. Here
\() -> Done
represents the "rest of the program", which in this case is nothing. The sophisticated solution to this problem is that
main
is passed to the operating system which will bind the next program (perhaps a shell) to
main
. Thus the semantics of our Haskell program becomes embedded into the semantics of the entire operating system run. The type for
IO a
that we have given contains invalid programs such as 
IO (\k -> filterTree (not . isPutChar) k ()) :: IO ()
which would remove the output of any future
putChar
commands. However, none of these illegal programs can be generated from the monadic interface and the primitive operations provided.
Retrieved from "http://www.haskell.org/haskellwiki/IO_Semantics"

Category: Theoretical foundations