IO Semantics

An adapted example

Based on page 42 of 76 in Turing-Post Relativized Computability and Interactive Computing:

The Limit Computable or Approximation Model

There exists a sequence of Turing programs {P_t : t ∈ T } so that P_t computes function g_t at time t. There is not necessarily any connection between different programs and computing may have to start all over again as the time changes from t to t + 1.

Suppose a meteorologist receives data every second t ∈ T from weather stations scattered across the country. The configuration at the meteorologist's desk may be described using the Shoenfield Limit Lemma by a computable function where g_t is the computable characteristic function of B_t, the configuration of the meteorological computation at the end of time t. The computable function g_t gives an algorithm to compute the condition B_t at time t but it gives no relationship between B_t and B_t+1. It will not be possible for the meteorologist to run, let alone write a new program every second. How will the meteorologist write a program to uniformly compute the index g_t for t ∈ T ?

The Online Model With an Oracle Machine

By the Shoenfield Limit Lemma there is a computably enumerable set A (or even a ∆⁰₂ set) and oracle machine Φ_e such that B = Φ_e^A. Now the meteorologist can program the algorithm Φ_e into a computer once and for all at the start of the day. Every second t ∈ T the meteorologist receives from the weather stations the latest readings A_t which enter directly into that computer by an network connection. The meteorologist does not (and cannot) change the program Φ_e every second. The algorithm simply receives the “oracle” information A from the weather-station network as it is continually updated, and computes the approximation B_t(x) = Φ_e^A_t(x) . The meteorologist's program then produces the next scheduled weather forecast for the day from the algorithm's result. It is difficult to see how this meteorologist could have carried out that activity using a batch processing, automatic machine model, instead of an online model.

More is needed

But the meteorologist's program has to do more than download weather-station data: it also has to upload the resulting weather forecasts, for example, to the computers of media outlets to be broadcast to listeners or viewers. Another machine model is needed, not just for interactions with other computers but also:

• a screen, to view a document,
• a printer, to have a hard copy of a document,
• a speaker, to produce some sound,
• a keyboard, mouse, microphone or controller, to obtain some input,
• an operator, if an "arbitrary choice” is needed,
• an oracle, which simply “cannot be a machine”.

An “automatic” machine becomes a “choice” machine as soon as we allow the machine’s tape to be modified by external entities: the tape itself becomes a means of communication. This is essentially what happens in “real” computers (memory-mapped I/O); for example, we can write to the computer’s screen by modifying one particular area of memory, or find out which key was pressed on the computer’s keyboard by reading another.

Making uniqueness types less unique (page 23 of 264).

So a choice machine could merely be an automatic machine given an extra ability to make requests to external entities while it is running:

• requests for output to a screen, printer or speaker.
• or for input from a keyboard, mouse, microphone, controller, an operator or an oracle.

with an oracle machine then being a specialised choice machine. Therefore if an automatic machine computes the result of an ordinary expression (like 56 + 24), a choice machine computes the result of an I/O action (like getChar) when provided with an external-entity request. So how can this concept be adapted for use in a functional language like Haskell?

Two different approaches

Note:

• For simplicity, the examples here only gives semantics for teletype I/O.
• These are only some of the various ways to describe the semantics of IO a; your actual implementation may vary.

A free type

(Inspired by Luke Palmer's post.)

The idea is to define IO as

data IO a = Done a
          | PutChar Char (IO a)
          | GetChar (Char -> IO a)

Think of IO a as a tree:

• PutChar is a node that has one child tree and the node holds one character of data.
• GetChar is a node that has many children; it has one child for every character, but GetChar holds no data itself.
• Done a (a leaf) is a node that holds the result of the program.

This tree contains all the information needed to execute basic interactions. One interprets (or executes) an IO a 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 at this point that Haskell code is 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 a Done node is encountered, the program ends.

Done holds the result of the computation, but in the case of Main.main :: IO () the data is of type () and thus ignored as it contains no information.

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 return is just another name for Done. The bind operation (>>=) takes a tree x and a function f and replaces the Done nodes (the leaves) of x by a new tree produced by applying f to the data held in the Done nodes.

The primitive I/O commands are defined using these constructors.

putChar :: Char -> IO ()
putChar x = PutChar x (Done ())

getChar :: IO Char
getChar = GetChar (\c -> Done c)

• The function putChar builds a small IO () tree that contains one PutChar node holding the character data followed by Done.
• The function getChar builds a short IO Char tree that begins with a GetChar node that holds one Done node for every character.

Other commands can be defined in terms of these primitives:

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

More generally speaking, IO a will represent the desired interaction with the operating system. For every system call there will be a corresponding I/O-tree constructor of the form:

	| SysCallName p1 p2 ... pn (r -> IO a)

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 for I/O trees if they don't correspond to system calls).

A more direct style

Here is the key idea:

A value of type IO a is an “action” that, when performed, may do some input/output, before delivering a value of type a.

Tackling the Awkward Squad (page 5 of 60).

It also has a simple translation:

            type IO a = (->) OI a
                  .       .  .  .
 an action that __|       |  |  |
                          |  |  |
 when performed __________|  |  |
                             |  |
 may do some input/output ___|  |
                                |
 before delivering a value _____|

Think of an IO a action as an entity which:

• can be used like other Haskell functions,
• but may also have effects like procedures.

This combination of denotative and imperative features is enough to provide basic interactions. An IO a action works by calling it when applied to an OI argument, subject to certain conditions:

• Each OI value should be distinct from all others, to help preserve referential transparency.
• Each OI value should be used at most once, to ensure actions can be used like other functions.

As for the OI type itself:

data OI  -- no constructors are visible to the user

Most OI values would then be provided by one or more specific actions:

foreign import partOI  :: OI -> (OI, OI)

partsOI                :: OI -> [OI]
partsOI u              = let !(u1, u2) = partOI u in u1 : partsOI u2

but in the case of Main.main :: IO () the initial argument is provided directly by the implementation. It is from this initial argument that all other OI values in the program are obtained.

Not being able to define OI values directly in Haskell means actions in a Haskell program cannot work until the program, applied to its initial OI argument, is called by the run-time system.

The monadic operations are defined as follows:

instance Monad ((->) OI)
  where
        return x =  \ u -> let !_ = partOI u in x 

        m >>= k  =  \ u -> let !(u1, u2) = partOI u
                               !x = m u1
                               !y = k x u2 in
                           in y

Note that both methods use their OI parameters, with return simply returning its other parameter x to the caller. The bind operation (>>=) takes an action m and a function k and uses new OI values to call m to obtain x, then call k x to obtain the result y.

Other actions can be declared:

foreign import getChar :: OI -> Char
foreign import putChar :: Char -> OI -> ()

or defined:

getLine                :: OI -> [Char]
getLine                = do c <- getChar
                            if c == ’\n’ then return ""
                                         else do cs <- getLine
                                              return (c:cs)

putStr                 :: [Char] -> OI -> ()
putStr cs              = foldr (\ !(_) -> id) () . zipWith putChar cs . partsOI

In more fully-featured implementations, each system call would have its own declaration:

primitive primSysCallName :: T1 -> T2 -> ... -> OI -> Tr

foreign import ... extnSysCallName :: T1 -> T2 -> ... -> OI -> Tr

where:

• T1, T2 ... are the types of the parameters for the system call,
• and Tr is the type of the system call's result.

Further reading

• The Haskell 2010 Report

ed. Simon Marlow Marlow, 2010.

• A Functional Specification of Effects

Wouter Swierstra. Ph.D. thesis, University of Nottingham. (2009).

• Beauty in the Beast: A Functional Semantics for the Awkward Squad

Wouter Swierstra, Thorsten Altenkirch. In: Proceedings of the ACM SIGPLAN Workshop on Haskell, Haskell ’07, ACM, New York, NY, USA, pages 25–36 (2007).

• A Semantic Framework for Deterministic Functional Input/Output

Malcolm Dowse. PhD dissertation, University of Dublin, Trinity College (2006).

• Semantics of fixIO

Levent Erkök, John Launchbury, Andrew Moran. In Fixed Points in Computer Science Workshop, FICS'01 (2001).

• Tackling the Awkward Squad: monadic input/output, concurrency, exceptions, and foreign-language calls in Haskell

Simon Peyton Jones. In "Engineering theories of software construction", ed. Tony Hoare, Manfred Broy, Ralf Steinbruggen, IOS Press, ISBN 1 58603 1724, 2001, pages 47-96.

• Relating operational and denotational semantics for input/output effects

Roy L. Crole, Andrew D. Gordon. Mathematical Structures in Computer Science 9(2): 125-158 (1999).

• How to Declare an Imperative

Philip Wadler. ACM Computing Surveys, 29(3): 240-263, September 1997.

• Monadic I/O in Haskell 1.3

Andrew D. Gordon and Kevin Hammond. In: Proceedings of the Haskell Workshop, La Jolla, California, June 1995.

• A Sound Metalogical Semantics for Input/Output Effects

Andrew Gordon. In International Workshop on Computer Science Logic, January 1995. Springer Berlin Heidelberg.

• An Operational Semantics for I/O in a Lazy Functional Language

Andrew Gordon. In FPCA '93: Conference on Functional Programming Languages and Computer Architecture, Copenhagen, June 1993. ACM Press.

• Functional Programming and Input/Output

Andrew Gordon. Cambridge University Press. Revision of 1992 PhD dissertation.

• PFL+: A Kernel Scheme for Functional I/O

Andrew Gordon. Computer Laboratory Technical Report Number 160, University of Cambridge (1989).

• Interactive Functional Programs: A Method and a Formal Semantics

Simon Thompson. Technical Report 48, Computing Laboratory, University of Kent, Canterbury, UK, November 1987.