%-*- mode: Latex; abbrev-mode: true; auto-fill-function: do-auto-fill -*-

%include lhs2TeX.fmt
%include myFormat.fmt

\out{
\begin{code}
-- This code was automatically generated by lhs2tex --code, from the file 
-- HSoM/MUI.lhs.  (See HSoM/MakeCode.bat.)

\end{code}
}

\chapter{Higher-Order Types and Monads}
\label{ch:monads}

\index{type!higher-order} 
\index{type!constructor} 

All of the types that we have considered thus far in this text have
been \emph{first order}.  For example, the type constructor |Music|
has so far always been paired with an argument, as in |Music
 Pitch|.  This is because |Music| by itself is a \emph{type
  constructor}: something that takes a type as an argument and returns
a type as a result.  There are no \emph{values} in Haskell that have
this type, but such ``higher-order types'' can be used in type class
declarations in useful ways, as we shall see in this chapter.

\section{The Functor Class}
\label{sec:functors}

To begin, consider the |Functor| class described previously in
Section~\ref{sec:functor-class}, and defined in the Standard
Prelude:\footnote{The term \emph{functor} (as well as the term
  \emph{monad} to be introduced shortly) comes from a branch of
  abstract mathematics known as \emph{category theory}
  \cite{pierce-ct}.  This reflects the strong mathematical principles
  that underly Haskell, but otherwise does not concern us here; i.e.,
  you do not need to know anything about category theory to understand
  Haskell's functors and monads.}  \indexhs{fmap}
\begin{spec}
class Functor f where
  fmap :: (a -> b) -> f a -> f b
\end{spec}

\syn{Type applications are written in the same manner as function
applications, and are also left associative: the type |T a b| is
equivalent to |((T a) b)|.}

There is something new here: the type variable |f| is applied to other
type variables, as in |f a| and |f b|.  Thus we would expect |f| to be
a \emph{type constructor} such as |Music| that can be applied to an
argument.  Indeed, a suitable instance of |Functor| for |Music| is:
\begin{code}
instance Functor Music where
  fmap f m = mMap f m
\end{code}
Similarly for |Primitive|:
\begin{code}
instance Functor Primitive where
  fmap f p = pMap f p
\end{code}
%% \begin{code}
%% instance Functor Tree where
%%   fmap f (Leaf x)       = Leaf   (f x)
%%   fmap f (Branch t1 t2) = Branch (fmap f t1) (fmap f t2)
%% \end{code}

Indeed, in retrospect, back in Chapter~\ref{ch:more-music} where we
defined |mMap| and |pMap|, we could have declared |Music| and
|Primitive| as instances of |Monad| directly, and avoided defining the
names |mMap| and |pMap| altogether:
\begin{spec}
instance Functor Music where
  fmap f (Prim p)      = Prim (fmap f p)
  fmap f (m1 :+: m2)   = fmap f m1 :+: fmap f m2
  fmap f (m1 :=: m2)   = fmap f m1 :=: fmap f m2
  fmap f (Modify c m)  = Modify c (fmap f m)

instance Functor Primitive where
  pMap               :: (a -> b) -> Primitive a -> Primitive b
  pMap f (Note d x)  = Note d (f x)
  pMap f (Rest d)    = Rest d
\end{spec}

In Haskell we write |Music Pitch| for a |Music| value instantiated on
|Pitch| values; |Music| is the type constructor.  Similarly, we write
|[Int]| for lists instantiated on integers; but what is the type
constructor for lists?  Because of Haskell's special syntax for the
list data type, there is also a special syntax for its type
constructor, namely |[]|.

\syn{Similarly, for tuples the type constructors are |(,)|, |(,,)|,
  |(,,,)|, and so on, and the type constructor for the function type
  is |(->)|.  This means that the following pairs of types are
  equivalent: |[a]| and |[] a|, |f -> g| and |(->) f g|, |(a,b)| and
  |(,) a b|, and so on.}

This allows us to create an instance of |Functor| for lists, as
follows:
\begin{spec}
instance Functor [] where
  fmap f []      = []
  fmap f (x:xs)  = f x : fmap f xs
\end{spec}
Note the use of |[]| here in two ways: as a value in the list
data type, and as a type constructor as described above.  

Of course, the above declaration is equivalent to:
\begin{spec}
instance Functor [] where
  fmap = map
\end{spec}
where |map| is the familiar function that we have been using since
Chapter \ref{ch:poly}.  This instance is in fact predefined in the
Standard Prelude.

One of the nice things about the |Functor| class, of course, is that
we can now use the same name, |fmap|, for lists, |Music|, and
|Primitive| values (and any other data type for which an instance of
|Functor| is declared).  This could not have been done without
higher-order type constructors, and here demonstrates the ability to
handle generic ``container'' types, allowing functions such as |fmap|
to work uniformly over them.

As mentioned in Section \ref{sec:tc-laws}, type classes often imply
a set of \emph{laws} which govern the use of the operators in the
class.  In the case of the |Functor| class, the following laws are
expected to hold:
\begin{spec}
fmap id       = id
fmap (f . g)  = fmap f . fmap g
\end{spec}

\syn{|id| is the \emph{identity function}, |\x->x|.  Although
|id| is polymorphic, note that if its type on the left-hand side of
the equation above is |a->a|, then its type on the right must be
|t a -> t a|, for some type constructor |t| that is an instance
of |Functor|.}

These laws ensure that the shape of the ``container type'' is
unchanged by |fmap|, and that the contents of the container are not
re-arranged by the mapping function.

\vspace{.1in}\hrule

\begin{exercise}{\em
Verify that the instances of |Functor| for lists, |Primitive|, and
|Music| are law-abiding.}
\end{exercise}

\vspace{.1in}\hrule

\section{The |Monad| Class}
\label{sec:monadic-classes}

There are several classes in Haskell that are related to the notion of
a monad, which can be viewed as a generalization of the principles
that underly IO.  Because of this, although the names of the classes
and methods may seem unusual, these ``monadic'' operations are rather
intuitive and useful for general programming.\footnote{Moggi
  \cite{moggi89} was one of the first to point out the value of monads
  in describing the semantics of programming languages, and Wadler
  first popularized their use in functional programming
  \cite{wadler-popl92,peytonjoneswadler-popl93}.}

There are three classes associated with monads: |Functor| (which we
have discussed already), |Monad| (also defined in the Standard
Prelude), and |MonadPlus| (defined in |Control.Monad|).
\indexamb{Monad}{type class} \indexamb{Monad}{library}

The |Monad| class defines four basic operators: |(>>=)| (often
pronounced ``bind''), |(>>)| (often pronounced ``sequence''),
|return|, and |fail|:
\begin{spec}
class  Monad m  where
    (>>=)   :: m a -> (a -> m b) -> m b
    (>>)    :: m a -> m b -> m b
    return  :: a -> m a
    fail    :: String -> m a

    m >> k  = m >>= \_ -> k
    fail s  = error s
\end{spec}

\syn{The two infix operators above are typeset nicely here; using a
  text editor, you will have to type \verb+>>=+ and \verb+>>+
  instead.}

The default methods for |(>>)| and |fail| define behaviors that
are almost always just what is needed.  Therefore most instances of
|Monad| need only define |(>>=)| and |return|.  

Before studying examples of particular instances of |Monad|, we will
first reveal another secret in Haskell, namely that the |do| syntax is
actually shorthand for use of the monadic operators!  The rules for
this are a bit more involved than those for other syntax we have seen,
but are still straightforward.  The first rule is this:
\begin{spec}
do e ==> e
\end{spec}
So an expression such as |do putStr "Hello World"| is equivalent 
to just \linebreak
|putStr "Hello World"|.  

The next rule is:
\begin{spec}
do e1; e2; ...; en
==> e1 >> do e2 ; ...; en
\end{spec}

For example, combining this rule with the previous one means that:
\begin{spec}
do  writeFile "testFile.txt" "Hello File System"
    putStr "Hello World"
\end{spec}
is equivalent to:
\begin{spec}
writeFile "testFile.txt" "Hello File System" >>
putStr "Hello World"
\end{spec}
Note now that the sequencing of two commands is just the application
of the function |(>>)| to two values of type |IO ()|.  There is
no magic here---it is all just functional programming!  

\syn{What is the type of |(>>)| above?  From the type class
declaration we know that its most general type is:
\begin{spec}
(>>) :: Monad m => m a -> m b -> m b
\end{spec}

However, in the case above, its two arguments both have type 
|IO ()|, so the type of |(>>)| must be:
\begin{spec}
(>>) :: IO () -> IO () -> IO ()
\end{spec}
That is, |m = IO|, |a = ()|, and |b = ()|.  Thus the type of
the result is |IO ()|, as expected.}

The rule for pattern matching is the most complex, because we must
deal with the situation where the pattern match fails:
\begin{spec}
do pat <- e1 ; e2 ; ...; en
==>  let  ok pat  = do e2 ; ...; en
          ok _    = fail "..."
     in e1 >>= ok 
\end{spec}
The right way to think of |(>>=)| above is simply this: it
``executes'' |e1|, and then applies |ok| to the result.  What
happens after that is defined by |ok|: if the match succeeds, the
rest of the commands are executed, otherwise the operation |fail|
in the monad class is called, which in most cases (because of the
default method) results in an |error|.

\syn{The string argument to |error| is a compiler-generated error
message, preferably giving some indication of the location of the
pattern-match failure.}

A special case of the above rule is the case where the pattern |pat|
is just a name, in which case the match cannot fail, so the rule
simplifies to:
\begin{spec}
do x <- e1 ; e2 ; ...; en
==> e1 >>= \x -> do e2 ; ...; en
\end{spec}
The final rule deals with the |let| notation within a |do|
expression:
\begin{spec}
do let decllist ; e2 ; ...; en
==> let decllist in do e2 ; ...; en
\end{spec}
\indexkw{let}
\syn{Although we have not used this feature, note that a |let|
inside of a |do| can take multiple definitions, as implied by the
name |decllist|.}

As mentioned earlier, because you already understand Haskell IO, you
should have a fair amount of intuition about what the monadic
operators do.  Unfortuantely, we cannot look very closely at the
instance of |Monad| for the type |IO|, since it ultimately relies on
the state of the underlying operating system, which we do not have
direct access to other than through primitive operations that
communicate with it.  Even then, these operations vary from system to
system.

Nevertheless, a proper implementation of IO in Haskell is obliged to
obey the following \emph{\indexwd{monad laws}}:
\begin{spec}
return a >>= k           = k a
m >>= return             = m
m >>= (\x -> k x >>= h)  = (m >>= k) >>= h
\end{spec}
The first of these laws expresses the fact that |return| simply
``sends'' its value to the next action.  Likewise, the second law says
that if we immediately return the result of an action, we might as
well just let the action return the value itself.  The third law is
the most complex, and essentially expresses an \emph{associativity}
property for the bind operator |(>>=)|.  A special case of this
law applies to the sequence operator |(>>)|:
\begin{spec}
m1 >> (m2 >> m3)  = (m1 >> m2) >> m3
\end{spec}
in which case the associativity is more obvious.

There is one other monad law, whose purpose is to connect the
|Monad| class to the |Functor| class, and therefore only applies
to types that are instances of both:
\begin{spec}
fmap f xs = xs >>= return . f
\end{spec}
We will see an example of this shortly.

Of course, this law can also be expressed in |do| notation:
\begin{spec}
fmap f xs                  = do x <- xs ; return (f x)
\end{spec}
as can the previous ones for |do|:
\begin{spec}
do x <- return a ; k x      = k a
do x <- m ; return x        = m
do x <- m ; y <- k x ; h y  = do y <- (do x <- m ; k x) ; h y
do m1 ; m2 ; m3             = do (do m1 ; m2) ; m3
\end{spec}
So something like this:
\begin{spec}
do  k <- getKey w
    return k
\end{spec}
is equivalent to just |getKey w|, according to the second law above.
As a final example, the third law above allows us to transform this:
\begin{spec}
do  k <- getKey w
    n <- changeKey k
    respond n
\end{spec}
into this:
\begin{spec}
let keyStuff = do  k <- getKey w
                   changeKey k
in do  n <- keyStuff
       respond n
\end{spec}

\vspace{.1in}\hrule

\begin{exercise}{\em
Verify the associativity law for |(>>)|, starting with the
associativity law for |(>>=)|.}
\end{exercise}

\vspace{.1in}\hrule

\subsection{Other Instances of Monad}
\label{monad-instances}

\paragraph*{|Maybe|}
\indexhs{Maybe}

In addition to |IO|, the Standard Prelude's |Maybe| data type is
a predefined instance of |Monad|:
\begin{spec}
instance Monad Maybe where
    Just x   >>= k   = k x
    Nothing  >>= k   = Nothing
    return           = Just
    fail s           = Nothing
\end{spec}
\syn{|Maybe| is also a predefined instance of |Functor|:
\begin{spec}
instance Functor Maybe  where
    fmap f Nothing    =  Nothing
    fmap f (Just x)   =  Just (f x)
\end{spec}
}

When used with this instance, the types of the monad operators are:
\begin{spec}
(>>=)   :: Maybe a -> (a -> Maybe b) -> Maybe b
return  :: a -> Maybe a
\end{spec}
We leave as an exercise the task of proving that this instance is
law-abiding.

To see how this might be used, consider a computation involving
functions |f :: Int -> Int|, |g :: Int -> Int|, and 
|x :: Int|:
\begin{spec}
g (f x)
\end{spec}
Now suppose that each of the calculations using |f| and |g|
could in fact be erroneous, and thus the results are encoded using the
|Maybe| data type.  Unfortunately this can become rather tedious to
program, since each result that might be an error must be checked
manually, as in:
\begin{spec}
case (f x) of 
  Nothing  -> Nothing
  Just y   -> case (g y) of
                Nothing  -> Nothing
                Just z   -> z
\end{spec}
Alternatively, we could take advantage of |Maybe|'s membership in
the |Monad| class, and convert this into monadic form:
\begin{spec}
f x  >>= \y ->
g y  >>= \z ->
return z
\end{spec}
Or, using the more familiar |do| notation:
\begin{spec}
do  y  <- f x
    z  <- g y
    return z
\end{spec}
Thus the tedium of the error check is ``hidden'' within the monad.  In
this sense monads are a good example of the abstraction principle in
action (pardon the pun)!

It is also worth noting the following simplification:
\begin{spec}
f x  >>= \y ->
g y  >>= \z ->
return z
==> { currying simplification }
f x >>= \y ->
g y >>= return 
==> { monad law for return }
f x >>= \y ->
g y
==> { currying simplification }
f x >>= g
\end{spec}
So we started with |g (f x)| and ended with |f x >>= g|; this is
not too bad considering the alternative that we started with!

For an even more pleasing result, we can define a monadic composition
operator:
\indexhs{composeM}
\begin{spec}
composeM :: Monad m => (b -> m c) -> (a -> m b) -> (a -> m c)
(g `composeM` f) x = f x >>= g
\end{spec}
in which case we started with |(g . f) x| and ended with 
|(g `composeM` f) x|.  

\syn{Note the type of |composeM|.  It demonstrates that
higher-order type constructors are also useful in type signatures.}

%% \vspace{.1in}\hrule

%% \begin{exercise}{\em
%% Recall in Section \ref{sec:picture-interaction} the use of the
%% |Maybe| data type in the function |adjust|.  Rewrite this
%% function using monadic operations.}
%% \end{exercise}

%% \vspace{.1in}\hrule

\paragraph*{Lists}

The list data type in Haskell is also a predefined instance of class
|Monad|:
\begin{spec}
instance  Monad []  where
    m >>= k   =  concat (map k m)
    return x  =  [x]
    fail x    =  [ ]
\end{spec}
\syn{Recall that |concat| takes a list of lists and concatenates them
  all together.  It is defined in the Standard Prelude as:
\begin{spec}
concat :: [[a]] -> [a]
concat xss = foldr (++) [] xss
\end{spec}
}

The types of the monadic operators in this case are:
\begin{spec}
(>>=)  :: [a] -> (b -> [b]) -> [b]
return :: a -> [a]
\end{spec}
The monadic functions in this context can be thought of as dealing
with ``multiple values.''  Monadic binding takes a set (list) of
values and applies a function to each of them, collecting all
generated values together.  The |return| function creates a
singleton list, and |fail| an empty one.  For example,
\begin{spec}
do  x <- [1,2,3]
    y <- [4,5,6]
    return (x,y)
\end{spec}
returns the list:
\begin{spec}
[(1,4),(1,5),(1,6),(2,4),(2,5),(2,6),(3,4),(3,5),(3,6)]
\end{spec}
which happens to be the same list generated by:
\begin{spec}
[(x,y) | x <- [1,2,3], y <- [4,5,6]]
\end{spec}
\index{list comprehension}
So list comprehension syntax is in essence another kind of monad
syntax; indeed, they are not very different!  (However, list
comprehensions can only be used with lists.)

% The existence of list comprehensions in Haskell is why the list data
% type is not predefined as an instance of |Monad|.

Note that if:
\begin{spec}
do x <- xs ; return (f x)
\end{spec}
is equivalent to:
\begin{spec}
[ f x | x <- xs ]
\end{spec}
(which is clearly just |map f xs|), then at least for the instance of
lists in |Monad|, the last monad law makes perfect sense:
\begin{spec}
fmap f xs = do x <- xs ; return (f x)
\end{spec}
Also note that the |Maybe| data type in monadic form behaves as a
sort of truncated list in monadic form: |Nothing| is the same as
|[]| and |Just x| is the same as |[x]|.)

\vspace{.1in}\hrule

\begin{exercise}{\em
Verify that all of the instance declarations in this section are
law-abiding.}
\end{exercise}

\begin{exercise}{\em
Consider the \emph{identity data type} defined by:
\begin{spec}
data Id a = Id a
\end{spec}
Create an instance of |Monad| for |Id|, and prove that it is
law-abiding.}
\end{exercise}

\vspace{.1in}\hrule

\subsection{Other Monadic Operations}
\label{sec:other-monadic-ops}

The Standard Prelude has several functions specifically designed for
use with monads; they are shown in Figure \ref{fig:monad-utilities}.
Indeed, one of these we have already used: |sequence_|.  Any
mystery about how it works should be gone now; it is a very simple
fold of the sequencing operator |(>>)|, with |return ()| at the
end.  Note also the definition of |sequence|, a generalization of
|sequence_| that returns a list of values of the intermediate
results.
\indexhs{sequence}
\indexhs{sequence\_}
\indexhs{mapM}
\indexhs{mapM\_}
\indexhs{(=<<)}

Finally, recall from Section \ref{sec:actions-are-value} that |putStr|
can be defined as:
\begin{spec}
putStr    :: String -> IO ()
putStr s  = sequence_ (map putChar s)
\end{spec}
Using |mapM_| from Figure \ref{fig:monad-utilities}, this can be
rewritten as:

\indexhs{putStr}
\begin{spec}
putStr    :: String -> IO ()
putStr s  = mapM_ putChar s
\end{spec}

\begin{figure}
\cbox{
\begin{spec}
sequence   :: Monad m => [m a] -> m [a] 
sequence   =  foldr mcons (return [])
                where mcons p q = do  x   <- p
                                      xs  <- q
                                      return (x:xs)

sequence_  :: Monad m => [m a] -> m () 
sequence_  =  foldr (>>) (return ())

mapM       :: Monad m => (a -> m b) -> [a] -> m [b]
mapM f as  =  sequence (map f as)

mapM_      :: Monad m => (a -> m b) -> [a] -> m ()
mapM_ f as =  sequence_ (map f as)

(=<<)      :: Monad m => (a -> m b) -> m a -> m b
f =<< x    =  x >>= f
\end{spec}}
\caption{Monadic Utility Functions}
\label{fig:monad-utilities}
\end{figure}

\section{The MonadPlus Class}
\label{sec:monad-plus}

The class |MonadPlus|, defined in the Standard Library
|Control.Monad|, is used for monads that have a \emph{zero element}
and a \emph{plus operator}: \indexhs{mzero} \indexhs{mplus}
\begin{spec}
class Monad m => MonadPlus m  where
  mzero  :: m a
  mplus  :: m a -> m a -> m a
\end{spec}
The zero element should obey the following laws: 
\begin{spec}
m >>= (\x -> mzero)  = mzero
mzero >>= m          = mzero
\end{spec}
and the plus operator should obey these:
\begin{spec}
m `mplus` mzero  = m
mzero `mplus` m  = m
\end{spec}
By analogy to arithmetic, think of |mzero| as 0, |mplus| as
addition, and |(>>=)| as multiplication.  The above laws should
then make more sense.

For the |Maybe| data type, the zero and plus values are:
\begin{spec}
instance MonadPlus Maybe where
    mzero                  = Nothing
    Nothing  `mplus` ys    = ys
    xs       `mplus` ys    = xs
\end{spec}
and for lists they are:
\begin{spec}
instance  MonadPlus []  where
    mzero  = []
    mplus  = (++)
\end{spec}
So you can see now that the familiar concatentation operation
|(++)| that we have been using all along for lists is just a
special case of the |mplus| operator.

It is worth pointing out that the IO monad is not an instance of the
|MonadPlus| class, since it has no zero element.  For if it did
have a zero element, then the IO action |putStr "Hello" >> zero|
should \emph{not} print the string |"Hello"|, according to the first
zero law above.  But this is counter-intuitive, or at least is
certainly not what the designers of Haskell had in mind for IO.

The |Monad| module in the Standard Library also includes several
other useful functions defined in terms of the monadic primitives.
You are encouraged to read these for possible use in your own
programs.

\vspace{.1in}\hrule

\begin{exercise}{\em
Verify that the instances of |MonadPlus| for the |Maybe| and
list data types are law-abiding.}
\end{exercise}

\vspace{.1in}\hrule

\section{State Monads}
\label{sec:state-monads}
\index{state monad}

Monads are commonly used to simulate stateful, or imperative,
computations, in which the details of updating and passing around the
state are hidden within the mechanics of the monad.  Generally
speaking, a \emph{state monad} has a type of the form:
\begin{spec}
data SM s a = SM (s -> (s,a))
\end{spec}
where |s| is the state type, and |a| is the value type.  The instance
of this type in |Monad| is given by:
\begin{spec}
instance Monad (SM s) where
  return a    
    = SM $ \s0 -> (s0,a)
  SM sm0 >>= fsm1
    = SM $ \s0 ->
        let  (s1,a1)  = sm0 s0
             SM sm1   = fsm1 a1
             (s2,a2)  = sm1 s1
        in (s2,a2)
\end{spec}
The last equation in the |let| expression could obviously be
eliminated, but it is written this way to stress the symmetry in the
treatment of the two commands.

\syn{Note that |SM| is a type constructor that takes \emph{two} type
  arguments.  Applyiing it to one argument (as in |SM s| above) is a
  kind of type-level currying, yielding a new type constructor that
  takes one argument, as required by the |Monad| class.}

A good example of a state monad, at least abstractly speaking, is
Haskell's |IO| type, where the state |s| can be thought of as the
``state of the world,'' such as the contents of the file system, the
image on a display, and the output of a printer.

But what about creating our own state monad?  As a simple example,
consider this definition of a |Tree| data type:
\begin{spec}
data Tree a = Leaf a | Branch (Tree a) (Tree a)
     deriving Show
\end{spec}
Suppose now we wish to define a function |label :: Tree a -> Tree
Int| such that, for example, the value |test|:
\begin{spec}
test = let t = Branch (Leaf 'a') (Leaf 'b')
       in label (Branch t t)
\end{spec}
evaluates to:
\begin{spec}
Branch  (Branch (Leaf 0) (Leaf 1)) 
        (Branch (Leaf 2) (Leaf 3))
\end{spec}
Without knowing anything about monads, this job is relatively easy:
\begin{spec}
label    :: Tree a -> Tree Int
label t  = snd (lab t 0)

lab :: Tree a -> Int -> (Int, Tree Int)
lab (Leaf a) n 
    = (n+1, Leaf n)
lab (Branch t1 t2) n
    =  let  (n1,t'1)  = lab t1  n
            (n2,t'2)  = lab t2 n1
       in   (n2, Branch t'1 t'2)
\end{spec}
Although simple, there is an undeniable tedium in ``threading'' the
value of |n| from one call to |lab| to the next.  To solve this
problem, note that |lab t| has type |Int -> (Int, Tree Int)|, which is
in the right form for a state monad.  Of course, we need a true data
type, and so we write:
\begin{spec}
newtype Label a = Label (Int -> (Int,a))
\end{spec}

\syn{A |newtype| declaration behaves just like a |data| declaration,
  except that only one constructor is allowed on the right-hand side.
  This allows the compiler to implement the datatype more efficiently,
  since it ``knows'' that only one possibility exists.  It is also
  more type-safe than a type synonym, since, like |data|, it generates
  a new type, rather than being a synonym for an existing type.}

The |Monad| instance for |Label| is just like that for |SM| above:
\begin{spec}
instance Monad Label where
  return a         
    = Label $ \s -> (s,a)
  Label lt0 >>= flt1
    = Label $ \s0 ->
        let  (s1,a1)    = lt0 s0
             Label lt1  = flt1 a1
        in lt1 s1
\end{spec}

Whereas the monad handles the threading of the state, we also need a
way to extract information from the state, as needed in a particular
application.  In the case of labeling trees, we need to know what the
current value of the state (an |Int|) is, at each point that we
encounter a leaf.  So we define:
\begin{spec}
getLabel :: Label Int
getLabel = Label $ \n -> (n+1,n)
\end{spec} % $

Now we can write the following monadic version of the labeling
function:
\begin{spec}
mlabel :: Tree a -> Tree Int
mlabel t =  let Label lt = mlab t
            in snd (lt 0)

mlab :: Tree a -> Label (Tree Int)
mlab (Leaf a)
     = do  n <- getLabel
           return (Leaf n)
mlab (Branch t1 t2)
     = do  t'1 <- mlab t1
           t'2 <- mlab t2
           return (Branch t'1 t'2)
\end{spec}
Note that the threading of the state has been completely eliminated
from |mlab|, as has the incrementing of the state, which has been
isolated in the function |getLabel|.

As an example, this test case:
\begin{spec}
mtest =  let t = Branch (Leaf 'a') (Leaf 'b')
         in mlabel (Branch t t)
\end{spec}
generates the same result as the non-monadic version above.

For this simple example you may decide that eliminating the threading
of state is not worth it.  Indeed, in reality it has just been moved
from the definition of |lab| to the method declaration for |(>>=)|,
and the new version of the program is certainly longer than the old!
But the capture of repetitious code into one function is the whole
point of the abstraction principle, and hopefully you can imagine a
context where threading of state happens often, perhaps hundreds of
times, in which case the abstraction will surely pay off.  IO is one
example of this (imagine threading the state of the world on every IO
command).

\vspace{.1in}\hrule

\begin{exercise}{\em
Recall the definition of |replFun| in Chapter~\ref{lsystems},
Section~\ref{sec:musical-lsystem}.  Note how it threads the random
number source through the program.  Rewrite this function using a
state monad so that this threading is eliminated. }
\end{exercise}

\vspace{.1in}\hrule

\section{Type Class Type Errors}
\label{sec:class-reasoning}

As you know, Haskell's type system detects ill-typed expressions.  But
what about errors due to malformed types?  The value |(+) 1 2 3|
results in a type error since |(+)| takes only two arguments.
Similarly, the type |Tree Int Int| should result in some sort of an
error since the |Tree| type constructor takes only a single argument.
So, how does Haskell detect malformed types?  The answer is a second
type system which ensures the correctness of types!  That is, each
type is assigned its own type---which is called its \emph{kind}---and
these \indexwd{kinds} are used to ensure that the type is used
correctly.

There are only two kinds that we need to consider:
\begin{itemize}
\item The symbol $\ast$ represents the kind of type associated with
concrete data objects.  That is, if the value |v| has type |t|,
then the kind of |t| must be $\ast$.

\item If $\kappa_1$ and $\kappa_2$ are kinds, then
$\kappa_1\rightarrow\kappa_2$ is the kind of types that take a type of
kind $\kappa_1$ and return a type of kind $\kappa_2$.
\end{itemize}
The details of how kinds are used to detect malformed types are beyond
the scope of this text, but it is helpful to walk through a familiar
example:

|Int| has kind $\ast$, as does the type |Tree Int|.  The type
constructor |Tree|, however, has kind $\ast\rightarrow\ast$.
Instances of the |Functor| class must all have the kind
$\ast\rightarrow\ast$.  Thus a kind error would result from a
declaration such as:
\begin{spec}
instance Functor Int where ...
\end{spec}
or
\begin{spec}
instance Functor (Tree Int) where ...
\end{spec}
Kinds do not appear directly in Haskell programs; the Haskell system
infers them without any need for ``kind declarations.''  Kinds stay in
the background of a Haskell program except when a kind error occurs,
in which case an error message may refer to the kind conflict.
Fortunately, kinds are simple enough that your Haskell system should
be able to provide descriptive error messages in most cases.