### Yet Another Monad Tutorial (part 7: state monads)

In this article we'll look at a very interesting class of monads: state monads.

## The `State`

monad

Up to this point, our approach has consisted of taking an existing type
constructor, showing how it could be used as a monad (*i.e* to represent some
kind of function-with-other-effects), and then deriving the monad instance using
a combination of plausible arguments and the three monad laws. In this section,
we'll have to create the type constructor from scratch, which will involve a
little extra work.

The basic idea of a state monad is to allow us to represent functions which interact with local state variables (which are just called local variables in most languages), or global state variables (usually called global variables). Essentially, they allow us to simulate some aspects of imperative programming in a purely functional setting.

Why would we want to do this? Programmers who come to functional languages from
an imperative language background (which means, nearly all programmers) are used
to writing code in which state manipulations happen on almost every line. As
one gets used to functional programming, one realizes that a great deal of this
state manipulation is unnecessary. Nevertheless, some kinds of code are simply
more convenient to write with explicit state manipulation (*i.e.* in an
imperative style). Using a state monad can simplify such code tremendously by
letting us hide the state manipulation, only calling it forth when needed. We
will see later on that there are other ways to simulate imperative programming
idioms in Haskell (notably, in the `IO`

monad using `IORefs`

and `IOArrays`

),
but using state monads is still a common approach when the number of stateful
items being passed around is small.

To start with, let's think about how we could handle this without monads. We have our function-with-effects, which we can write schematically as follows:

```
a --[access/modify state variables]--> b
```

The function takes in a value of type `a`

, may access and/or modify some state
variables, and then returns a value of type `b`

.

We will assume that this function will have a fixed number of state variables.
We can collect all of them into a tuple type which we will call `s`

(for
"state"). These state variables will have to get passed along as extra
arguments to the function. The type signature of this function will look like
this:

```
(a, s) -> (b, s)
```

This is a pure function. It accepts a tuple of the state (of type `s`

) plus the
input value (of type `a`

) as its input and outputs a tuple of the state (still
of type `s`

, though the values of the components may be different) and the
output value (of type `b`

). This approach to modeling state in a purely
functional language is called "threading the state". Writing functions in this
manner is perfectly straightforward, though often quite tedious (in much the
same way that writing functions returning `Maybe`

values is straightforward and
often tedious, as we saw in part 4 of this series). We will use a state monad
to make it easier to write these functions (essentially by handling all of the
threading of the state "under the surface").

The function's type signature (`(a, s) -> (b, s)`

) is not in the form of a
monadic function, so we will have to massage it a bit to make it into one.
Let's start by recalling what I previously said about currying. We can unpack a
tuple of two arguments into two separate arguments to get this:

```
a -> s -> (b, s)
```

This is not the same type signature as the previous one, but it can represent the same kinds of functions.

Now let's add some parentheses:

```
a -> (s -> (b, s))
```

This is exactly the same type signature as the previous one (the arrow (`->`

)
associates to the right), but I'm using the extra parentheses to highlight that
this function takes a value of type `a`

and returns a value which is a function
of type `(s -> (b, s))`

. We'll call functions with the type signature ```
(s ->
(b, s))
```

"state transformer functions"; they take a state tuple as input and
return an updated state tuple, along with a return value of type `b`

.

We still don't have what we need. Our monadic function must have a type of the form:

```
a -> m b
```

for some type constructor `m`

. We don't have a type constructor here, just a
function type of the form `(s -> (b, s))`

. This function type depends on two
type parameters (`s`

and `b`

), so we can define a type constructor called
`State`

with two type parameters as follows:

```
data State s b = State (s -> (b, s))
```

Values of this data type will be the monadic values for our state monads. I will also be calling these monadic values "state transformers", by which I mean they are values which contain a state transformer function.

`State`

is a type constructor which (unlike `Maybe`

or the list type
constructor, but like the `Either`

type constructor we saw in the previous two
articles) takes *two* type arguments (the state `s`

and the output type `b`

).
This will turn out to be very important. I also want to point out that there
are two distinct uses of the word `State`

in the definition; the leftmost
`State`

refers to the type constructor called `State`

while the rightmost
`State`

is a value constructor (for an algebraic data type with a single
constructor). Don't confuse type constructors and value constructors; they are
completely different things! In Haskell, the namespace for value constructors
is completely distinct from the namespace for types and type constructors, so
this doesn't confuse Haskell (though it's been known to confuse programmers,
yours truly included). It would be clearer to write this as *e.g.*

```
data State s b = StateC (s -> (b, s))
```

where `StateC`

means "`State`

value constructor", but alas, that's not the way
it's done in the Haskell libraries. I think it's best to stick with the real
version instead of inventing my own. By the way, in GHC you can find the
`State`

monad in the module `Control.Monad.State`

. (There is also a distinction
between lazy and strict state monads which I am going to completely ignore,
because this section is complicated enough already.)

Side note:The actual definition of the`State`

data type in the GHC libraries is a bit different:`newtype State s b = State (s -> (b, s))`

The meaning is the same.

`newtype`

is used with single-constructor classes because the compiler can generate more efficient code with a`newtype`

declaration than with a`data`

declaration, for reasons that do not concern us here.

The bottom line is this: in the `State`

monad, the monadic values represent
*functions*, which are state transforming functions of the form `(s -> (b, s)`

for some state type `s`

. In a particular computation in the `State`

monad, the
state type `s`

will be constant but the value type `b`

may change at every
step.

I want to pause and let this sink in. Previously, I told you that monadic
values were weird in that they were values that could be thought of as being
like functions (a lot of Haskell literature uses the term "action" and I even
used the term "undercover function" at one point). I used the analogy that a
monadic value of type `m b`

is similar to a monadic function of type ```
() -> m
b
```

. That's a reasonable way to think about monadic values, but state monadic
values offer the additional confusion of actually *being* functions — they
contain state transforming functions with the type `s -> (b, s)`

. If I pursued
my analogy I would say that state monadic values are kind of like state monadic
functions of type `() -> State s b`

, which means that they would in effect be
like functions of type `((), s) -> (b, s)`

. This is not significantly different
from functions of type `s -> (b, s)`

; you would of course have to use the
function differently but it maps the same kinds of inputs to the same kinds of
outputs. With other kinds of monads, we can think of the monadic values as
being "kind of like" functions that have some effect and return some value, but
with state monadic values, they really *are* functions that have some effect
(changing the state) and return some value. Or to be completely precise, they
are data that contain such functions. This makes it more difficult to keep the
explanations simple, but I'll do my best.

Let's show what the definition of the `State`

type and constructor mean with an
example. Assume that you have a function that will convert an input value of
type `String`

to an output value also of type `String`

. Assume that you have
two state items you are passing around, one of type `Int`

and one of type
`Float`

. So your state has the type `(Int, Float)`

(a two-tuple consisting of
an `Int`

and a `Float`

). Let's say you have a function `foo`

that looks like
this:

```
foo :: (String, (Int, Float)) -> (String, (Int, Float))
foo (a, st) = {- some expression involving a and the state tuple st -}
```

We could curry the initial `(String, (Int, Float))`

tuple into two separate
arguments (one representing the input value (of type `String`

), the other the
initial values of the state (of type `(Int, Float)`

)) and write a new version of
this function as:

```
foo' :: String -> (Int, Float) -> (String, (Int, Float))
foo' a st = {- some expression involving a and the state tuple st -}
```

We can rewrite this definition slightly to give:

```
foo' :: String -> (Int, Float) -> (String, (Int, Float))
foo' a = \st -> {- some expression involving a and the state tuple st -}
```

All we've done here is move the state argument to the right-hand side as an explicit lambda expression. We can make one more change:

```
foo'' :: String -> State (Int, Float) String
foo'' a = State (\st -> {- some expression involving a and the state tuple st -})
```

What we are doing here is packaging the right-hand side of the function `foo'`

into a data value of type `State (Int, Float) String`

using the `State`

constructor (or `StateC`

if we were using that). The good thing about this is
that `foo''`

is a monadic function, and the expression

```
State (\st -> {- some expression involving a and the state tuple st -})
```

will be a monadic value of type `State (Int, Float) String`

. But somehow, there
must be a mapping between `State (Int, Float) String`

and `m b`

for the general
case of a monadic function. If `b`

is just `String`

in this case, then the
monad `m`

is `State (Int, Float)`

. `State (Int, Float)`

is a partially applied
type constructor (just like `Either e`

for some error type `e`

is a partially
applied type constructor; we saw this in the previous two articles). You can
think of it as being like a "curried" type constructor; you apply the
two-argument `State`

type constructor to a single type argument (the tuple
`(Int, Float)`

) to get a one-argument type constructor. And, as we know, a
`Monad`

instance has to be a one-argument type constructor. In general, for a
state type `s`

, we have monadic functions of the form

```
a -> State s b
```

which could alternatively be written

```
a -> (State s) b
```

and the `Monad`

instance is thus `State s`

. From this we can see that there is
a whole family of `State`

monads, not just one (in contrast to the `Maybe`

and
list monads, but like the `Either e`

monad). There is one specific `State`

monad instance for every distinct state type `s`

. So we don't speak of *the*
`State`

monad, but *a* `State`

monad. Fortunately, though, the same definition
of the monadic operators/functions (`>>=`

and `return`

) will suffice for all
`State`

monads. The definition looks like this in skeletal form:

```
instance Monad (State s) where
mv >>= f = {- definition of >>= for state monads -}
return x = {- definition of return for state monads -}
```

Now we come to the unenviable task of deriving the definitions of `>>=`

and
`return`

for state monads. We'll define them based on what we want the monad to
do for us, and then we'll use the monad laws to check that everything behaves
correctly. **Warning**: this will get a bit complicated.

We'll start by deciding what we want our state monad to do. Like any monad, the
point of a state monad is to allow us to compose monadic functions in a
"reasonable" way. So let's say, for a given state type `s`

, we want to compose
these functions:

```
f :: a -> (State s) b
g :: b -> (State s) c
```

to give:

```
h :: a -> (State s) c
```

What does this mean? If you ignore the state, the implication is clear: `f`

converts a value of type `a`

to a value of type `b`

, which gets passed to `g`

,
which converts the value of type `b`

to a value of type `c`

. So `h`

converts a
value of type `a`

to a value of type `c`

. But in addition to this, either of
the functions `f`

and `g`

can access and/or modify the state value (of type
`s`

), and (this is the critical part) the initial state value that `g`

will see
is the *final* state value of `f`

*i.e.* the state value that exists once `f`

has finished all of its modifications of *its* initial state value. So `h`

starts off with the same initial state value as `f`

, and once it's finished the
state value is the same as the final state value of `g`

.

This is easier to see if we rewrite these functions in a non-monadic form, with explicit state threading:

```
f' :: (a, s) -> (b, s)
g' :: (b, s) -> (c, s)
h' :: (a, s) -> (c, s)
```

We can easily define `h'`

as follows:

```
h' (x, st) =
let (y, st') = f' (x, st)
(z, st'') = g' (y, st') -- initial state of g' = final state of f'
in (z, st'')
```

Or, more simply, as:

```
h' (x, st) = let (y, st') = f' (x, st) in g' (y, st')
```

In words, we pass the original state and input value to the function `f'`

, get
the resulting state/value pair, pass that to the function `g'`

and return the
final state/value pair. The state gets passed from function to function just
like any other function argument.

We could even write out `h'`

as:

```
h' = g' . f'
```

but we'll stick to the expanded form for clarity. You might wonder, though, why
we bother with state monads if you can just chain together these functions using
regular function composition. The reason is that in many cases, explicitly
threading the state is much grungier and less clear than using a state monad.
This is similar to the case with the `Maybe`

, list, and error monads, where one
can always write the code non-monadically, but it's usually cleaner to do it
monadically.

In the monadic version, using the monadic functions `f`

, `g`

, and `h`

instead of
`f'`

, `g'`

, and `h'`

, we can define `h`

as simply:

```
h = f >=> g
```

using the monadic composition operator `>=>`

. Expanding this out into the
equivalent form using the `>>=`

operator, we have:

```
h x = f x >>= g
```

Or, equivalently:

```
h x = f x >>= \y -> g y
```

With the `do`

notation, this becomes:

```
h x = do y <- f x
g y
```

All the last three forms are equivalent; we can use whichever one we find most convenient. The interesting thing about them is that the state is never seen; it's passed from function to function "under the surface" due to the monadic machinery. In the last version, we interpret the function as follows:

Compute

`f x`

; this may change the (hidden) state and will yield the value`y`

.Compute

`g y`

; this may change the (hidden) state and will return the final monadic value.

Aside from defining what the bind operator `>>=`

means for state monads (we're
getting to that!), there is one other thing we need before we can actually
compute something from a state monadic computation. What state monads allow us
to do is to chain state-transforming functions together to get one composite
state-transforming function (like the way `f'`

and `g'`

combine to form `h'`

),
but you can't get a value out of the resulting state-transforming function
unless you (a) give it an input value (this is like any function), and (b) give
it an initial state. When you just provide an input value (like `h x`

above),
you end up with a (state) monadic value, which is of the form:

```
State (s -> (b, s))
```

for some state type `s`

and some return type `b`

. So what you've computed isn't
the final result, but a state transformer function which will give you the final
result once you give it the initial state. To get the final result value (of
type `b`

), you thus have to pass the initial state to the state transformer
function of type `(s -> (b, s))`

, and get the resulting value of type `(b, s)`

,
which is a tuple of the final result and the final state. The
`Control.Monad.State`

module defines some useful functions for computing results
from a state monadic value:

```
runState :: State s a -> s -> (a, s)
runState (State f) init_st = f init_st
evalState :: State s a -> s -> a
evalState mv init_st = fst (runState mv init_st)
execState :: State s a -> s -> s
execState mv init_st = snd (runState mv init_st)
```

where `mv`

is a state monadic value, and `fst`

and `snd`

are functions which
extract the first and second elements of a 2-tuple respectively. Each of these
functions take a state monadic value as well as the initial state `init_st`

as
arguments. `runState`

returns the final (value, state) tuple; `evalState`

returns the final result (output value) only while `execState`

returns the final
state only.

The way you do computations in the state monad is that you chain together
however many monadic functions you want (generally using the `do`

notation, or
using the `>>=`

operator if you prefer). These all have the type signature ```
a
-> State s b
```

for some types `a`

, `b`

(which may be different for each function)
and state type `s`

(which doesn't change). When you have your final state
transformer (a monadic value of type `State s b`

, which as we've seen is a
wrapper around a state transformer function with the type `s -> (b, s)`

), you
then pass the initial state to it to get the final result. This result is a
tuple of the final output value (of type `b`

) and the final output state (of
type `s`

), from which you can extract whichever component(s) you want.

When you think about it, this is not that different from what a function in the C programming language does with its local variables. In C, you are implicitly passing around an array of all the local variables behind the scenes, and each line that interacts with any local variables can be viewed as a tiny state transformer which extracts and/or sets the values of some local variables. To get the entire function you chain together all of these tiny state transformers to get a composite state transformer, which you initialize with the set of initial values of the local variables. The main conceptual difference between C's local variables and Haskell's state monads is that Haskell is much more explicit about this process; if you want to use that style of programming in Haskell, you have to ask for it by creating and using state monadic values and functions.

With that said, let's get back to the definitions of `>>=`

and `return`

for the
`State`

monad. We'll start with `>>=`

, and we'll make sure that our definition
works the same way as we saw above when combining the non-monadic functions `f'`

and `g'`

to get `h'`

.

### Deriving the `>>=`

operator

Recall the definition of `h'`

given above:

```
h' (x, st) =
let (y, st') = f' (x, st)
in g' (y, st')
```

This equation shows how non-monadic state-transforming functions `f'`

and `g'`

compose to give the non-monadic state-transforming function `h'`

. Recall that
`f'`

, `g'`

and `h'`

have the types:

```
f' :: (a, s) -> (b, s)
g' :: (b, s) -> (c, s)
h' :: (a, s) -> (c, s)
```

for some input/output types `a`

and `b`

, and a state type `s`

. The challenge is
to rewrite this definition in a monadic form.

If you know what `f'`

, `g'`

and `h'`

are, it's easy to write monadic versions of
these functions. Let's start with `f'`

:

```
f' :: (a, s) -> (b, s)
f' (x, st) = {- body of f' -}
```

We could write a curried version of this trivially as follows:

```
f'' :: a -> s -> (b, s)
f'' x st = f' (x, st)
```

Let's rewrite this slightly:

```
f'' :: a -> s -> (b, s)
f'' x = \st -> f' (x, st)
```

And now let's wrap the right-hand side (which has the type `(s -> (b, s))`

) in a
`State`

constructor (which takes a single value of type `(s -> (b, s))`

as its
argument):

```
f :: a -> State s b
f x = State (\st -> f' (x, st))
```

This is a monadic function; specifically, it's the monadic version of `f'`

.
Similarly, we can easily get the monadic versions of `g'`

and `h'`

:

```
g :: b -> State s c
g y = State (\st -> g' (y, st))
h :: a -> State s c
h x = State (\st -> h' (x, st))
```

We use `x`

for the argument of `f`

and `h`

and `y`

for the argument of `g`

so
that all `x`

s have type `a`

and `y`

has type `b`

. Of course, we could use any
names we like.

Whatever definition of the `>>=`

operator we select, it has to be such that this
equation is true:

```
h = f >=> g
```

In other words, `h`

must be the monadic composition of `f`

and `g`

. As we know,
we can expand out this definition by using the definition of `>=>`

to put the
equation in terms of the `>>=`

operator:

```
h x = f x >>= g
```

The question now becomes: what does the definition of `>>=`

for state monads
have to be in order to make this work properly? Let's work through the
derivation:

```
f x >>= g = h x
f x >>= g = State (\st -> h' (x, st)) -- definition of h x
f x >>= g = State (\st -> -- definition of h'
let (y, st') = f' (x, st)
in g' (y, st'))
```

Recall the definitions of `f`

and `g`

in terms of `f'`

and `g'`

:

```
f :: a -> State s b
f x = State (\st -> f' (x, st))
g :: b -> State s c
g y = State (\st -> g' (y, st))
```

We can use these definitions to rewrite the right-hand side in terms of `f`

and
`g`

instead of `f'`

and `g'`

as follows:

```
f x >>= g = State (\st ->
let (State ff) = f x -- unpack (f x)
-- n.b. ff == \st -> f' (x, st)
(y, st') = ff st -- ff st == f' (x, st)
(State gg) = g y -- unpack (g y)
-- n.b. gg == \st -> g' (y, st)
in gg st') -- gg st' == g' (y, st')
```

This is a fairly complicated step, but the comments show that the right-hand
side written in terms of `f`

and `g`

is exactly the same as the right-hand side
above written in terms of `f'`

and `g'`

.

Substitute `mv`

for `f x`

to get:

```
mv >>= g = State (\st ->
let (State ff) = mv
(y, st') = ff st
(State gg) = g y
in gg st')
```

This is the correct definition of the `>>=`

operator for state monads. This
definition of `>>=`

for state monads may not seem particularly intuitive, but
the original non-monadic version was quite intuitive: we are just stringing
together two state transforming functions to make a single state-transforming
function. The derivation shows that the monadic version is doing the exact same
thing.

We can use `runState`

to make the definition a bit more concise:

```
mv >>= g = State (\st ->
let (y, st') = runState mv st
in runState (g y) st')
```

This definition is also a bit more intuitive. It says that to apply a monadic
function `g`

(in the `State`

monad) to a monadic value `mv`

(also in the `State`

monad), we apply the monadic value to the initial state `st`

(using `runState`

)
to get a new value `y`

and a new state `st'`

. Then we apply the monadic
function `g`

to the new value `y`

to get another state transformer (monadic
value), which we apply to the new state `st'`

to get the final state/value pair.
Notice, though, that the result is not a state/value pair but a function
(wrapped up as a state monadic value using the `State`

value constructor) which
can generate this state/value pair given the initial state `st`

. OK, maybe this
isn't that much more intuitive, but anyway, the derivation shows you what the
significance of this really is.

### Deriving the `return`

function

As I've mentioned before, the `return`

function for any monad is a monadic
function which is that monad's equivalent of the identity function. For the
state monad, it's not hard to derive this from first principles. Let's look at
the form of a non-monadic state transforming function (like `f'`

, `g'`

and `h'`

above):

```
f' :: (a, s) -> (b, s)
```

We want to have an identity function with this type signature. Let's call it
`id_state`

:

```
id_state :: (a, s) -> (a, s)
```

The type signature of `id_state`

shows that the function takes in a value/state
tuple of type `(a, s)`

and returns a value/state tuple with the same type. The
definition is trivial:

```
id_state :: (a, s) -> (a, s)
id_state (x, st) = (x, st)
```

Now all we need to do to get the `return`

function for the state monad is to
convert `id_state`

into its monadic equivalent. Let's do that in stages.
First, we'll curry the initial value/state tuple:

```
id_state' :: a -> s -> (a, s)
id_state' x st = (x, st)
```

Then, we'll rearrange the definition a bit:

```
id_state' :: a -> (s -> (a, s)) -- add parentheses
id_state' x = \st -> (x, st)
```

This is the same definition as before, written slightly differently. Finally,
we'll wrap the right-hand side in a `State`

value constructor to get a monadic
function which is the correct definition of `return`

for state monads:

```
return :: a -> State s a
return x = State (\st -> (x, st))
```

This definition shows that applying `return`

(in the state monad) to an argument
`x`

creates a state transforming function which doesn't change the state at all,
but which "returns" the value `x`

which was supplied to `return`

in the first
place.

### Verifying the definitions using the monad laws

Now we've derived the definitions of the `>>=`

(bind) operator and the `return`

function for state monads. But I hope that by now you know that there is one
final step we need to perform: we have to verify that our definitions of `>>=`

and `return`

do not violate the monad laws.

#### Monad law 1

Monad law 1 states:

```
-- given: x :: a and g :: a -> State s b
return x >>= g == g x
```

Recall the definition of `>>=`

for state monads:

```
mv >>= g = State (\st ->
let (State ff) = mv
(y, st') = ff st
(State gg) = g y
in gg st')
```

Substituting `return x`

for `mv`

, we get:

```
return x >>= g = State (\st ->
let (State ff) = return x
(y, st') = ff st
(State gg) = g y
in gg st')
```

Expand out the definition of `return`

, using `st''`

for the bound variable
instead of `st`

for clarity:

```
return x >>= g = State (\st ->
let (State ff) = (State (\st'' -> (x, st'')))
(y, st') = ff st
(State gg) = g y
in gg st')
```

Since the first `let`

-binding doesn't depend on the bound variable `st`

, we can
pull it out of the `State`

constructor into a separate `let`

expression:

```
return x >>= g =
let (State ff) = (State (\st'' -> (x, st''))) in
State (\st ->
let (y, st') = ff st
(State gg) = g y
in gg st')
```

The `State`

wrapper in the first `let`

-expression is duplicated on both sides of
the equal sign, so we can remove it:

```
return x >>= g =
let ff = \st'' -> (x, st'') in
State (\st ->
let (y, st') = ff st
(State gg) = g y
in gg st')
```

Substitute the definition of `ff`

and remove the outermost `let`

expression to
get:

```
return x >>= g =
State (\st ->
let (y, st') = (\st'' -> (x, st'')) st
(State gg) = g y
in gg st')
```

Simplify:

```
return x >>= g =
State (\st ->
let (y, st') = (x, st)
(State gg) = g y
in gg st')
return x >>= g = State (\st ->
let (State gg) = g x
in gg st)
```

Lift the `let`

expression out of the right-hand side once again to get:

```
return x >>= g = let (State gg) = g x in
State (\st -> gg st)
```

Change `\st -> gg st`

to just `gg`

(this is called an *eta reduction* in
computer science lingo):

```
return x >>= g = let (State gg) = g x in State gg
```

Simplify again:

```
return x >>= g = g x
```

And we're done (Q.E.D.). That takes care of monad law 1.

#### Monad law 2

Monad law 2 states:

```
-- given: mv :: State s a and return :: a -> State s a
mv >>= return == mv
```

Again, recall the definition of `>>=`

for state monads:

```
mv >>= g = State (\st ->
let (State ff) = mv
(y, st') = ff st
(State gg) = g y
in gg st')
```

Substituting `return`

for `g`

, we have:

```
mv >>= return = State (\st ->
let (State ff) = mv
(y, st') = ff st
(State gg) = return y
in gg st')
```

Substitute the definition of `return`

:

```
mv >>= return = State (\st ->
let (State ff) = mv
(y, st') = ff st
(State gg) = (State (\st'' -> (y, st'')))
in gg st')
```

Remove the `State`

constructor wrapper from the `(State gg) = (State ...)`

binding:

```
mv >>= return = State (\st ->
let (State ff) = mv
(y, st') = ff st
gg = \st'' -> (y, st'')
in gg st')
```

Evaluate `gg st'`

and remove the binding for `gg`

:

```
mv >>= return = State (\st ->
let (State ff) = mv
(y, st') = ff st
in (\st'' -> (y, st'')) st')
```

Simplify:

```
mv >>= return = State (\st ->
let (State ff) = mv
(y, st') = ff st
in (y, st'))
mv >>= return = State (\st ->
let (State ff) = mv
in ff st)
```

Lift the `let`

out of the `State`

constructor:

```
mv >>= return = let (State ff) = mv
in State (\st -> ff st)
```

Convert `\st -> ff st`

to just `ff`

(eta reduction again):

```
mv >>= return = let (State ff) = mv in State ff
```

Simplify again:

```
mv >>= return = mv
```

And we're done (Q.E.D.). Monad law 2 is not violated. Yay.

#### Monad law 3

This derivation is going to be a bit painful. If you skip it, you won't hurt my feelings. But anyway, here we go.

Recall the definition of monad law 3, in terms of the `>>=`

operator:

```
(mv >>= f) >>= g == mv >>= (\x -> (f x >>= g))
```

We have the following types:

```
mv :: State s a
f :: a -> State s b
g :: b -> State s c
```

Here again is the definition of the `>>=`

operator for state monads. I've changed some
of the names, but the meaning is the same; the name changes will make it easier
to keep track of what's what in the derivation.

```
mv >>= f = State (\st1 ->
let (State f1) = mv
(v1, st2) = f1 st1
(State f2) = f v1
in f2 st2)
```

Technical point:In this definition the names we choose for`st1`

,`st2`

,`f1`

,`f2`

, and`v1`

(which are called "bound variables") are completely arbitrary as long as they are different from each other and aren't the same as any other names we are using in the derivation. Sometimes we will choose other names to avoid such name clashes. This renaming is calledalpha-renamingin computer science; this just means that the specific names don't matter as long as we make sure that all names that should be different are different.

We are going to show that with this definition of `>>=`

, monad law 3 is not
violated. The strategy will be to evaluate the left-hand side of monad law 3 as
far as we can go, then do the same for the right-hand side, and show that the
two sides evaluate to the same thing.

Let's start with the left-hand side of monad law 3:

```
(mv >>= f) >>= g
```

Expand `(mv >>= f)`

using the definition of `>>=`

for state monads to get:

```
(State (\st1 ->
let (State f1) = mv
(v1, st2) = f1 st1
(State f2) = f v1
in f2 st2)) >>= g
```

Expand the remaining `>>=`

operator. Use different names for the bound
variables so as not to clash with the previous ones.

```
State (\st3 ->
let (State f3) =
(State (\st1 -> --|
let (State f1) = mv --| this is the previous
(v1, st2) = f1 st1 --| expansion of
(State f2) = f v1 --| mv >>= f
in f2 st2)) --|
(v2, st4) = f3 st3
(State f5) = g v2
in f5 st4
```

Pull the first `let`

-binding out of the outermost `State`

constructor into a
separate `let`

expression:

```
let (State f3) = (State \st1 ->
let (State f1) = mv
(v1, st2) = f1 st1
(State f2) = f v1
in f2 st2)
in
State (\st3 ->
let (v2, st4) = f3 st3
(State f5) = g v2
in f5 st4)
```

Remove the `State`

wrapper from the outer `let`

binding, which is unnecessary:

```
let f3 = \st1 ->
let (State f1) = mv
(v1, st2) = f1 st1
(State f2) = f v1
in f2 st2
in
State (\st3 ->
let (v2, st4) = f3 st3
(State f5) = g v2
in f5 st4)
```

Replace `f3`

with its definition, removing the outermost `let`

in the process
(since it's no longer needed):

```
State (\st3 ->
let (v2, st4) =
(\st1 ->
let (State f1) = mv
(v1, st2) = f1 st1
(State f2) = f v1
in f2 st2) st3
(State f5) = g v2
in f5 st4)
```

Simplify:

```
State (\st3 ->
let (v2, st4) =
let (State f1) = mv
(v1, st2) = f1 st3
(State f2) = f v1
in f2 st2
(State f5) = g v2
in f5 st4)
```

Pull the inner `let`

expression out of the outer `let`

expression:

```
State (\st3 ->
let (State f1) = mv
(v1, st2) = f1 st3
(State f2) = f v1
in
let (v2, st4) = f2 st2
(State f5) = g v2
in f5 st4)
```

Combine the two `let`

expressions into a single `let`

expression:

```
State (\st3 ->
let (State f1) = mv
(v1, st2) = f1 st3
(State f2) = f v1
(v2, st4) = f2 st2
(State f5) = g v2
in f5 st4)
```

Rename some bound variables to get:

```
State (\st1 ->
let (State f1) = mv
(v1, st2) = f1 st1
(State f2) = f v1
(v2, st3) = f2 st2
(State f3) = g v2
in f3 st3)
```

This is the final simplification of the left-hand side of the original equation for monad law 3, applied to state monads. Now let's simplify the right-hand side of the same equation.

We start with the original right-hand side:

```
mv >>= (\x -> (f x >>= g))
```

Expand out the leftmost application of the `>>=`

operator:

```
State (\st1 ->
let (State f1) = mv
(v1, st2) = f1 st1
(State f2) = (\x -> (f x >>= g)) v1
in f2 st2)
```

Reduce the expression `(\x -> (f x >>= g)) v1`

to `(f v1 >>= g)`

(this is just a
normal function application, also known as a *beta reduction*) to get:

```
State (\st1 ->
let (State f1) = mv
(v1, st2) = f1 st1
(State f2) = (f v1 >>= g)
in f2 st2)
```

Now expand out the remaining `>>=`

application, renaming the bound variables to
names which haven't been used yet:

```
State (\st1 ->
let (State f1) = mv
(v1, st2) = f1 st1
(State f2) = (State (\st3 ->
let (State f3) = f v1
(v2, st4) = f3 st3
(State f4) = g v2
in f4 st4))
in f2 st2)
```

Remove the `State`

wrappers from `(State f2)`

and `(State (\st3 -> ...))`

(they
aren't needed):

```
State (\st1 ->
let (State f1) = mv
(v1, st2) = f1 st1
f2 = \st3 ->
let (State f3) = f v1
(v2, st4) = f3 st3
(State f4) = g v2
in f4 st4
in f2 st2)
```

Apply the function `f2`

to `st2`

, getting rid of the `f2`

binding in the process
(since it isn't needed anywhere else):

```
State (\st1 ->
let (State f1) = mv
(v1, st2) = f1 st1
in (\st3 ->
let (State f3) = f v1
(v2, st4) = f3 st3
(State f4) = g v2
in f4 st4) st2)
```

Simplify:

```
State (\st1 ->
let (State f1) = mv
(v1, st2) = f1 st1
in
let (State f3) = f v1
(v2, st4) = f3 st2
(State f4) = g v2
in f4 st4
```

Combine the two `let`

expressions into one:

```
State (\st1 ->
let (State f1) = mv
(v1, st2) = f1 st1
(State f3) = f v1
(v2, st4) = f3 st2
(State f4) = g v2
in f4 st4
```

Renaming some bound variables, we get:

```
State (\st1 ->
let (State f1) = mv
(v1, st2) = f1 st1
(State f2) = f v1
(v2, st3) = f2 st2
(State f3) = g v2
in f3 st3
```

This is the same as the final expansion of the left-hand side, so we're done (Q.E.D.). Whew!

What we've shown in this section is that the state monads we derived previously are in fact monads, and therefore, monadic functions in the state monad will compose properly.

## The complete `Monad`

instance definition for state monads

To recap, the complete (and verified!) instance of `Monad`

for state monads is:

```
instance Monad (State s) where
return x = State (\st -> (x, st))
mv >>= g = State (\st ->
let (State ff) = mv
(y, st') = ff st
(State gg) = g y
in gg st')
```

The `>>`

operator and the `fail`

function for state monads are just the default
versions, so this is the full definition.

## Next time

That's plenty for one article.

In the next
installment, we'll work through a complete example of a simple computation
that uses state monads. Along the way, we'll discover the handy
`MonadState`

type class, which will make working with state monads a
lot more pleasant.

mvanierRe: Excellent Series on Monads.