Difference between revisions of "IO Semantics"
(rename unIO into runIO) |
m |
||
(25 intermediate revisions by 3 users not shown) | |||
Line 1: | Line 1: | ||
+ | [[Category:Theoretical_foundations]] |
||
− | == Semantics of IO: A Continuation Approach == |
||
+ | == An adapted example == |
||
− | The following is inspired by [http://luqui.org/blog/archives/2008/03/29/io-monad-the-continuation-presentation/ Luke Palmer's post]. This only describes one possible semantics of <hask>IO a</hask>; your actually implementation may vary. |
||
+ | Based on page 42 of 76 in [http://www.people.cs.uchicago.edu/~soare/Turing/shagrir.pdf Turing-Post Relativized Computability and Interactive Computing]: |
||
− | The idea to to define <hask>IO</hask> as |
||
+ | |||
+ | <blockquote> |
||
+ | <b>The Limit Computable or Approximation Model</b> |
||
+ | |||
+ | There exists a sequence of Turing programs {<i>P<sub>t</sub></i> : <i>t</i> ∈ <i>T</i> } so that |
||
+ | <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 |
||
+ | 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<sub>t</sub></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 == |
||
+ | <i> |
||
+ | 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 </i><code>IO a</code><i>; your actual implementation may vary. |
||
+ | </i> |
||
+ | |||
+ | === A free type === |
||
+ | |||
+ | (Inspired by [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 |
||
<haskell> |
<haskell> |
||
+ | data IO a = Done a |
||
− | newtype IO a = IO {runIO :: (a -> IOTree) -> IOTree} |
||
+ | | PutChar Char (IO a) |
||
+ | | GetChar (Char -> IO a) |
||
</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>. |
||
+ | Think of <code>IO a</code> as a tree: |
||
+ | * <code>PutChar</code> is a node that has one child tree and the node holds one character of data. |
||
+ | * <code>GetChar</code> is a node that has many children; it has one child for every character, but <code>GetChar</code> holds no data itself. |
||
+ | * <code>Done a</code> (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 <code>IO a</code> by tracing a route from root of the tree to a leaf: |
||
+ | * If a <code>PutChar</code> 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 <code>GetChar</code> 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 <code>Done</code> node is encountered, the program ends. |
||
+ | |||
+ | <code>Done</code> holds the result of the computation, but in the case of <code>Main.main :: IO ()</code> the data is of type <code>()</code> 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: |
||
<haskell> |
<haskell> |
||
− | return |
+ | return :: a -> IO a |
+ | return x = Done x |
||
− | x >>= f = IO (\k -> runIO x (\a -> runIO (f a) (\b -> k b))) |
||
+ | |||
+ | (>>=) :: 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) |
||
</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. |
||
− | <haskell> |
||
− | data IOTree = Done |
||
− | | PutChar Char IOTree |
||
− | | GetChar (Char -> IOTree) |
||
− | </haskell> |
||
− | (This is a tree because the <hask>GetChar</hask> node has one subtree for every character) |
||
+ | As you can see <code>return</code> is just another name for <code>Done</code>. The bind operation <code>(>>=)</code> takes a tree <code>x</code> and a function <code>f</code> and replaces the <code>Done</code> nodes (the leaves) of <code>x</code> by a new tree produced by applying <code>f</code> to the data held in the <code>Done</code> nodes. |
||
− | <hask>IOTree</hask> contains all the information needed to execute teletype interactions. |
||
− | One interprets (or executes) an <hask>IOTree</hask> by tracing a route from root of the tree to a leaf. |
||
+ | The primitive I/O commands are defined using these constructors. |
||
− | If a <hask>PutChar</hask> 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 <hask>GetChar</hask> node is encountered, a character is read from the terminal (blocking if necessary) and the subtree corresponding to the character received is executed. If <hask>Done</hask> is encountered the program ends. |
||
− | The primitive IO commands are defined using these constructors |
||
<haskell> |
<haskell> |
||
putChar :: Char -> IO () |
putChar :: Char -> IO () |
||
− | putChar x = |
+ | putChar x = PutChar x (Done ()) |
getChar :: IO Char |
getChar :: IO Char |
||
− | getChar = |
+ | getChar = GetChar (\c -> Done c) |
</haskell> |
</haskell> |
||
+ | |||
− | Other teletype commands can be defined in terms of these primitives |
||
+ | * The function <code>putChar</code> builds a small <code>IO ()</code> tree that contains one <code>PutChar</code> node holding the character data followed by <code>Done</code>. |
||
+ | * The function <code>getChar</code> builds a short <code>IO Char</code> tree that begins with a <code>GetChar</code> node that holds one <code>Done</code> node for every character. |
||
+ | |||
+ | Other commands can be defined in terms of these primitives: |
||
<haskell> |
<haskell> |
||
putStr :: String -> IO () |
putStr :: String -> IO () |
||
putStr = mapM_ putChar |
putStr = mapM_ putChar |
||
</haskell> |
</haskell> |
||
+ | |||
− | More generally speaking, <hask>IOTree</hask> will represent the desired interaction with the operating system. For every system call there will be a corresponding constructor in <hask>IOTree</hask> of the form |
||
+ | More generally speaking, <code>IO a</code> 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: |
||
<haskell> |
<haskell> |
||
− | | SysCallName p1 p2 ... pn (r -> |
+ | | SysCallName p1 p2 ... pn (r -> IO a) |
</haskell> |
</haskell> |
||
+ | where: |
||
− | where <hask>p1</hask> ... <hask>pn</hask> are the parameters for the system call, and <hask>r</hask> is the result of the system call. (Thus <hask>PutChar</hask> and <hask>GetChar</hask> will not occur as constructors of <hask>IOTree</hask> if they don't correspond to system calls) |
||
+ | * <code>p1</code> ... <code>pn</code> are the parameters for the system call, |
||
+ | * and <code>r</code> is the result of the system call. |
||
+ | (Thus <code>PutChar</code> and <code>GetChar</code> will not occur as constructors for I/O trees if they don't correspond to system calls). |
||
− | 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. |
||
+ | === A more direct style === |
||
− | 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. |
||
+ | Recalling that a choice machine computes the result of an I/O action when |
||
− | 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 action is provided an external-entity request: |
||
− | The type for <hask>IO a</hask> that we have given contains invalid programs such as |
||
<haskell> |
<haskell> |
||
+ | data OI -- a request to an external entity |
||
− | IO (\k -> filterTree (not . isPutChar) k ()) :: IO () |
||
+ | |||
+ | 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 |
||
</haskell> |
</haskell> |
||
+ | |||
− | which would remove the output of any future <hask>putChar</hask> commands. However, none of these illegal programs can be generated from the monadic interface and the primitive operations provided. |
||
+ | The action <code>partOI :: OI -> (OI, OI)</code> is needed to obtain new <code>OI</code> values |
||
+ | because each one represents a single (once-only) request to an external entity. |
||
+ | Hence multiple actions using the same <code>OI</code> value for different requests would |
||
+ | be ambiguous. |
||
+ | |||
+ | In more fully-featured implementations, each system call would have its own declaration: |
||
+ | |||
+ | <haskell> |
||
+ | primitive primSysCallName :: T1 -> T2 -> ... -> OI -> Tr |
||
+ | </haskell> |
||
+ | |||
+ | <haskell> |
||
+ | foreign import ... extnSysCallName :: T1 -> T2 -> ... -> OI -> Tr |
||
+ | </haskell> |
||
+ | |||
+ | where: |
||
+ | * <code>T1</code>, <code>T2</code> ... are the types of the parameters for the system call, |
||
+ | * and <code>Tr</code> is the type of the system call's result. |
||
+ | |||
+ | |||
+ | The type of I/O actions is easily defined: |
||
+ | |||
+ | <pre> |
||
+ | type IO a = OI -> a |
||
+ | . . . . |
||
+ | | | | | |
||
+ | an I/O | | | |
||
+ | action | | | |
||
+ | | | | |
||
+ | may involve a | | |
||
+ | request to an | | |
||
+ | external entity | | |
||
+ | | | |
||
+ | when being | |
||
+ | computed | |
||
+ | | |
||
+ | to obtain |
||
+ | a result |
||
+ | </pre> |
||
+ | |||
+ | As for the monadic interface: |
||
+ | |||
+ | <haskell> |
||
+ | 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 |
||
+ | </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], |
||
+ | 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 == |
||
+ | |||
+ | * [https://www.haskell.org/definition/haskell2010.pdf The Haskell 2010 Report] |
||
+ | ::ed. Simon Marlow Marlow, 2010. |
||
+ | |||
+ | * [http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.722.8440&rep=rep1&type=pdf A Functional Specification of Effects] |
||
+ | ::Wouter Swierstra. Ph.D. thesis, University of Nottingham. (2009). |
||
+ | |||
+ | * [https://www.cs.nott.ac.uk/~psztxa/publ/beast.pdf 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). |
||
+ | |||
+ | * [https://www.scss.tcd.ie/publications/tech-reports/reports.06/TCD-CS-2006-19.pdf A Semantic Framework for Deterministic Functional Input/Output] |
||
+ | ::Malcolm Dowse. PhD dissertation, University of Dublin, Trinity College (2006). |
||
+ | |||
+ | * [https://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.15.736&rep=rep1&type=pdf Semantics of ''fixIO''] |
||
+ | ::Levent Erkök, John Launchbury, Andrew Moran. In Fixed Points in Computer Science Workshop, FICS'01 (2001). |
||
+ | |||
+ | * [https://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.13.9123&rep=rep1&type=pdf 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. |
||
+ | |||
+ | * [https://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.52.6409&rep=rep1&type=pdf 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). |
||
+ | |||
+ | * [https://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.91.3579&rep=rep1&type=pdf How to Declare an Imperative] |
||
+ | ::Philip Wadler. ACM Computing Surveys, 29(3): 240-263, September 1997. |
||
+ | |||
+ | * [https://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.52.6922&rep=rep1&type=pdf Monadic I/O in Haskell 1.3] |
||
+ | ::Andrew D. Gordon and Kevin Hammond. In: Proceedings of the Haskell Workshop, La Jolla, California, June 1995. |
||
+ | |||
+ | * [https://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.16.5894&rep=rep1&type=pdf A Sound Metalogical Semantics for Input/Output Effects] |
||
+ | ::Andrew Gordon. In International Workshop on Computer Science Logic, January 1995. Springer Berlin Heidelberg. |
||
+ | |||
+ | * [https://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.16.3541&rep=rep1&type=pdf 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. |
||
+ | |||
+ | * [https://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.134.5784&rep=rep1&type=pdf Functional Programming and Input/Output] |
||
+ | ::Andrew Gordon. Cambridge University Press. Revision of 1992 PhD dissertation. |
||
+ | |||
+ | * [https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-160.pdf PFL+: A Kernel Scheme for Functional I/O] |
||
+ | ::Andrew Gordon. Computer Laboratory Technical Report Number 160, University of Cambridge (1989). |
||
+ | |||
+ | * [https://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.45.8497&rep=rep1&type=pdf Interactive Functional Programs: A Method and a Formal Semantics] |
||
+ | ::Simon Thompson. Technical Report 48, Computing Laboratory, University of Kent, Canterbury, UK, November 1987. |
Latest revision as of 16:38, 14 August 2024
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 {Pt : t ∈ T } so that Pt computes function gt at time t ∈ T. 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 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 gt is the computable characteristic function of Bt, the configuration of the meteorological computation at the end of time t. The computable function gt gives an algorithm to compute the condition Bt at time t but it gives no relationship between Bt and Bt+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 gt 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 ∆02 set) and oracle machine Φe such that B = ΦeA. 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 At 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 At from the weather-station network as it is continually updated, and computes the approximation Bt(x) = ΦeAt(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 the action is 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, butGetChar
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 smallIO ()
tree that contains onePutChar
node holding the character data followed byDone
. - The function
getChar
builds a shortIO Char
tree that begins with aGetChar
node that holds oneDone
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
Recalling that a choice machine computes the result of an I/O action when the action is provided an external-entity request:
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
isn't sequential,
the fact that a sequencing definition was a known necessity since 1996
notwithstanding.
Further reading
- ed. Simon Marlow Marlow, 2010.
- Wouter Swierstra. Ph.D. thesis, University of Nottingham. (2009).
- Wouter Swierstra, Thorsten Altenkirch. In: Proceedings of the ACM SIGPLAN Workshop on Haskell, Haskell ’07, ACM, New York, NY, USA, pages 25–36 (2007).
- Malcolm Dowse. PhD dissertation, University of Dublin, Trinity College (2006).
- Levent Erkök, John Launchbury, Andrew Moran. In Fixed Points in Computer Science Workshop, FICS'01 (2001).
- 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.
- Roy L. Crole, Andrew D. Gordon. Mathematical Structures in Computer Science 9(2): 125-158 (1999).
- Philip Wadler. ACM Computing Surveys, 29(3): 240-263, September 1997.
- Andrew D. Gordon and Kevin Hammond. In: Proceedings of the Haskell Workshop, La Jolla, California, June 1995.
- Andrew Gordon. In International Workshop on Computer Science Logic, January 1995. Springer Berlin Heidelberg.
- Andrew Gordon. In FPCA '93: Conference on Functional Programming Languages and Computer Architecture, Copenhagen, June 1993. ACM Press.
- Andrew Gordon. Cambridge University Press. Revision of 1992 PhD dissertation.
- Andrew Gordon. Computer Laboratory Technical Report Number 160, University of Cambridge (1989).
- Simon Thompson. Technical Report 48, Computing Laboratory, University of Kent, Canterbury, UK, November 1987.