# IO Semantics

### From HaskellWiki

(Difference between revisions)

m |
(rename unIO into runIO) |
||

Line 5: | Line 5: | ||

The idea to to define <hask>IO</hask> as |
The idea to to define <hask>IO</hask> as |
||

<haskell> |
<haskell> |
||

− | newtype IO a = IO {unIO :: (a -> IOTree) -> IOTree} |
+ | newtype IO a = IO {runIO :: (a -> IOTree) -> IOTree} |

</haskell> |
</haskell> |
||

This is equivalent to defining <hask>IO</hask> as <hask>Cont IOTree</hask> from the [[monad template library]]. The monad functions for <hask>IO</hask> are derived from the monad functions for <hask>Cont</hask>. |
This is equivalent to defining <hask>IO</hask> as <hask>Cont IOTree</hask> from the [[monad template library]]. The monad functions for <hask>IO</hask> are derived from the monad functions for <hask>Cont</hask>. |
||

<haskell> |
<haskell> |
||

return x = IO (\k -> k x) |
return x = IO (\k -> k x) |
||

− | x >>= f = IO (\k -> unIO x (\a -> unIO (f a) (\b -> k b))) |
+ | x >>= f = IO (\k -> runIO x (\a -> runIO (f a) (\b -> k b))) |

</haskell> |
</haskell> |
||

<hask>IOTree</hask> is the ultimate result of a program. For simplicity we will give an example of <hask>IOTree</hask> that gives semantics for teletype IO. |
<hask>IOTree</hask> is the ultimate result of a program. For simplicity we will give an example of <hask>IOTree</hask> that gives semantics for teletype IO. |
||

Line 45: | Line 45: | ||

We said that the ultimate result of a program is an <hask>IOTree</hask>, however the main function has type <hask>IO ()</hask>. This is isomorphic to <hask>(() -> IOTree) -> IOTree</hask>, or equivalently <hask>IOTree -> IOTree</hask> which is not right. |
We said that the ultimate result of a program is an <hask>IOTree</hask>, however the main function has type <hask>IO ()</hask>. This is isomorphic to <hask>(() -> IOTree) -> IOTree</hask>, or equivalently <hask>IOTree -> IOTree</hask> which is not right. |
||

− | The simple solution to this is that the runtime system produces an <hask>IOTree</hask> from main by evaluating <hask>unIO main (\() -> Done) :: IOTree</hask>. Here <hask>\() -> Done</hask> represents the "rest of the program", which in this case is nothing. |
+ | The simple solution to this is that the runtime system produces an <hask>IOTree</hask> from main by evaluating <hask>runIO main (\() -> Done) :: IOTree</hask>. Here <hask>\() -> Done</hask> represents the "rest of the program", which in this case is nothing. |

The sophisticated solution to this problem is that <hask>main</hask> is passed to the operating system which will bind the next program (perhaps a shell) to <hask>main</hask>. Thus the semantics of our Haskell program becomes embedded into the semantics of the entire operating system run. |
The sophisticated solution to this problem is that <hask>main</hask> is passed to the operating system which will bind the next program (perhaps a shell) to <hask>main</hask>. Thus the semantics of our Haskell program becomes embedded into the semantics of the entire operating system run. |

## Revision as of 10:02, 18 July 2008

## Semantics of IO: A Continuation Approach

The following is inspired by Luke Palmer's post. This only describes one possible semantics ofIO a

IO

newtype IO a = IO {runIO :: (a -> IOTree) -> IOTree}

IO

Cont IOTree

IO

Cont

return x = IO (\k -> k x) x >>= f = IO (\k -> runIO x (\a -> runIO (f a) (\b -> k b)))

IOTree

IOTree

data IOTree = Done | PutChar Char IOTree | GetChar (Char -> IOTree)

GetChar

IOTree

IOTree

PutChar

GetChar

Done

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

Other teletype commands can be defined in terms of these primitives

putStr :: String -> IO () putStr = mapM_ putChar

IOTree

IOTree

| SysCallName p1 p2 ... pn (r -> IOTree)

p1

pn

r

PutChar

GetChar

IOTree

IOTree

IO ()

(() -> IOTree) -> IOTree

IOTree -> IOTree

IOTree

runIO main (\() -> Done) :: IOTree

\() -> Done

main

main

IO a

IO (\k -> filterTree (not . isPutChar) k ()) :: IO ()

putChar