# reperiendi

## Functors and monads

Posted in Category theory, Math, Programming by Mike Stay on 2009 June 23

In many languages you have type constructors; given a type `A` and a type constructor `Lift`, you get a new type` Lift<A>`. A functor is a type constructor together with a function

`   lift: (A -> B) -> (Lift<A> -> Lift<B>)`

that preserves composition and identities. If `h` is the composition of two other functions `g` and `f`

`   h (a) = g (f (a)),`

then `lift (h)` is the composition of `lift (g)` and `lift (f)`

`   lift (h) (la) = lift (g) (lift (f) (la)),`

where the variable `la` has the type `Lift<A>`. Similarly, if h is the identity function on variables of type `A`

`   h (a: A) = a,`

then `lift (h)` will be the identity on variables of type `Lift<A>`

`   lift (h) (la) = la.`

### Examples:

• Multiplication
`Lift<>` adjoins an extra integer to any type:

`   Lift<A> = Pair<A, int>`

The function `lift()` pairs up `f` with the identity function on integers:

`   lift (f) = (f, id)`
• Concatenation
`Lift<>` adjoins an extra string to any type:

`   Lift<A> = Pair<A, string>`

The function `lift()` pairs up `f` with the identity function on strings:

`   lift (f) = (f, id)`
• Composition
Let `Env` be a type representing the possible states of the environment and

`   Effect = Env -> Env`

Also, we’ll be explicit in the type of the identity function

```   id<A>: A -> A
id<A> (a) = a,```

so one possible `Effect` is `id<Env>`, the “trivial side-effect”.

Then `Lift<>` adjoins an extra side-effect to any type:

`   Lift<A> = Pair<A, Effect>`

The function `lift()` pairs up `f` with the identity on side-effects:

`   lift (f) = (f, id<Effect>)`
• Lists
The previous three examples used the Pair type constructor to adjoin an extra value. This functor is slightly different. Here, `Lift<>` takes any type `A` to a list of `A`‘s:

`   Lift<A> = List<A>`

The function `lift()` is the function map():

`   lift = map`
• Double negation, or the continuation passing transform
In a nice type system, there’s the `Unit` type, with a single value, and there’s also the `Empty` type, with no values (it’s “uninhabited”). The only function of type `X -> Empty` is the identity function `id<Empty>`. This means that we can think of types as propositions, where a proposition is true if it’s possible to construct a value of that type. We interpret the arrow as implication, and negation can be defined as “arrowing into `Empty`“: let `F = Empty` and `T = F -> F`. Then `T -> F = F` (since `T -> F` is uninhabited) and `T` is inhabited since we can construct the identity function of type F -> F. Functions correspond to constructive proofs. “Negation” of a proof is changing it into its contrapositive form:

`  If A then B => If NOT B then NOT A.`

Double negation is doing the contrapositive twice:

`  IF A then B => If NOT NOT A then NOT NOT B.`

Here, `Lift<>` is double negation:

`   Lift<A> = (A -> F) -> F.`

The function lift takes a proof to its double contrapositive:

```   lift: (A -> B)   ->   ((A -> F) -> F) -> ((B -> F) -> F)
lift  (f) (k1) (k2) = k1 (lambda (a) { k2 (f (a)) })```

A monad is a functor together with two functions

```   m: Lift<Lift<A>> -> Lift<A>
e: A -> Lift<A>```

satisfying some conditions I’ll get to in a minute.

### Examples:

• Multiplication
If you adjoin two integers, `m()` multiplies them to get a single integer:

```   m: Pair<Pair<A, int>, int> -> Pair<A, int>
m  (a, i, j)               =  (a, i * j).```

The function `e()` adjoins the multiplicative identity, or “unit”:

```   e: A   -> Pair<A, int>
e  (a) = (a, 1)```
• Concatenation
If you adjoin two strings, `m()` concatenates them to get a single string:

```   m: Pair<Pair<A, string>, string> -> Pair<A, string>
m  (a, s, t)                     =  (a, s + t).```

The function `e()` adjoins the identity for concatenation, the empty string:

```   e: A   -> Pair<A, string>
e  (a) = (a, "")```
• Composition
If you adjoin two side-effects, `m()` composes them to get a single effect:

```   m: Pair<Pair<A, Effect>, Effect> -> Pair<A, Effect>
m  (a, s, t)                     =  (a, t o s),```

where

`   (t o s) (x) = t (s (x)).`

The function `e()` adjoins the identity for composition, the identity function on `Env`:

```   e: A   -> Pair<A, Effect>
e  (a) = (a, id<Env>)```
• Lists
If you have two layers of lists, `m()` flattens them to get a single layer:

```   m: List<List<A>> -> List<A>
m = flatten```

The function `e()` makes any element of A into a singleton list:

```   e: A -> List<A>
e (a) = [a]```
• Double negation, or the continuation passing transform
If you have a quadruple negation, `m()` reduces it to a double negation:

```   m: ((((A -> F) -> F) -> F) -> F)   ->  ((A -> F) -> F)
m (k1) (k2) = k1 (lambda (k3) { k3 (k2) })```

The function `e()` is just reverse application:

```   e: A -> (A -> F) -> F
e (a) (k) = k (a)```

The conditions that `e` and `m` have to satisfy are that `m` is associative and `e` is a left and right unit for `m`. In other words, assume we have

```   llla: Lift<Lift<Lift<A>>>
la: Lift<A>```

Then

`   m (lift (m) (llla))  =  m (m (llla))`

and

`   m (e (la))  =  m (lift (e) (la))  =  la`

### Examples:

• Multiplication:
There are two different ways we can use lifting with these two extra functions `e()` and `m()`. The first is applying `lift()` to them. When we apply `lift` to `m()`, it acts on three integers instead of two; but because

`   lift (m) = (m, id),`

it ignores the third integer:

`   lift (m) (a, i, j, k) = (a, i * j, k).`

Similarly, lifting `e()` will adjoin the multiplicative unit, but will leave the last integer alone:

```   lift (e) = (e, id)
lift (e) (a, i) = (a, 1, i)```

The other way to use lifting with `m()` and `e()` is to apply `Lift<>` to their input types. This specifies `A` as `Pair<A', int>`, so the first integer gets ignored:

```   m (a, i, j, k) = (a, i, j * k)
e (a, i) = (a, i, 1)```

Now when we apply `m()` to all of these, we get the associativity and unit laws. For associativity we get

```   m (lift (m) (a, i, j, k)) = m(a, i * j, k) = (a, i * j * k)
m (m (a, i, j, k)) = m(a, i, j * k) = (a, i * j * k)```

and for unit, we get

```   m (lift (e) (a, i)) = m (a, 1, i) = (a, 1 * i) = (a, i)
m (e (a, i)) = m (a, i, 1) = (a, i * 1) = (a, i)```
• Concatenation
There are two different ways we can use lifting with these two extra functions `e()` and `m()`. The first is applying `lift()` to them. When we apply lift to `m()`, it acts on three strings instead of two; but because

`   lift (m) = (m, id),`

it ignores the third string:

`   lift (m) (a, s, t, u) = (a, s + t, u).`

Similarly, lifting `e()` will adjoin the empty string, but will leave the last string alone:

```   lift (e) = (e, id)
lift (e) (a, s) = (a, "", s)```

The other way to use lifting with `m()` and `e()` is to apply `Lift<>` to their input types. This specifies `A` as `Pair<A', string>`, so the first string gets ignored:

```   m (a, s, t, u) = (a, s, t + u)
e (a, s) = (a, s, 1)```

Now when we apply `m()` to all of these, we get the associativity and unit laws. For associativity we get

```   m (lift (m) (a, s, t, u)) = m(a, s + t, u) = (a, s + t + u)
m (m (a, s, t, u)) = m(a, s, t + u) = (a, s + t + u)```

and for unit, you get

```   m (lift (e) (a, s)) = m (a, "", s) = (a, "" + s) = (a, s)
m (e (a, s)) = m (a, s, "") = (a, s + "") = (a, s)```
• Composition
There are two different ways we can use lifting with these two extra functions `e()` and `m()`. The first is applying `lift()` to them. When we apply lift to `m()`, it acts on three effects instead of two; but because

`   lift (m) = (m, id<Effect>),`

it ignores the third effect:

`   lift (m) (a, s, t, u) = (a, t o s, u).`

Similarly, lifting `e()` will adjoin the identity function, but will leave the last string alone:

```   lift (e) = (e, id<Effect>)
lift (e) (a, s) = (a, id<Env>, s)```

The other way to use lifting with `m()` and `e()` is to apply `Lift<>` to their input types. This specifies `A` as `Pair<A', Effect>`, so the first effect gets ignored:

```   m (a, s, t, u) = (a, s, u o t)
e (a, s) = (a, s, id<Env>)```

Now when we apply `m()` to all of these, we get the associativity and unit laws. For associativity we get

```   m (lift (m) (a, s, t, u)) = m(a, t o s, u) = (a, u o t o s)
m (m (a, s, t, u)) = m(a, s, u o t) = (a, u o t o s)```

and for unit, you get

```   m (lift (e) (a, s)) = m (a, id<Env>, s) = (a, s o id<Env>) = (a, s)
m (e (a, s)) = m (a, s, id<Env>) = (a, id<Env> o s) = (a, s)```
• Lists
There are two different ways we can use lifting with these two extra functions `e()` and `m()`. The first is applying `lift()` to them. When we apply lift to `m()`, it acts on three layers instead of two; but because

`   lift (m) = map (m),`

it ignores the third (outermost) layer:

```     lift (m) ([[[a, b, c], [], [d, e]], [[]], [[x], [y, z]]])
= [[a, b, c, d, e], [], [x, y, z]]```

Similarly, lifting `e()` will make singletons, but will leave the outermost layer alone:

`   lift (e) ([a, b, c]) = [[a], [b], [c]]`

The other way to use lifting with `m()` and `e()` is to apply `Lift<>` to their input types. This specifies `A` as `List<A'>`, so the *innermost* layer gets ignored:

```     m ([[[a, b, c], [], [d, e]], [[]], [[x], [y, z]]])
= [[a, b, c], [], [d, e], [], [x], [y, z]]

e ([a, b, c]) = [[a, b, c]]```

Now when we apply `m()` to all of these, we get the associativity and unit laws. For associativity we get

```     m (lift (m) ([[[a, b, c], [], [d, e]], [[]], [[x], [y, z]]]))
= m([[a, b, c, d, e], [], [x, y, z]])
= [a, b, c, d, e, x, y, z]

m (m ([[[a, b, c], [], [d, e]], [[]], [[x], [y, z]]]))
= m([[a, b, c], [], [d, e], [], [x], [y, z]])
= [a, b, c, d, e, x, y, z]```

and for unit, we get

```   m (lift (e) ([a, b, c])) = m ([[a], [b], [c]]) = [a, b, c]
m (e ([a, b, c])) = m ([[a], [b], [c]]) = [a, b, c]```

## Monads in Haskell style, or “Kleisli arrows”

Given a monad `(Lift, lift, m, e)`, a Kleisli arrow is a function

`   f: A -> Lift<B>,`

so the `e()` function in a monad is already a Kleisli arrow. Given

`   g: B -> Lift<C>`

we can form a new Kleisli arrow

```   (g >>= f): A -> Lift<C>
(g >>= f) (a) = m (lift (g) (f (a))).```

The operation >>= is called “bind” by the Haskell crowd. You can think of it as composition for Kleisli arrows; it’s associative, and `e()` is the identity for bind. `e()` is called “return” in that context. Sometimes code is less complicated with bind and return instead of `m` and `e`.

If we have a function `f: A -> B`, we can turn it into a Kleisli arrow by precomposing with `e()`:

```   (e o f): A -> Lift<B>
(e o f) (a) = e (f (a)) = return (f (a)).```

### Example:

• Double negation, or the continuation passing style transform
We’re going to (1) show that the CPS transform of a function takes a continuation and applies that to the result of the function.  We’ll also (2) show that for two functions `r, s`,

`     CPS (s o r)    =    CPS (s) >>= CPS (r),`

(1) To change a function `f: A -> B` into a Kleisli arrow (i.e. continuized function)` CPS (f): A -> (B -> X) -> X`, we just compose with `e`—or in the language of Haskell, we `return` the result:

```     CPS (f) (a) (k)
= return (f (a)) (k)
= (e o f) (a) (k)
= e (f (a)) (k)
= k (f (a))```

(2) Given two Kleisli arrows

`   f: A -> (B -> F) -> F`

and

`   g: B -> (C -> F) -> F,`

we can bind them:

```     (g >>= f) (a) (k)
= m (lift (g) (f (a))) (k)                                // defn of bind
= lift (g) (f (a)) (lambda (k3) { k3 (k) })               // defn of m
= f (a) (lambda (b) { (lambda (k3) { k3 (k) }) (g (b)) }) // defn of lift
= f (a) (lambda (b) { g (b) (k) }),                       // application```

which is just what we wanted.

In particular, if `f` and `g` are really just continuized functions

```   f = (e o r)
g = (e o s)```

then

```     (g >>= f) (a) (k)
= f (a) (lambda (b) { g (b) (k) })             // by above
= (e o r) (a) (lambda (b) { (e o s) (b) (k) }) // defn of f and g
= (e o r) (a) (lambda (b) { k (s (b)) })       // defn of e
= (e o r) (a) (k o s)                          // defn of composition
= (k o s) (r (a))                              // defn of e
= k (s (r (a)))                                // defn of composition
= (e o (s o r)) (a) (k)                        // defn of e
= CPS (s o r) (a) (k)                          // defn of CPS```

so

`   CPS (s) >>= CPS (r)    =    CPS (s o r).`