# Difference between revisions of "IO Semantics"

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 { |
+ | 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 -> |
+ | 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> |
+ | 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 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))
```

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.