Kleisli Tools

← → November 23, 2016

Welcome back! Thanks for not having torn your eyes out with disgust at how egregiously difficult it was to use our Kleisli category for State s in the last chapter. Our plan for this chapter, as promised, is to derive some useful lemma machines to allow us to work with Kleisli categories more easily.

Lambda Abstraction

The first tool we’ll need isn’t particularly tied to Kleisli categories, but it’s what you might call a “quality of life” improvement, in that it will allow us to write symbolic computations a little more tersely. This tool comes directly from the realization that although we have been saying that our machines are just values, they’re obviously different somehow. We can see this in the sense that our symbolic computations require a “special” syntax to make machines. Let’s take a closer look.

In order to evaluate, for example, our machine map : Kliesli m => (a -> b) -> m a -> m b, we need a function of type a -> b to give it as an input. Evaluating it might look something like this:

addTwo : Nat -> Nat
addTwo n = n + 2

> map addTwo (Just 8) = Just 10

This works well enough, but it’s rather annoying that we need to make a new machine definition every time we want to use a higher-order function (such as map). Especially if this machine is nothing but a lemma and won’t be useful anywhere else, it’d be nice if we could somehow define our function where we want to use it, rather than somewhere above or below.

With this in mind, our first tool will be a means of describing simple machines locally at the place they’re needed. As an example of this, will can rewrite our above example with our new tool:

> map (λn. n + 2) (Just 8) = Just 10

Much simpler! What a welcome change that is. We call this λn. n + 2 a lambda abstraction, a lambda expression, or if you’re a fan of brevity, it’s also known as just a lambda.

There are a few rules around the syntax of lambda abstractions. The lambda symbol λ introduces a new lambda expression, which takes inputs separated by spaces until the next .. Each of these inputs is bound in the lambda machine, and refers to a new binding that didn’t exist before. That means if there is already a binding called x when we create our lambda λx. x, the x inside of the lambda refers to the input bound by the lambda, not to the one that existed beforehand. That being said, a lambda can refer to any bindings that existed already so long as they don’t share a name.

Such a property (stealing the name of binding if it conflicts) is known as lexical scoping of bindings. Our entire system of symbolic computations is lexically scoped, and so lambdas share the same rules as the rest of the language. Parsimony!

The other syntactic rule of lambdas is that their function definition extends as far as it can. This means that

map λn. n + 2 (Just 8)

is not equivalent to the one given earlier. This represents attempting to pass a single machine defined as λn. n + 2 (Just 8) as the first input to map, which doesn’t make any sense, and obviously isn’t what we meant. In order to delimit the contents of a lambda, we must enclose it in parentheses.

This rule of “extending as far as you can” has the interesting property that it allows us to write lambdas inside of lambdas:

λx. λy. x + y

is a lambda which binds x, and then outputs a lambda which binds y and then outputs x + y. You’ll recall that all of our machines are curried like this, so there’s nothing new here, but it’s nice to know that the same rules apply. This will come in handy in a second.

Before we move on, we should note that lambdas, just like regular machines, may take multiple inputs:

λx y z. x + y + z

and this behaves exactly as you’d expect it to – taking three inputs, x, y, and z, and then adding them together.

Kleisli Bind

The next tool we’ll formalize is actually one we’ve already seen. Recall our definition of hold from the previous chapter:

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)

This bind thing seems rather odd – it doesn’t appear to have anything to do with State or even with the computation behind hold. All we need it for is as an “adapter” to allow us to start our Kliesli composition. By that we mean that if we have a function of type a -> m b, and we have an m a, how can we apply our function to the m a? bind is the solution to this problem.

We have a quick lemma to look at before getting around to bind, however:

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

always is one of those “adapter” higher-order machines. always takes two inputs, and regardless of what the second one is, it returns the first input. This means if we fill in the first input but leave the second empty, we get a machine that “always” spits out the first input we put in, no matter what this machine is called with. That means we can use it to transform our m a into a y -> m a, allowing us to begin Kleisli composing things together.

With always under our belt, we’re ready to look at bind proper.

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

We can use always ma to get a function of type y -> m a (here a is no longer a type variable – it’s fixed to be the same a as was in our ma : m a. y, however is still polymorphic). With this function, we can composeK it with f : a -> m b, the result of which is y -> m b for some polymorphic y. Because y is polymorphic, it can be anything, so we fill it with a Unit, and out pops a value of type m b.

bind can be thought of like this: it allows us to supply a value existing in a context, to a computation which itself runs in a context. It’s analogous to “running a pure computation with a pure input”, except now we’re running Kleisli compositions with Kleisli inputs.

As it happens, bind plays a very important role in the Kleisli tool ecosystem. In fact, it’s so important that we will come up with a symbolic name for it (in the same way that we had special symbols for our core gates back when we were doing machine diagrams). The symbol we use is »=, but is still pronounced “bind”. Because of this symbol, the two following expressions are equivalent:

> bind ma f

and

> ma »= f

Hold, Revisited

Recall, our original definition for hold. It’s still just as ugly as it ever was:

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)

however, armed with our new tools, we can write hold in this much prettier form:

hold : Bool -> State Bool Bool
hold val =     get
        »= λs. set (or val s)
        »= λ_. get

Regardless of your political, racial, historical, or desktop background, you must admit that this is much nicer to deal with and to reason about. When presented in this format, it’s pretty clear that there are some series of steps happening to compute the result. First, we get the current state, and bind it to s. We then set the state to or val s, and then output the new state.

Because of our rules about the extent of lambda abstracts, after s is bound on the second line, it would be available anywhere after that, should it be necessary. We ignore the output coming out of set (λ_.) because if you remember, set always returns Unit, which is uninformative for us to bind.

As a matter of fact, we’ll see that we usually don’t care about the output of a particular Kleisli computation – often we’re just composing them in order to run their “side effects” on the context/environment. This use case is so common that we present one last lemma: ignoring.

ignoring : Kleisli m
        => m a
        -> m b
        -> m b
ignoring ma mb =     ma
              »= λ_. mb

which goes by the special symbol ». Ignoring performs the “side effects” of its first input, but actually returns just its second input. You can keep bind (»=) separate from ignoring (») in your mind by remembering that bind allows you to “equate” a binding, so it’s the one that has the equals sign.

With ignoring, we can write hold again:

hold : Bool -> State Bool Bool
hold val =     get
        »= λs. set (or val s)
        »      get

This is pretty good, all things considered. We have one final complaint, however. The binding s gets it value from the first get, but the first sighting of s is on the next line! That’s bad for those of us with slight obsessive compulsions, and so we’ll introduce one final syntactic piece of “sugar” to help us along. It’s called do-notation, and we can use it to rewrite hold one last time:

hold : Bool -> State Bool Bool
hold val = do
    s ← get
    set (or val s)
    get

In do-notation, we introduce a new “block” in which Kleisli values are written one-a-line. If the result of any particular Kleisli value is interesting to us, we can bind it via the ← symbol. This new binding is available to us for all Kleisli values below the current line, because behind the scenes, all do-notation is doing for us is giving us a less-boilerplate way of writing nested lambdas and binds.

Whenever a binding is required, say s ← get, do-notation “de-sugars” down to get »= λs. and the computation carries on its merry way. If a binding isn’t required, do uses ignoring (») to discard that particular value.

It’s finally time to rejoice. With do-notation, our deep dive into Kleisli categories is complete, and we find ourselves with all the tools necessary to continue doing work on the computer we’ve been wanting to build for this entire time. We’ll really and truly get back to that in the next chapter, an with our new tools, the remainder of our project will be surprisingly easy.

Exercises

Rewrite map : Kleisli m => (a -> b) -> m a -> m b from the last chapter in terms of do-notation.
Manually desugar the following do-notation to make sure you’ve got the hang of it:

modifyAndAdd : (Nat -> Nat) -> State Nat Nat
modifyAndAdd f = do
    oldState ← get
    set (f oldState)
    newState ← get
    inject (oldState + newState)

← →