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 xs 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 called alpha-renaming in 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.