IO Semantics: Difference between revisions

Latest revision as of 16:36, 17 February 2025

More than denotational

As mathematics is denotative, a semantics of I/O needs to go beyond mathematics. One option is to use the choice machine and its external operator - being external means the operator can also facilitate I/O. But as the basis for a semantics of I/O in Haskell programs, the choice machine has one potential difficulty - it is an imperative abstraction. So can it be adapted for use in a functional language?

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

The choice machine can also be viewed as an extended automatic machine whose state can be accessed by external entities, at the request of of the running program:

data OI                   -- a request to an external entity

partOI :: OI -> (OI, OI)  -- an I/O action requesting two more requests

getChar :: OI -> Char     -- an I/O action requesting the next character of input

putChar :: Char ->        -- a function expecting a character which returns
           OI -> ()       -- an I/O action requesting the output of the given character

The action partOI :: OI -> (OI, OI) is needed to obtain new OI values because each one represents a single (once-only) request to an external entity. Hence multiple actions using the same OI value for different requests would be ambiguous.

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.

The type of I/O actions is easily defined:

type IO a  =  OI -> a
      .       .  .  .
      |       |  |  |
   an I/O     |  |  |
   action     |  |  |
              |  |  |
  may involve a  |  |
  request to an  |  |
 external entity |  |
                 |  |
        when being  |
         computed   |
                    |
            to obtain
             a result

As for the monadic interface:

instance {-# OVERLAPPING #-} Monad ((->) OI) where
    return = unitIO
    (>>=)  = bindIO
    (>>)   = nextIO

unitIO     :: a -> OI -> a
unitIO x   = \ u -> partOI u `pseq` x

bindIO     :: (OI -> a) -> (a -> OI -> b) -> OI -> b
bindIO m k = \ u -> case partOI u of (u1, u2) -> (\ x -> x `pseq` k x u2) (m u1)

nextIO     :: (OI -> a) -> (IO -> b) -> OI -> b
nextIO m w = \ u -> case partOI u of (u1, u2) -> m u1 `pseq` w u2

Control.Parallel.pseq is needed because Prelude.seq is non-sequential, prior evidence to the contrary notwithstanding.

@@ Line 1: / Line 1: @@
 [[Category:Theoretical_foundations]]
-== An adapted example ==
+== More than denotational ==
-Based on page 42 of 76 in [http://www.people.cs.uchicago.edu/~soare/Turing/shagrir.pdf Turing-Post Relativized Computability and Interactive Computing]:
+As mathematics is [[denotative]], a semantics of I/O needs to go beyond mathematics.
+One option is to use the [[Turing's_various_machines#The_choice_machine|choice machine]]
-<blockquote>
+and its external operator - being external means the operator can also
-<b>The Limit Computable or Approximation Model</b>
+facilitate I/O. But as the basis for a semantics of I/O in Haskell
+programs, the choice machine has one potential difficulty - it is an
-There exists a sequence of Turing programs {<i>P<sub>t</sub></i> : <i>t</i> ∈ <i>T</i> } so that
+imperative abstraction. So can it be adapted for use in a functional
-<i>P<sub>t</sub></i> computes function <i>g<sub>t</sub></i> at time <i>t</i> ∈ <i>T</i>. There is not
+language?
-necessarily any connection between different programs and computing may have to
-start all over again with a new program as the time changes from <i>t</i> to <i>t</i> + 1.
-Suppose a meteorologist receives data every second <i>t</i> ∈ <i>T</i> 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 <i>g<sub>t</sub></i> is the computable characteristic function of
-<i>B<sub>t</sub></i>, the configuration of the meteorological computation at the end
-of time <i>t</i>. The computable function <i>g<sub>t</sub></i> gives an algorithm to
-compute the condition <i>B<sub>t</sub></i> at time <i>t</i> but it gives no relationship
-between <i>B<sub>t</sub></i> and <i>B</i><sub><i>t</i>+1</sub>. 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 <i>g<sub>t</sub></i>
-for <i>t</i> ∈ <i>T</i> ?
-<b>The Online Model With an Oracle Machine</b>
-By the Shoenfield Limit Lemma there is a computably enumerable set <i>A</i> (or even
-a ∆<sup>0</sup><sub>2</sub> set) and oracle machine Φ<sub><i>e</i></sub> such that
-<i>B</i> = Φ<sub><i>e</i></sub><sup><i>A</i></sup>. Now the meteorologist can program the
-algorithm Φ<sub><i>e</i></sub> into a computer once and for all at the start of the
-day. Every second <i>t</i> ∈ <i>T</i> the meteorologist receives from the weather stations
-the latest readings <i>A<sub>t</sub></i> which enter directly into that computer by
-an network connection. The meteorologist does not (and cannot) change the
-program Φ<sub><i>e</i></sub> every second. The algorithm simply receives the
-“oracle” information <i>A</i> from the weather-station network as it is continually
-updated, and computes the approximation <i>B<sub>t</sub></i>(<i>x</i>) =
-Φ<sub><i>e</i></sub><sup><i>A<sub>t</sub></i></sup>(<i>x</i>) . 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.
-</blockquote>
-== 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,
-* [https://www.cs.virginia.edu/~robins/Turing_Paper_1936.pdf an operator], if an "arbitrary choice” is needed,
-* [https://pure.mpg.de/rest/items/item_2403325_2/component/file_2403324/content an oracle], which simply “cannot be a machine”.
-<blockquote>
-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.
-<small>[https://web.archive.org/web/20160527210838/https://www.edsko.net/pubs/thesis.pdf Making uniqueness types less unique] (page 23 of 264).</small>
-</blockquote>
-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 <i>output</i> to a screen, printer or speaker.
-* or for <i>input</i> 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
-<code>56 + 24</code>), a choice machine computes the result of an I/O action (like
-<code>getChar</code>) when the action is provided with an external-entity request. So how can
-this concept be adapted for use in a <i>functional</i> language like Haskell?
 == Two different approaches ==
@@ Line 90: / Line 20: @@
 === A free type ===
-(Inspired by [https://lukepalmer.wordpress.com/2008/03/29/io-monad-the-continuation-presentation Luke Palmer's post].)
+(Inspired by [https://web.archive.org/web/20111016161358/https://lukepalmer.wordpress.com/2008/03/29/io-monad-the-continuation-presentation Luke Palmer's post].)
 The idea is to define <code>IO</code> as
@@ Line 156: / Line 86: @@
 === A more direct style ===
-Recalling that a choice machine computes the result of an I/O action when
+The choice machine can also be viewed as an extended
-the action is provided an external-entity request:
+[[Turing's_various_machines#The_automatic_machine|automatic machine]] whose
+state can be accessed by external entities, at the request of of the running
+program:
 <haskell>
@@ Line 214: / Line 146: @@
 <haskell>
 instance {-# OVERLAPPING #-} Monad ((->) OI) where
-     return = unitOI
+     return = unitIO
      (>>=)  = bindIO
-     (>>)   = nextOI
+     (>>)   = nextIO
-unitOI     :: a -> OI -> a
+unitIO     :: a -> OI -> a
-unitOI x   = \ u -> partOI u `pseq` x
+unitIO x   = \ u -> partOI u `pseq` x
-bindOI     :: (OI -> a) -> (a -> OI -> b) -> OI -> b
+bindIO     :: (OI -> a) -> (a -> OI -> b) -> OI -> b
-bindOI m k = \ u -> case partOI u of (u1, u2) -> (\ x -> x `pseq` k x u2) (m u1)
+bindIO m k = \ u -> case partOI u of (u1, u2) -> (\ x -> x `pseq` k x u2) (m u1)
-nextOI     :: (OI -> a) -> (IO -> b) -> OI -> b
+nextIO     :: (OI -> a) -> (IO -> b) -> OI -> b
-nextOI m w = \ u -> case partOI u of (u1, u2) -> m u1 `pseq` w u2
+nextIO m w = \ u -> case partOI u of (u1, u2) -> m u1 `pseq` w u2
 </haskell>
-<code>Control.Parallel.pseq</code> is needed because <code>Prelude.seq</code> [https://mail.haskell.org/pipermail/glasgow-haskell-users/2006-October/011430.html isn't sequential],
+<code>Control.Parallel.pseq</code> is needed because <code>Prelude.seq</code> is [[Seq|non]]-sequential, prior evidence to the contrary notwithstanding.
-the fact that a sequencing definition was a known necessity [https://web.archive.org/web/20040228202402/http://www.dcs.gla.ac.uk/fp/workshops/fpw96/Trinder.pdf since 1996]
-notwithstanding.
 == <span id="readmore"></span> Further reading ==