# reperiendi

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]```

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).`

## The first 220 milliseconds of an https connection

Posted in Uncategorized by Mike Stay on 2009 June 12

## My talk at Perimeter Institute

Posted in Category theory, General physics, Math, Quantum by Mike Stay on 2009 June 11

I spent last week at the Perimeter Institute, a Canadian institute founded by Mike Lazaridis (CEO of RIM, maker of the BlackBerry) that sponsors research in cosmology, particle physics, quantum foundations, quantum gravity, quantum information theory, and superstring theory. The conference, Categories, Quanta, Concepts, was organized by Bob Coecke and Andreas Döring. There were lots of great talks, all of which can be found online, and lots of good discussion and presentations, which unfortunately can’t. (But see Jeff Morton’s comments.) My talk was on the Rosetta Stone paper I co-authored with Dr. Baez.