Representing lists and trees in System F

Question

System F (also known as second-order lambda calculus or polymorphic lambda calculus) is defined as follows.

Types are defined starting from type variables $X, Y, Z, \ldots$ by means of two operations:

1. if U and V are types, then $U\rightarrow V$ is a type

2. if V is a type, and X a type variable, then $\Pi X.V$ is a type

There are five schemes for forming terms:

variables: $x^T,y^T,z^T,\ldots$ of type T

application: tu of type V, where t is of type $U\rightarrow V$ and $u$ is of type $U$

$\lambda$-abstraction: $\lambda u.v $ of type $U\rightarrow V$ where $x^U$ is a variable of type U and v is of type V

universal abstraction: if v is a term of type V, then we can form $\Lambda X.v$ of type $\Pi X.V,ドル so long as the variable X is not free in the type of a free variable of v

universal application if t is a term of type $\Pi X.V$ and U is a type, then tU is a term of type V[U/X]

Now, what I ask is a simple and informal explanation (or alink to an article or book that has it) of how it is possible to encode data strutures like lists and trees using System F. I understand Church numerals, but I can't go on with more complicated structures.

Church encoding

Using untyped lambda calculus it is easier to do that, because you don't have types to worry about types.

$$\operatorname{pair} \equiv \operatorname{cons} \equiv \lambda x.\lambda y.\lambda z.z\ x\ y $$ $$\operatorname{first} \equiv \lambda p.p\ (\lambda x.\lambda y.x) $$ $$\operatorname{second} \equiv \lambda p.p\ (\lambda x.\lambda y.y) $$ $$\operatorname{true} \equiv \lambda a.\lambda b.a$$ $$\operatorname{nil} \equiv \operatorname{pair}\ \operatorname{true}\ \operatorname{true}$$

For example, $$ \operatorname{first}\ (\operatorname{pair}\ a\ b) $$ $$ \rightarrow_\beta (\lambda p.p\ (\lambda x.\lambda y.x))\ ((\lambda x.\lambda y.\lambda z.z\ x\ y)\ a\ b) $$ $$ \rightarrow_\beta (\lambda p.p\ (\lambda x.\lambda y.x))\ (\lambda z.z\ a\ b) $$ $$ \rightarrow_\beta (\lambda z.z\ a\ b)\ (\lambda x.\lambda y.x) $$ $$ \rightarrow_\beta (\lambda x.\lambda y.x)\ a\ b = a $$

So the list (1, 2, 3) will be represented as (cons 1 (cons 2 (cons 3 nil))).

System F

In System F things get complicated, as you can see from the following definitions from page 90 of Proofs And Types by Jean-Yves Girard, Paul Taylor and Yves Lafont :

$$\operatorname{List U} = \Pi X.X\rightarrow (U\rightarrow X\rightarrow X)\rightarrow X$$ $$\operatorname{nil} = \Lambda X. \lambda x^X. \lambda y^{U\rightarrow X\rightarrow X}. x$$ $$\operatorname{cons u t } = \Lambda X. \lambda x^X. \lambda y^{U\rightarrow X\rightarrow X}. y u (tX x y)$$

I can't understand their meaning.

• Nikolaj-K: I'm a layman on this, so grant me my question: Why doesn't the previous approach work anymore if you add polymorphism? I'd guess you must only type the abstracted variables as function types accordinly.
• Vitaly Olegovitch: @NikolajK. Thank you for the link! I have modified my question and added a comparison between Church encoding and System F.
• Nikolaj-K: I take it you have that from page 90 of paultaylor.eu/stable/prot.pdf?
• Vitaly Olegovitch: @NikolajK. that is right. I have added the reference to my question. But I can't understand it.

Answer 1

The way I understand these types is by thinking of what functions I can build that satisfy the signature.

Booleans

For booleans, we have the type $\Pi\alpha . \alpha \rightarrow \alpha \rightarrow \alpha$. All members of this type will take in two abstract values (that is, values of type $\alpha,ドル where $\alpha$ can be anything) and return an abstract value (an $\alpha$).

In System F, there are exactly two functions that match this signature: $(\lambda x . \lambda y . x)$ and $(\lambda x . \lambda y . y)$. We can name them true and false and properly claim "all booleans are either true or false".

Integers

Integers have the type $\Pi\alpha . \alpha \rightarrow (\alpha \rightarrow \alpha) \rightarrow \alpha$. All members of this type need to be functions that take in two things: an abstract value and a function on abstract values, and return an abstract value.

(Again, we don't know anything about what type $\alpha$ actually is, nor do we know what the function of type $(\alpha \rightarrow \alpha)$ does. It could be the identity, it could be the successor function, it could accept a list and return the empty list.)

One function that matches this signature is $(\lambda x . \lambda f . x)$. Another is $(\lambda x . \lambda f . f x)$. Yet another is $(\lambda x . \lambda f . f (f x))$. There are countably many of these functions, so we can put them in one-to-one correspondence with the natural numbers and name them 0, 1, 2, ... . The only difference between these and Church numerals is that you can only apply them to values $x$ and $f$ with the right type.

Lists & Trees

After integers, lists and trees are easy. The type for lists, like you said, is $\Pi \alpha . \alpha \rightarrow (U \rightarrow \alpha \rightarrow \alpha) \rightarrow \alpha$. Again, members of this type take in two arguments, an abstract value and a function that can manipulate abstract values, and returns an abstract value. The interesting part is the type $U,ドル which Girard uses to denote the type of elements in the list. A List Boolean has type $\Pi \alpha . \alpha \rightarrow (Boolean \rightarrow \alpha \rightarrow \alpha) \rightarrow \alpha$.

We can easily define a function nil as $(\lambda x . \lambda f . x)$. That's one way to return a list given the arguments $x$ and $f$. The only other thing we can do to return a list is to apply the function $f$; given a value $u$ of type $U,ドル we could make the function $(\lambda x . \lambda f . f u x)$. If we parameterize over the value $u,ドル we get a more familiar cons function: $(\lambda u . \lambda x . \lambda f . f u x)$. Its type is $\Pi U . \Pi \alpha . \alpha \rightarrow (U \rightarrow \alpha \rightarrow \alpha) \rightarrow \alpha$.

Trees have the type $\Pi \alpha . \alpha \rightarrow (U \rightarrow \alpha \rightarrow \alpha \rightarrow \alpha) \rightarrow \alpha$. You just add another branch!

Example: Lists in other Programming Languages

A list is one of two things:

• Empty
• Non empty, so we can think of it as one element attached to a smaller list

Let's stick to lists of integers, which Girard would describe with the type $\Pi \alpha . \alpha \rightarrow (Integer \rightarrow \alpha \rightarrow \alpha) \rightarrow \alpha$. His empty list is $\alpha,ドル the first argument, and his non-empty list is the second argument (which is a function expecting one element and another list).

In Java, we could represent these two alternatives by making an interface and a pair of classes. interface IntList {} class Empty implements IntList {} class Cons implements IntList { int head; IntList tail; }

The Cons class has fields representing the two parts of any non-empty list.

In OCaml, things look a little more like System F. type int_list = Empty | Cons of int * int_list

Again, there are two alternatives. A list can be Empty, or it can be a pair like Cons(2, Empty) made of an element and another list.

Girard's type is difficult to read because he expresses these ideas with one $\Pi$-type, but the idea's the same.

• lisyarus: Could you elaborate a bit on the intuition behind the definition of List?
• ben: I added examples above. Do they help?
• rlms: I don't think your cons is right. There are two problems. Firstly, you gave the type of cons as being the same as the type of list, when it should be U -> list -> list. Secondly, your definition of the function is of type U -> list, which is neither of those. I believe the correct definition of cons is \u \l \x \f . f u (l x f). Also, your examples of functions are written in untyped syntax which is a bit confusing when the question is about System F specifically.

Answer 2

Pages 347-353 of the Types and Programming Languages book explain these encodings in detail. The main idea is this: "for lists, where a list with elements x, y, and z is represented as a function that, given any function f and starting value v, calculates f x (f y (f z v)). In OCaml terminology, a list is represented as its own fold_right function. The type List X of lists with elements of type X is defined as follows:

List X = ∀R. (X→R→R) → R → R;

The nil value for this representation of lists is easy to write.

nil = λX. (λR. λc:X→R→R. λn:R. n) as List X;
nil : ∀X. List X

The cons and isnil operations are also easy:

cons = λX. λhd:X. λtl:List X.
 (λR. λc:X→R→R. λn:R. c hd (tl [R] c n)) as List X;
cons : ∀X. X → List X → List X
isnil = λX. λl:List X. l [Bool] (λhd:X. λtl:Bool. false) true;
isnil : ∀X. List X → Bool"