March 2021
“How to declare an imperative”, Philip Wadler. ACM Computing Surveys, 29(3):240–263, September 1997.
How can we express imperative input/output in a purely-functional language?
Let’s use an embedded domain specific language:
Our initial type of commands is:
For now: ignore the ()-parameter and think of this as an “opaque” type.
Let us consider a function putChar of the following type.
For example,
denotes a command that, if it is ever performed, prints a single question-mark character.
We can build more complex commands from two simpler ones by combining them sequentially.
For example,
denotes a command that, if it is ever performed, prints a question-mark followed by an exclamation mark.
It is useful to have a “null” command that doesn’t do anything.
Note that done doesn’t actually do nothing; it just denotes the command that, if it is ever performed, won’t do anything.
Compare thinking about doing nothing with actually doing nothing — they’re not the same thing!
We can build complex commands from simple ones.
Example: print a string, one character at a time.
For example, putStr "?!" is equivalent to
We could also express putStr using higher-order functions over lists.
E.g.:
putStr "?!"
= foldr (>>) done (map putChar ['?','!'])
= foldr (>>) done [putChar '?', putChar '!']
= putChar '?' >> (putChar '!' >> done)How are commands ever performed?
Answer: the runtime system executes a “special” command named main.
Note that only main is executed even thought there may be other values of type IO () in our program.
In both Haskell and OCaml, the terms
and
are equivalent (both evaluate to 9).
In OCaml print_string : string -> () performs output as a side-effect.
We loose referential transparency, i.e. the ability to exchange identical sub-expressions.
print_string "ah"; print_string "ah"
(* prints "ahah" *)
let x = print_string "ah" in x; x end
(* prints a single "ah" *)
let f () = print_string "ah"
in f (); f () end
(* prints "ahah" *)In Haskell (unlike OCaml), the terms
and
are also equivalent (both denote a command that prints “ahah”).
IO () is the type of commands that return no useful value.
Recall that
()is the unit type with a single inhabitant also written().
More generally, IO a is the type of commands that return a value of type a.
IO Char -- returns a single charater
IO (Char,Char) -- ... a pair of characters
IO Int -- ... a single integer
IO [Char] -- ... a list of charatersA command for reading the next input character:
E.g., if the available input is "abc" then getChar will yield the value 'a' and the input remaining will be "bc".
The command
does nothing and but returns the given value.
E.g. performing
yields the value 42 and leaves the input unchanged.
The operator >>= (pronunced “bind”) combines two commands and passes a value from the first to the second.
For example, performing the command
when the input is "abc" produces the output "A" and the remaning input is "bc".
If
then
is a command that acts as follows:
m yielding x of type ak x yielding y of type byA program to read input until a newline and yield the list of characters read.
getLine :: IO [Char]
getLine = getChar >>= \x ->
if x == '\n' then
return []
else
getLine >>= \xs ->
return (x:xs)The general combinators for commands are:
The command done is a special case of return and >> is a special case of >>=:
The operator >>= behaves similarly to let when the continuation is a lambda expression.
Compare two type rules for let and >>=:
\[ \newcommand{\mbind}{>\!\!>\!=} \newcommand{\of}{::} \begin{array}{l} \Gamma \vdash m \of a \\ \Gamma,\, x\of a \vdash n \of b \\[0.5ex] \hline \Gamma \vdash \text{let}~ x = m ~\text{in}~ n \of b \end{array} \quad \begin{array}{l} \Gamma \vdash m \of \text{IO}~a \\ \Gamma,\, x\of a \vdash n \of \text{IO}~b \\[0.5ex] \hline \Gamma \vdash m \mbind \lambda x \rightarrow n \of \text{IO}~b \end{array} \]
A program that echoes each input line in upper-case.
echo :: IO ()
echo = getLine >>= \line ->
if line == "" then
return ()
else
putStrLn (map toUpper line) >>
echoHere’s the same program using “do” notation.
echo :: IO ()
echo = do {
line <- getLine;
if line == "" then
return ()
else do {
putStrLn (map toUpper line);
echo
}
}Each line “x <- e; ...” becomes “e >>= \x -> ...”.
Each line “e; ...” becomes “e >> ...”.
is equivalent to
A monoid is a pair \((\star,\,u)\) of an associative operator \(\star\) with an identity value \(u\) that satisfy the following laws:
\(u \star x ~=~ x\)
\(x \star u ~=~ x\)
\((x \star y) \star z ~=~ x \star (y \star z)\)
(+) and 0
(*) and 1
(||) and False
(&&) and True
(++) and []
(>>) and done
A monad is a pair of functions (>>=, return) that satisfy the following laws:
return a >>= f \(\quad=\quad\) f a
m >>= return \(\quad=\quad\) m
(m >>= f) >>= g \(\quad=\quad\) m >>= (\x -> f x >>= g)
-- (1) Left identity
do { x'<-return x ; f x' } = do { f x }
-- (2) Right identity
do { x <- m; return x } = do { m }-- (3) Associativity
do { y <- do { x <- m; f x }
g y
}
=
do { x <- m;
do { y <- f x; g y }
}
=
do { x <- m;
y <- f x;
g y
}Monad operations in Haskell are overloaded in a type class.
-- in the Prelude
class Monad m where
return :: a -> m a
(>>=) :: m a -> (a -> m b) -> m b
instance Monad IO where
return = ... -- primitive ops
(>>=) = ...
-- other Monad instancesNB: for something to be a monad it should also satisfy the three monad laws — these are not checked by the compiler!