Difference between revisions of "IO Semantics"

From HaskellWiki
Jump to: navigation, search
(Continuation style semantics for IO)
 
m (Extra references added; existing one expanded)
 
(15 intermediate revisions by 3 users not shown)
Line 1: Line 1:
== Semantics of IO, a continuation approach ==
+
[[Category:Theoretical_foundations]]
 +
== Semantics of <code>IO</code>: A Free Approach ==
  
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.
+
The following is inspired by [https://lukepalmer.wordpress.com/2008/03/29/io-monad-the-continuation-presentation Luke Palmer's post] on the topic. This only describes one possible semantics of <code>IO a</code>; your actual implementation may vary.
  
The idea to to define <hask>IO</hask> as
+
The idea is to define <code>IO</code> as
 
<haskell>
 
<haskell>
newtype IO a = IO {unIO :: (a -> IOTree) -> IOTree}
+
data IO a = Done a
 +
          | 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>.
+
 
 +
For simplicity, this is an example of <code>IO</code> that only gives semantics for teletype I/O.
 +
 
 +
Think of <code>IO a</code> as a tree whose leaves are <code>Done a</code> that holds the result of the program:
 +
* <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.
 +
 
 +
This tree contains all the information needed to execute teletype 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 executedIt 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 <code>Done</code> 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 contains no information and is ignored.
 +
 
 +
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 x = IO (\k -> k x)
+
return :: a -> IO a
x >>= f = IO (\k -> unIO x (\a -> unIO (f a) (\b -> k b)))
+
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)
 
</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)
 
  
<hask>IOTree</hask> contains all the information needed to execute teletype interactions.
+
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.
One interprets (or executes) an <hask>IOTree</hask> by tracing a route from root of the tree to a leaf.
 
  
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 I/O commands are defined using these constructors.
The primitive IO commands are defined using these constructors
 
 
<haskell>
 
<haskell>
 
putChar :: Char -> IO ()
 
putChar :: Char -> IO ()
putChar x = IO (\k -> PutChar x (k ()))
+
putChar x = PutChar x (Done ())
  
 
getChar :: IO Char
 
getChar :: IO Char
getChar = IO (\k -> GetChar (\x -> k x))
+
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 teletype 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 -> IOTree)
+
| SysCallName p1 p2 ... pn (r -> IO a)
 
</haskell>
 
</haskell>
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)
+
where <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).
 +
 
 +
== Further reading ==
 +
 
 +
* [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://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).
  
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.
+
* [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.
  
The simple solution to this is that the runtime system produces an <hask>IOTree</hask> from main by evaluating <hask>unIO main (\() -> Done) :: IOTree</hask>. Here <hask>\() -> Done</hask> represents the "rest of the program", which in this case is nothing.
+
* [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).
  
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.
+
* [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.
  
The type for <hask>IO a</hask> that we have given contains invalid programs such as
+
* [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]
<haskell>
+
::Andrew Gordon. In FPCA '93: Conference on Functional Programming Languages and Computer Architecture, Copenhagen, June 1993. ACM Press.
IO (\k -> filterTree (not . isPutChar) k ()) :: IO ()
+
 
</haskell>
+
* [https://dblp.org/rec/phd/ethos/Gordon92.html Functional Programming and Input/Output]
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.
+
::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).

Latest revision as of 04:21, 25 April 2022

Semantics of IO: A Free Approach

The following is inspired by Luke Palmer's post on the topic. This only describes one possible semantics of IO a; your actual implementation may vary.

The idea is to define IO as

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

For simplicity, this is an example of IO that only gives semantics for teletype I/O.

Think of IO a as a tree whose leaves are Done a that holds the result of the program:

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

This tree contains all the information needed to execute teletype 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 Done 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 contains no information and is ignored.

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

Further reading

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