Revisiting State

← → November 22, 2016

We ended last chapter by looking at what does it mean for something to be a Kleisli category, and found ourselves on a cliffhanger regarding the Kleisli nature of reality itself. We showed how choosing some type constructor m, and a pair of functions inject : a -> m a and composeK : (a -> m b) -> (b -> m c) -> (a -> m c) resulted in us saying that m was Kleisli.

This notion can be formalized into the following claim in symbolic computation:

class Klesili m where
  inject   : a -> m a
  composeK : (a -> m b) -> (b -> m c) -> (a -> m c)

which tells us exactly what we said above. It should be read as

There is a class of patterns, called Kleisli, which binds a type constructor variable m. In order for this to be a pattern, the type constructor m must support two functions: inject and composeK.

We can now “prove” to the symbolic computation that Maybe and Identity are Kleisli by making claims of the form:

instance Kleisli Maybe where
  inject a      = injectMaybe a
  composeK m1 m2 = composeMaybe m1 m2

instance Kleisli Identity where
  inject a       = injectIdentity a
  composeK m1 m2 = composeIdentity m1 m2

The word instance is short for “is an instance of the pattern”. We say that, for example, this instance Kleisli Maybe statement is witness to the fact that Maybe is Kleisli – meaning, that instance Kleisli Maybe is a proof that Maybe is Kleisli. It’s a proof because it lists all of the necessary functions in one place.

Before we get started in earnest, it’s helpful to see how being an instance of the Kleisli pattern can be useful. If we stick to our original intuition behind type constructors being “containers”. we can use a Kleisli proof to “change the thing inside a container”:

map : Kleisli m => (a -> b) -> m a -> m b
map f ma = bind ma m1
  where
    m1 : a -> m b
    m1 = compose f inject

    bind : m a -> (a -> m b) -> m b
    bind ma f = (composeK (always ma) f) Unit

    always : x -> (y -> x)
    always x _ = x

As an example, we can evaluate:

map succ (Just 5) = Just 6

but

map succ Nothing = Nothing

The exact construction of map here isn’t necessarily the point, but it shows off some interesting things. The first of which is our new syntax: map : Kleisli m => (a -> b) -> m a -> m b which means “the map function exists as (a -> b) -> m a -> m b whenever m is Kleisli.” The reason this is can be so is that we defined map only using lemmas we could derive with inject and composeK, which we know only exist if m is Kleisli (because their existence is what makes something Klesili).

This fat arrow => should be read as “implies that we have”, and should be taken to be a delimiter between constraints necessary for the function to exist, and the actual types in the signature.

What you should takeaway from the map example is that we can use classes of patterns to describe machinery which is polymorphic, but need not exist for all types. We do this by defining our polymorphic thing in terms of features that are provided to us by having a witness that our type is an instance of a particular pattern.

Another way of saying that is if we can define something in terms of nothing but the Klesili functions, then it must exist for anything which is Kleisli. Makes sense, really. map is one such definition.

Revisiting State

Seemingly many moons ago we discovered that the formulation behind our stateful machine latches wasn’t “pure”, and thus couldn’t ever be evaluated as a symbolic computation. This was particularly upsetting, because we were capable of doing it with machine diagrams (even if we were technically cheating), but our system that was supposed to be the latest and greatest new hotness wasn’t capable of doing it.

That changes now. We had to jump several hoops in order to have all of the necessary conceptual tools in order, but we’re now ready to tackle stateful computations.

The question becomes “how can we model state?”, and it’s not a particularly hard thing to answer. A computation that runs in a stateful context must do two things: it must be dependent on some state, and it produces some output which can change depending on that state. In the process, this computation can even change that state.

Recall our Hold example. Here, our state is the second input to the or gate – the resulting computation depends on it. In this case, the state is always updated to be the same as the resulting computation. Really, as far as the interface to this function is concerned, the stateful wire is an “implementation detail”, in the sense that it isn’t part of either the input nor the output of the computation.

However, it can affect the computation, and this is what made our function impure, and thus gave us so much grief. But when phrased this way, it becomes a little clearer that indeed this Hold machine is a computation with some sort of context – the context of course being “the current state of that input wire”.

Modeling state is thus a transformation from some “old” state, to a computation and a “new” state. The word “transformation” in there should tip us off to a function type, and the word “and” points us towards a product type. Indeed:

type State s a = s -> (a, s)

We can interpret this as “State s a is the type of a computation which produces an a, using (and potentially updating) some state s in the process.”

This State s a type is messy, and if we had to sling this state around every time we wanted to work with it, we’d start hating our lives and probably take up a new hobby instead. But we have a trick up our sleeves. If we can prove that State s is Klesili, then we can use Kleisli composition to rig up all the correct handling of our state for us and spare us the gritty details.

The Kleisli Category of State

Before we can even begin to think of using Kleisli composition to solve any problems for us, we must first prove that we have an instance of the Kleisli pattern around.

The easiest step is usually to write inject : a -> State s a, so we’ll start there. Technically there are a few laws that any instance Kleisli must follow, but for the most part they boil down to “don’t do anything arbitrarily stupid”. We’ll look into them later when we look at the more general notion of categories. For the time being, we’ll just write the “obvious” inject, and that will turn out to be what we want.

How do we write inject? Well, what do we have, and what do we want? We have an a, and we want a s -> (a, s). Expanding this out, the type of inject is a -> s -> (a, s), which is “given an a and an s, give back a pair of an a and an s”.

Seems easy enough.

injectState : a -> State s a
injectState a s = (a, s)

Point of order: Even though we’re writing State s a in the type signature here for injectState, it really is just a s -> (a, s), which is why our implementation of injectState takes two inputs, rather than just one.

Great! So we have inject. All that’s left now is composeK. Let’s expand out its type as well to see if anything interesting comes out of it:

composeState : (a -> s -> (b, s))
            -> (b -> s -> (c, s))
            -> (a -> s -> (c, s))

At a first glance, it seems like we should be able to use the same trick of pulling the s out of the State s definition, but this function signature is misleading. The first two inputs we’re given into composeState are functions which require ss, they don’t give us anything we can use. Instead, it’s informative to drop the parentheses around the output, which if you recall, is completely legal and fair game:

composeState : (a -> s -> (b, s))
            -> (b -> s -> (c, s))
            -> a
            -> s
            -> (c, s)

Without the parentheses, it’s clear that we do in fact have an s to play with – it was just hiding in our output. This sounds crazy, until you recall that this is sort of exactly why we wanted to track state in the first place – so that our machines could depend somehow on their output. Kleisli machinery gives us a way of doing this, by hiding details inside of the machine’s output. It’s wild, but it actually works, so it’s hard to argue with.

And so we’re ready to write a definition of composeState. We’ll take the a and the s we’re given, pass them into our m1 : a -> s -> (b, s), where the output of m1 is a b and a new state s, which we can then pass into m2.

composeState : (a -> s -> (b, s))
            -> (b -> s -> (c, s))
            -> a
            -> s
            -> (c, s)
composeState m1 m2 a state = (c, finalState)
  where
    (b, newState)   = m1 a state
    (c, finalState) = m2 b newState

With that, we can now prove that State s is Kleisli:

instance Kleisli (State s) where
  inject   = injectState
  composeK = composeState

Finally we’re done! Well, sort of. The attentive reader will notice that we have provided no means for machines to actually get the value of the state context they’re running in. Having a state isn’t very useful if you’re unable to actually use it.

We therefore provide two additional functions to the Kleisli category of State s. The first is get : State s s:

get : State s s
get state = (state, state)

get provides access to the state. Notice its strange type: get : State s s. It has no inputs, and so we can consider get to be a constant “value” of type State s s, in the same way that 41 : Nat. Recall that State s a = s -> (a, s), and so get is really giving us back the internal state in the place of “a”, which we can then use Kleisli composition to do interesting things with.

Similarly, getting the current state isn’t very helpful if you’re unable to change it. Behold set:

set : s -> State s Unit
set newState _ = (Unit, newState)

We output a value of Unit to indicate that we didn’t have anything better to output. Outputting a Unit is the least interesting thing we can possibly do – recall that Unit tells us literally nothing, because we always can pull one up from nothingness. A machine which outputs Unit is thus somewhat interesting. It’s not outputting Unit because that’s a useful thing to tell us, so that means that any machine which outputs Unit in a Kleisli context must have actually done something. It must have somehow modified the context, because that’s the only other thing that Kleisli machines can do (other than return values). It’s a neat convention, and something to keep your eyes peeled for.

Finally, armed with all of these things, we’re ready to write Hold from above:

hold : Bool -> State Bool Bool
hold val = bind get withState
  where
    bind : State Bool a -> (a -> State Bool b) -> State Bool b
    bind ma f = (composeK (always m) f) Unit

    always : x -> (y -> x)
    always x _ = x

    withState : Bool -> State Bool Bool
    withState s = bind (set (or val s)) (always get)

Egads. What a terrible eyesore. It’s gruesome, but it turns out to actually work, and that’s the important part. Bet it makes you want to start finding a new hobby though, am I right? Don’t worry, in the next chapter, we’ll expand the syntax of our symbolic computations to something Kleisli-aware – which is to say “doesn’t make you want to rip your own eyes out with a rusty spoon when doing these kinds of things.” Hold onto your eyes until the next chapter, and we’ll make everything better.

Exercises

Work through the definition of map : Kleisli m => (a -> b) -> m a -> m b above. If you think of always : x -> (y -> x) as a function which always just ignores its second input and returns its first, it kind of looks like the right adapter we need in order to start working with composeK.
Work through the definition of hold : Bool -> State Bool Bool above. Notice how it uses the same bind lemma that map did.
Define a function modify : (s -> s) -> State s Unit which takes a machine that describes how to modify the internal state.

← →