IO Semantics: Difference between revisions

From HaskellWiki
mNo edit summary
mNo edit summary
 
(20 intermediate revisions by the same user not shown)
Line 1: Line 1:
[[Category:Theoretical_foundations]]
[[Category:Theoretical_foundations]]


== More than denotational ==
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]]
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 ==
<i>
<i>
Note:
Note:
Line 9: Line 20:
=== A free type ===
=== 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
The idea is to define <code>IO</code> as
Line 75: Line 86:
=== A more direct style ===
=== A more direct style ===


<blockquote>
The choice machine can also be viewed as an extended       
Here is the key idea:
[[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:


:A value of type <code>IO a</code> is an “action” that, when performed, may do some input/output, before delivering a value of type <code>a</code>.
<haskell>
data OI                  -- a request to an external entity


:<small>[[#readmore|Tackling the Awkward Squad]] (page 5 of 60).</small>
partOI :: OI -> (OI, OI) -- an I/O action requesting two more requests
</blockquote>


It also has a [https://www.interaction-design.org/literature/topics/keep-it-simple-stupid simple] translation:
getChar :: OI -> Char    -- an I/O action requesting the next character of input
<pre>
 
            type IO a = (->) OI a
putChar :: Char ->        -- a function expecting a character which returns
                  .       .  .  .
          OI -> ()      -- an I/O action requesting the output of the given character
an action that __|      |  |  |
</haskell>
                          |  |  |
when performed __________|  |  |
                            |  |
may do some input/output ___|  |
                                |
before delivering a value _____|
</pre>


Think of an <code>IO a</code> action as an entity which:
The action <code>partOI :: OI -> (OI, OI)</code> is needed to obtain new <code>OI</code> values
* can be used like other Haskell functions,
because each one represents a single (once-only) request to an external entity.
* but may also have effects like procedures.
Hence multiple actions using the same <code>OI</code> value for different requests would
be ambiguous.


This combination of [[Denotative|denotative]] and imperative features is enough to provide basic interactions. An <code>IO a</code> action works by calling it when applied to an <code>OI</code> argument, subject to certain conditions:
In more fully-featured implementations, each system call would have its own declaration:
* Each <code>OI</code> value should be distinct from all others, to help preserve [[Referential transparency|referential transparency]].
* Each <code>OI</code> value should be used at most once, to ensure actions can be used like other functions.


As for the <code>OI</code> type itself:
<haskell>
<haskell>
data OI -- no constructors are visible to the user
primitive primSysCallName :: T1 -> T2 -> ... -> OI -> Tr
</haskell>
</haskell>


Most <code>OI</code> values would then be provided by one or more specific actions:
<haskell>
<haskell>
foreign import partOI  :: OI -> (OI, OI)
foreign import ... extnSysCallName :: T1 -> T2 -> ... -> OI -> Tr
 
partsOI                :: OI -> [OI]
partsOI u              = let !(u1, u2) = partOI u in u1 : partsOI u2
</haskell>
</haskell>


but in the case of <code>Main.main :: IO ()</code> the initial argument is provided directly by the implementation. It is from this initial argument that all other <code>OI</code> values in the program are obtained.
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.


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


The monadic operations are defined as follows:
The type of I/O actions is easily defined:
<haskell>
instance Monad ((->) OI)
  where
        return x =  \ u -> let !_ = partOI u in x


        m >>= k =  \ u -> let !(u1, u2) = partOI u
<pre>
                              !x = m u1
type IO a =  OI -> a
                              !y = k x u2 in
      .      .  .  .
                          in y
      |      |  |  |
</haskell>
  an I/O    |  |  |
  action    |  |  |
              |  |  |
  may involve a  |  |
  request to an  |  |
external entity |  |
                |  |
        when being  |
        computed  |
                    |
            to obtain
            a result
</pre>


Note that both methods use their <code>OI</code> parameters, with <code>return</code> simply returning its other parameter <code>x</code> to the caller. The bind operation <code>(>>=)</code> takes an action <code>m</code> and a function <code>k</code> and uses new <code>OI</code> values to call <code>m</code> to obtain <code>x</code>, then call <code>k x</code> to obtain the result <code>y</code>.
As for the monadic interface:
 
Other actions can be declared:


<haskell>
<haskell>
foreign import getChar :: OI -> Char
instance {-# OVERLAPPING #-} Monad ((->) OI) where
foreign import putChar :: Char -> OI -> ()
    return = unitIO
</haskell>
    (>>=) = bindIO
    (>>)  = nextIO


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


<haskell>
bindIO    :: (OI -> a) -> (a -> OI -> b) -> OI -> b
getLine                :: OI -> [Char]
bindIO m k = \ u -> case partOI u of (u1, u2) -> (\ x -> x `pseq` k x u2) (m u1)
getLine                = do c <- getChar
                            if c == ’\n’ then return ""
                                        else do cs <- getLine
                                              return (c:cs)


putStr                :: [Char] -> OI -> ()
nextIO    :: (OI -> a) -> (IO -> b) -> OI -> b
putStr cs              = foldr (\ !(_) -> id) () . zipWith putChar cs . partsOI
nextIO m w = \ u -> case partOI u of (u1, u2) -> m u1 `pseq` w u2
</haskell>
</haskell>


In more fully-featured implementations, each system call would have its own declaration:
<code>Control.Parallel.pseq</code> is needed because <code>Prelude.seq</code> is [[Seq|non]]-sequential, prior evidence to the contrary notwithstanding.
 
<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.


== <span id="readmore"></span> Further reading ==
== <span id="readmore"></span> Further reading ==

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.

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.
Retrieved from "https://wiki.haskell.org/index.php?title=IO_Semantics&oldid=66992"