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 upf
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 upf
with the identity function on strings:lift (f) = (f, id)
- Composition
LetEnv
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
isid<Env>
, the “trivial side-effect”.Then
Lift<>
adjoins an extra side-effect to any type:Lift<A> = Pair<A, Effect>
The function
lift()
pairs upf
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 typeA
to a list ofA
‘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 theUnit
type, with a single value, and there’s also theEmpty
type, with no values (it’s “uninhabited”). The only function of typeX -> Empty
is the identity functionid<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 intoEmpty
“: letF = Empty
andT = F -> F
. ThenT -> F = F
(sinceT -> F
is uninhabited) andT
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 onEnv
: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 functionse()
andm()
. The first is applyinglift()
to them. When we applylift
tom()
, 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()
ande()
is to apply
to their input types. This specifiesLift<>
A
asPair<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 functionse()
andm()
. The first is applyinglift()
to them. When we apply lift tom()
, 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()
ande()
is to applyLift<>
to their input types. This specifiesA
asPair<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 functionse()
andm()
. The first is applyinglift()
to them. When we apply lift tom()
, 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()
ande()
is to applyLift<>
to their input types. This specifiesA
asPair<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 functionse()
andm()
. The first is applyinglift()
to them. When we apply lift tom()
, 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()
ande()
is to applyLift<>
to their input types. This specifiesA
asList<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 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 functionsr, 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 withe
—or in the language of Haskell, wereturn
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
andg
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