11 Compiling to System-F🔗

In this lecture we will conclude our discussion of System-F by understanding more about its expressivity: we will see how to compile simply-typed lambda calculus programs into System-F. Then we will more deeply explore the connection between programming languages, type systems, and logic via the Curry-Howard correspondence.

11.1 Church Encoding for System-F🔗

System F is surprisingly expressive. Consider the following abstract syntax for PairLang, a small language with pairs and Booleans:

> (define-type PairLang     (boolE [b : Boolean])     (andE [e1 : PairLang] [e2 : PairLang])     (pairE [e1 : PairLang] [e2 : PairLang])     (fstE [e : PairLang])     (sndE [e : PairLang]))

PairLang has a simple type system with the following types:

> (define-type PairType     (boolT)     (pairT [t1 : PairType] [t2 : PairType]))

Our goal will be to compile PairLang into System F. In particular, our compiler will be well-typed: it will translate well-typed PairLang programs into well-typed System-F programs. In this lecture, we will use an even more restricted subset of System F that does not even have base types for numbers:

> (define-type typ     (funT [arg : typ] [ret : typ])     (identT [id : Symbol])     (forallT [id : Symbol] [body : typ]))

> (define-type expr     (identF [id : Symbol])     (lamF [arg : Symbol] [t : typ] [body : expr])     (appF [e1 : expr] [e2 : expr])     (tlamF [id : Symbol] [body : expr])     (tappF [e1 : expr] [t : typ]))

We have had a similar exercise before when we designed Church encoding schemes for representing Booleans. Let’s again start with Booleans: how should we compile the PairLang value (boolE #t) into a System-F program? A natural choice is to start from the way we encoded this into the untyped lambda calculus:

\lambda x . \lambda y . x

This is not a System F program yet: we need to add type annotations. This is straightforward enough:

\texttt{f-true} = \Lambda T . \lambda x : T . \lambda y : T . x

This term has type \forall T. T \rightarrow T \rightarrow T. Hence, we can observe that the encoding of type Bool into System F is \forall T. T \rightarrow T \rightarrow T. Similarly, we can define the false encoding:

\texttt{f-false} = \Lambda T . \lambda x : T . \lambda y : T . y

Now, what do we do for \texttt{and}? Once again, we can start with the untyped lambda calculus encoding. Recall that in the untyped setting, we encoded and e1 e2 as e1 e2 false. Once again, we need to add types:

\texttt{f-and}~f_1~f_2 = (f_1~[\forall T . T \rightarrow T \rightarrow T]) ~ f_2 ~ \texttt{f-false}

The type of this term is \forall T . T \rightarrow T \rightarrow T , i.e., Boolean. We will call this type BoolF, short for "System F Boolean".

11.1.1 Compiling Pairs🔗

Now for the new part: compiling pairs.

Similar to compiling Booleans, it’s hard to appreciate how Church encodings work until you use them a bit. Let’s start by compiling pair construction (e_1,~e_2).

Suppose we want to compile (\#t, \#f). Our approach will be to wrap these two values in a function that, when you call it a certain way, yields either the first or the second element. Let’s start with an untyped approach, and then add types. We will use the notation \rightsquigarrow to denote compilation.

(\#t, \#f) \rightsquigarrow \lambda k . k~(\lambda x . \lambda y . x)~(\lambda x . \lambda y . y)

The parameter k is called a continuation. We will be learning a lot more about continuations in our upcoming module on control, but for now, just consider this a preview of some of the ideas. Intuitively, a compiled pair is a function that takes a continuation k, and then calls k with two arguments: the first argument is the first element of the pair, and the second argument is the second element of the pair.

Now, we can encode extracting values from pairs using fst e and snd e. Intuitively, these will work by calling their argument e with the right kind of continuation, one that simply extracts the first argument:

\texttt{fst }e = e~(\lambda \text{fst}. \lambda \text{snd} . \text{fst})

So we have that:

\texttt{fst (\#t, \#f)} \rightsquigarrow (\lambda k . k~(\lambda x . \lambda y . x)~(\lambda x . \lambda y . y)) ~ (\lambda \text{fst}. \lambda \text{snd} . \text{fst})

We can step this pr ogram to see that it evaluates to the Church encoding of #t, as expected:

\begin{align*} &(\lambda k . k~(\lambda x . \lambda y . x)~(\lambda x . \lambda y . y)) ~ (\lambda \text{fst}. \lambda \text{snd} . \text{fst})\\ &\rightarrow (\lambda \text{fst}. \lambda \text{snd} . \text{fst})~(\lambda x . \lambda y . x)~(\lambda x . \lambda y . y))\\ & \rightarrow (\lambda \text{snd} . (\lambda x . \lambda y . x)) ~(\lambda x . \lambda y . y) \\ &\rightarrow (\lambda x . \lambda y . x) \\ \end{align*}

11.1.2 Compilation Rules🔗

We’ve seen the high-level idea of how to do compile PairLang into untyped lambda calculus. Now, we just need to find the typing rules for these programs that make them valid System F.

Let’s look at the example from earlier of compiling (\#t, \#f) to \lambda k . k~(\lambda x . \lambda y . x)~(\lambda x . \lambda y . y)}. What should the types of everything be? In particular, what is the type of k? We know it is a function that takes two arguments of type \forall T . T \rightarrow T, but what is the return type?

The key is that we cannot know the return type of k in advance: depending on whether or not fst or snd is called, a different type may be returned by k. So, k must be parametric in its return type, as follows:

(\#t, \#f) \rightsquigarrow \Lambda X . \lambda k : (\texttt{BoolF} \rightarrow \texttt{BoolF} \rightarrow X).~ k~\texttt{true-f}~\texttt{false-f}

Notice how the type of k depends on the type of the arguments to the pair.

Now, with this intuition, we can give an inference rule to compile general pair (e_1, e_2):

\dfrac{ \tau_1 \rightsquigarrow \tau_1^F \qquad \tau_2 \rightsquigarrow \tau_2^F \qquad e_1 \rightsquigarrow e_1^F \qquad e_2 \rightsquigarrow e_2^F }{(e_1, e_2) : \tau_1 \times \tau_2 \rightsquigarrow \Lambda X . \lambda k : (\tau_1^F \rightarrow \tau_2^F \rightarrow X) . k ~ e_1^F ~ e_2^F }~\text{(C-EPair)}

This rule depends on the ability to compile PairLang terms and types into System F. We’ve seen the rule for compiling Bool:

\dfrac{~}{\texttt{Bool} \rightsquigarrow \forall X . X \rightarrow X \rightarrow X}~\text{(C-TBool)}

It may be the case that we are trying to compile a pair that contains a pair, like ((\#t, \#t), \#f). In this case, we will need to compile pair types as well. We know which type pairs should have, since we know how to compile pair values, so we can write this rule:

\dfrac{\tau_1 \rightsquigarrow A \qquad \tau_2 \rightsquigarrow B} {\tau_1 \times \tau_2 \rightsquigarrow \forall T . (A \rightarrow B \rightarrow T) \rightarrow T}~\text{(C-TPair)}

Now, we can compile the destructors fst and snd. This is quite a bit simpler: the only tricky part is that we need to call the continuation with the right type parameter:

\dfrac{e : \tau_1 \times \tau_2 \qquad \tau_1 \rightsquigarrow \tau_1^F \qquad \tau_2 \rightsquigarrow \tau_2^F \qquad \qquad e \rightsquigarrow e^F} {\texttt{fst}~e \rightsquigarrow (e^F [\tau_1^F])~(\lambda \text{fst} : \tau_1^F. \lambda \text{snd} : \tau_2^F .~\text{fst}) }~\text{(C-EFst)}

\dfrac{e : \tau_1 \times \tau_2 \qquad \tau_1 \rightsquigarrow \tau_1^F \qquad \tau_2 \rightsquigarrow \tau_2^F \qquad \qquad e \rightsquigarrow e^F} {\texttt{snd}~e \rightsquigarrow (e^F [\tau_2^F])~(\lambda \text{fst} : \tau_1^F. \lambda \text{snd} : \tau_2^F .~\text{snd})}~\text{(C-ESnd)}

Finally, we can give an implementation of this compiler in Plait, which is available here (you will also need to include the implementation for System F here):

11.2 Programming and Logic🔗

Many of the ideas in this section are paraphrasings and summaries of this excellent article:

Wadler, Philip. "Propositions as types." Communications of the ACM 58.12 (2015): 75-84.

The intellectual and technical development of programming languages is deeply intertwined with logic. This connection is fabulously deep; we will only touch on it here.

The connection between logic and programming is as follows:

• Propositions are types.

  Propositions are statements in some logic. For example, a proposition might be "if it is raining, then I get wet".

• Proofs are programs (i.e., inhabitants of types).

  Suppose I want to prove the fact that "if it is raining, then I get wet." To show you this, I can write you a program that consumes the "raining" fact and produces a "wet" fact.

• Simplification of proofs is evaluation of programs.

  Suppose I know that it is raining. Then, I can combine this fact with the fact that "if it is raining, then it is wet" to conclude that it is wet. This simplifies the world, and looks like beta reduction: I plugged in knowledge of raining into my program and learned that it is wet.

The above set of analogies is often called the Curry-Howard correspondence between types and programs. This is all very abstract. It begs a concrete question: what kinds of propositions can my type systems show, and what does it look like to "prove" things in them?

Let’s consider just the simply-typed lambda calculus with numbers and pairs. Suppose I want to show a simple statement like "If A is true, and A implies B, then B must be true".

Here is how. First, we translate this statement into some type: remember, propositions are types. In System F, this is quite natural because of how we chose our notation:

\forall A, B. A \rightarrow (A \rightarrow B) \rightarrow B

We can read this type as "if you give me a proof that A is true, and a proof that A implies B, then B is true". Note that base types (like "A") denote atomic facts that are true without further effort, while function types (like "A \rightarrow B" denote implications) denote facts that are only true if you satisfy their premises by giving them an argument.

Now, to prove Modus ponens, we use the analogy between proofs and programs: we find a System F program that has this type! Here it is:

\Lambda A . \Lambda B . \lambda a : A . \lambda f : (A \rightarrow B) . f ~ a

The above program is a proof of Modus ponens!

Other kinds of types also get logical interpretations. What about pairs? Pairs let us combine two proofs into a single proof: this is logical conjunction.

Let’s extend System F with syntactic pairs (we’ve just seen how this isn’t strictly necessary, and System F already has pairs in it, but this makes the examples simpler). Let’s prove the following obvious fact: "If A and B are both true, then A must be true".

First, let’s translate this into a type. Easy enough:

\forall A, B. A \times B \rightarrow A

Now, a proof: let’s find a program that inhabits this type. Again, this is quite easy: this is simply the first projection!

\Lambda A . \Lambda B . \lambda p : A \times B . \texttt{fst}~p

The Curry-Howard correspondence has been leveraged to design amazingly powerful tools called proof assistants for proving things in programming languages like Rocq and Lean. The core idea of these systems follows exactly the structure we saw above. First, you design a very powerful type system that is expressive enough to state very rich propositions like "the product of any two numbers with 2 is even". Then, the proof assistant will help you find a program that inhabits that type, and the type checker will check that the theorem is true! These proof assistants have been used to create formally verified software in many settings including aviation and compilers.