## Functors and monads

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 andEffect = 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)) })

## Monads

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 becauselift (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

to their input types. This specifies`Lift<>`

`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 getm (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 becauselift (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 getm (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 becauselift (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 getm (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 becauselift (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]]

`m()`

to all of these, we get the associativity and unit laws. For associativity we getm (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 functionsf = (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).

leave a comment