IO Semantics: Difference between revisions

Revision as of 02:44, 10 December 2024

More than denotational

Mathematics is denotative:

When a mathematician develops a theorem, she or he defines symbols, then writes down facts that relate those symbols. The order of those facts is unimportant, so long as all the symbols used are defined, and it certainly does not matter where each fact is written on the paper! A proof is a static thing—its parts just are, they do not act.

The Anatomy of Programming Languages (page 354 of 600).

Therefore a semantics of I/O needs to go beyond mathematics:

For some purposes we might use machines (choice machines or c-machines) whose motion is only partially determined by the configuration (hence the use of the word "possible" in §1). When such a machine reaches one of these ambiguous configurations, it cannot go on until some arbitrary choice has been made by an external operator. This would be the case if we were using machines to deal with axiomatic systems.

On Computable Numbers, with an Application to the Entscheidungsproblem (page 253).

While the operator isn't always needed:

If at each stage the motion of a machine (in the sense of §1) is completely determined by the configuration, we shall call the machine an "automatic machine" (or a-machine).

it being external means it can also facilitate I/O.

So the choice machine could be a suitable basis for a semantics of I/O in Haskell programs...apart from it being an imperative abstraction! 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:

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

with those external entities only allowed access at the request 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 = unitOI
    (>>=)  = bindIO
    (>>)   = nextOI

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

bindOI     :: (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)

nextOI     :: (OI -> a) -> (IO -> b) -> OI -> b
nextOI 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]:
+Mathematics is [[Denotative|denotative]]:
 <blockquote>
-<b>The Limit Computable or Approximation Model</b>
+When a mathematician develops a theorem, she or he defines symbols, then writes
+down facts that relate those symbols. The order of those facts is unimportant, so long as all the
+symbols used are defined, and it certainly does not matter where each fact is written on the paper!
+A proof is a static thing—its parts just <i>are</i>, they do not <i>act</i>.
-There exists a sequence of Turing programs <math>\{P_t:t \in T\}</math> so that
+:<small>[https://digitalcommons.newhaven.edu/cgi/viewcontent.cgi?article=1000&context=electricalcomputerengineering-books The Anatomy of Programming Languages] (page 354 of 600).</small>
-<math>P_t</math> computes function <math>g_t</math> at time <math>{t \in T}</math>. There is not
-necessarily any connection between different programs and computing may have to
-start all over again with a new program as the time changes from <math>t</math> to <math>t+1</math>.
-Suppose a meteorologist receives data every second <math>t \in T</math> 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 <math>g_t</math> is the computable characteristic function of
-<math>B_t</math>, the configuration of the meteorological computation at the end
-of time <math>t</math>. The computable function <math>g_t</math> gives an algorithm to
-compute the condition <math>B_t</math> at time <math>t</math> but it gives no relationship
-between <math>B_t</math> and <math>B_{t+1}</math>. 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 <math>g_t</math>
-for <math>{t \in T}</math>?
-<b>The Online Model With an Oracle Machine</b>
-By the Shoenfield Limit Lemma there is a computably enumerable set <math>{A}</math> (or even
-a <math>\Delta_2^0</math> set) and oracle machine <math>\Phi_e</math> such that
-<math>B = \Phi_e^A</math>. Now the meteorologist can program the
-algorithm <math>\Phi_e</math> into a computer once and for all at the start of the
-day. Every second <math>{t \in T}</math> the meteorologist receives from the weather stations
-the latest readings <math>A_t</math> which enter directly into that computer by
-an network connection. The meteorologist does not (and cannot) change the
-program <math>\Phi_e</math> every second. The algorithm simply receives the
-“oracle” information <math>A_t</math> from the weather-station network as it is continually
-updated, and computes the approximation <math>B_t(x) = \Phi_e^{A_t}(x)</math>.
-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 ==
+Therefore a semantics of I/O needs to go beyond mathematics:
-But an oracle is only a means of input:
-<blockquote>
-Now suppose instead, says Turing
-[https://pure.mpg.de/rest/items/item_2403325_2/component/file_2403324/content <span><span>]&nbsp;
-in effect, this situation obtains with the following
-modification. That at certain times the otherwise machine determined
-process raises the question is a certain positive integer in a given
-recursively enumerable set <math>S_2</math> of positive integers, and that the machine
-is so constructed that were the correct answer to this question supplied
-on every occasion that arises, the process would automatically
-continue to its eventual correct conclusion.<sup>23</sup>
-<sup>23</sup>Turing picturesquely suggests access to an “oracle” which would supply the
-correct answer in each case. The “if” of mathematics is however more conducive to the
-development of a theory.
-:<small>[https://www.ams.org/journals/bull/1944-50-05/S0002-9904-1944-08111-1/S0002-9904-1944-08111-1.pdf Recursively enumerable sets of positive integers and their decision problems] (page 311).</small>
-</blockquote>
-Therefore the oracle machine is insufficient for an online model - some means
-of output is needed:
-* for the weather-stations' programs to supply the network (and the meteorologist's program) with their readings,
-* and to supply the resulting forecasts, for example, to media outlets broadcasting to listeners or viewers.
-Furthermore, the meteorologist may for some reason decide to intervene while
-those programs are running (perhaps restarting some of them to provide more
-accurate forecasts after software upgrades). Given these extra requirements,
-can an online model for all of the meteorologist's programs still be based on
-one machine?
 <blockquote>
@@ Line 100: / Line 37: @@
 it being external means it can also facilitate I/O.
-At this point, the choice machine seems to be a more suitable basis for an
+So the choice machine could be a suitable basis for a semantics of I/O in
-online model of the meteorologist's programs. But one significant difficulty
+Haskell programs...apart from it being an imperative abstraction! Can it
-remains: it is an imperative abstraction. So how how can it be adapted for
+be adapted for use in a functional language?
-use in a functional language like Haskell?
 == Two different approaches ==

Revision as of 02:44, 10 December 2024

More than denotational

Two different approaches

A free type

A more direct style

Further reading