Typed Lambda Calculus For Me (And Maybe You)

I'm reading chapter 10 of Lambda-Calculus and Combinators by J. Roger Hindley and Jonathan P. Seldin, and I wanted to put down some notes. These notes are mostly for myself, much in the spirit of why I started this blog - to measure my own progress. However, since I know I have readers I'll write it in a way that people learn something. If people are interested in this though, since I'm already investing time in it, I'd be happy to do into more detail on the beginners stuff and/or some of the history behind this (I might just do it anyway). Also if anyone smarter than me finds any errors here, or has tips to explain it better, please do. Okay Go.

In the book there is this nugget:

(λx:p->ø->t.
 (λy:p->ø.
   (λz:p.((x:p->ø->t z:p):ø->t (y:p->ø z:p):ø):t):p->t
 ):A
):B

You (the reader) are supposed to solve this for A and B.

For those of you unfamiliar with lambda calculus, and/or typed lambda calculus, this is a lot easier than it looks. What I'll do here is try to explain the steps nice and slow, and then at the bottom maybe try to write this in Scala to demonstrate.

Explicit Type Information

Ok, the important thing here is that we are given a lot of information. Here's a list of the things we definitely know about the types in the statement above:

1. x:p->ø->t


2. y:p->ø


3. z:p

In more detail:

1. x is a function that takes a p and returns a function that takes an ø and returns a t.


2. y is a function that takes a p and returns an ø


3. z is simply a p

Or in Scala:

1. val x:p=>ø=>t


2. val y:p=>ø


3. val z:p

How do we know this? Well, that's basic typed lambda calculus. Here are a couple of very basic notes:

1. The statement (λx:p->ø->t.M) is a function that takes an argument, x, which is of type p->ø->t. Arrows imply function types and hence x is a function that takes a p and returns a function that takes an ø and returns a t.


2. The return value of the function in this tiny example is M (above is much more complicated, but that's what were getting to).

Function Application

Now, using what we know about the types, and the rest of the statement, what else can we figure out? Hmm, I guess we should talk about function application, by looking at the innermost bit of the statement above.

We see this: (x:p->ø->t z:p):ø->t, and this means we are calling the function x with the argument z. Remember that everything after the colons are simply types. Ignoring the types, we could just write (x z) which is basic function application in lambda calulus. In Scala this would be simply x(z). And what type does calling x yield? Not to beat it into your brain, but remember that x is a function that takes a p and returns a function that takes an ø and returns a t. Calling it with a p will yield a function that takes an ø and returns a t, or more simply ø->t.

In the original statement, we had (x:p->ø->t z:p):ø->t, and this is correct, as I just explained.

That isn't the only function application in the statement either. Right next to it we see (y:p->ø z:p):ø. Does this check out? Remember that y is a function that takes a p and returns an ø, and z is a p. Perfect. Applying y with argument x yields a ø.

Now, that fact that I said "right next to it" is meaningful. Now that we've resolved the first two applications, we end up with another application! The result of the first application ((x:p->ø->t z:p):ø->t) was ø->t, and the result of the second was a ø, and these also match. Applying ø->t to an ø results in a t. And now we've finished this big inner statement: ((x:p->ø->t z:p):ø->t (y:p->ø z:p):ø):t.

Building Functions

Now that we've looked at the internal parts of the statement boiling it all down to a t, we can start to work our way outwords. Recall that λ is used to denote a function. λx:Int."hey" is a function that takes an Int (named x) and returns a String, "hey". Fully typed this would be (λx:Int."hey"):String

Working our way one step outwards from our function applications, we have (λz:p.((x:p->ø->t z:p):ø->t (y:p->ø z:p):ø):t):p->t. Recall that we already determined the inner part to be a t. We can now thing of this as (λz:p.(some arbitrary t)):p->t. And that's correct. This is a function that takes a argument z of type p, and returns a t. Hence its type: p->t.

Solving for A

Lets take a look back to remember what were trying to solve. One thing we need to find is A:

(λy:p->ø.
   (λz:p.((x:p->ø->t z:p):ø->t (y:p->ø z:p):ø):t):p->t
 ):A

We've already determined the inner part to be correct - its p->t. Using what we just learned about creating functions with λ, and what we learned about types earlier, we know that (λy:p->ø. whatever):A builds a function that takes an argument, y:p-ø. That is - an argument y of type function from p to ø.

Additionally, this new function returns an A. But remember that the type of a function is not just its return type, it is (input type -> output type). So A must be the functions input type (which we know to be the type of the argument y, or p->ø) -> the functions return type (which is the return type of the inner statement, which we solved earlier to be p->t).

A is (p->ø)->(p->t).

Solving for B

To Solve for B, we do exactly what we did solving for A.

Recall:

(λx:p->ø->t.
 (λy:p->ø.
   (λz:p.((x:p->ø->t z:p):ø->t (y:p->ø z:p):ø):t):p->t
 ):A
):B

Or:

(λx:p->ø->t.whatever:A):B

Clearly the first half of B (the input type) is (p->ø->t). The output type is the type of whatever, which (from looking just above) is A.

So B is (p->ø->t)->A

And fully expanded:

B is (p->ø->t)->(p->ø)->(p->t)

Formal Listing

This came directly from the book. I'm not sure if I can even legally put this all here. If I hear that I can't, I'll immediately take it down. All the information here is explained in detail above.

x:p->o->t     z:p             y:p->o     z:p
-----------------            ---------------
     (xz):o->t                      (yz):o
--------------------------------------------
                (xy(yz)):t      
           -----------------------
            (λx:p.(xy(yz))t):p->t
-----------------------------------------------
(λy:p->o((λx:p.(xy(yz))t)p->t)): (p->o)->(p->t)
------------------------------------------------
(λx:p->o->t ((λy:p->o((λx:p.(xy(yz))t)p->t)): 
  (p->o)->(p->t))): (p->o->t)->(p->o)->(p->t)

The Scala Code To Prove It

trait Lambda {
  type p
  type ø
  type t
  type A = (p=>ø)=>(p=>t)
  type B = (p=>ø=>t)=>A

  val f:B = {(x: p => ø => t) => {(y: p => ø) => {(z: p) => {(x(z)(y(z)))}}}}
}