System F

An introduction by Franck Binard

Free Structures

Free structures are the bread and butter of programming. They are computational tools used by programmers to add specific behaviour to their programs. Iterative and recursive structures and data types are examples of free structures.

Example 1

Suppose you needed to model the structure of a traffic light. A traffic light can be represented as three constants (red, green, blue). The type

[TrafficLight] = [ΠX.X→X→X→X]
represents exactly this structure. The scheme used to obtain these types is described below. Once you have the type, there are three possible objects of that type that can be defined:

red = ΛXλx.λy.λz.x
green = ΛXλx.λy.λz.y
orange = ΛXλx.λy.λz.z

So suppose you have the three functions, careful, normal, stop, each of type [DrivingStyle]. The sentence:

traffic_light [DrivingStyle] stop normal careful
expresses normal driving behavior (traffic_light is of course an object of type [TrafficLight]) when facing a traffic light. This structure is an example of a set constants. These are mostly used for decisions and branching. The Boolean set is just the special case with two constants.

Example 2

Suppose we'd like to model play behaviour in an environment where an object of type [Toy] may be either a [Ball] or a [Puzzle]. We model this as:

[Toy]=[Π X . (Ball→X)→(Puzzle→X)→X]
If we have access to the two functions:

solve:[Puzzle→Behaviour]
kick:[Ball→Behaviour]

then the following function expresses the logical expected behaviour:

λx^Toy.x [Behaviour] kick solve

Example 3

A [StairCase] is a [Floor] or a [Stair] followed by a [StairCase]. We model this structure with the type:

[StairCase] = [(Floor→X)→(Stair→X→X)→X]
given walk:[Floor→Action] and climb_next:[Stair→Action→Action], we can encode the behaviour:
λx^StairCase.x [Action] walk climb_next

So, for a example a staircase of three stairs represented as s1 (s2 (s3 floor)) becomes climb_next s1 (climb_next s2 (climb_next s3 (walk floor))) when passed as the argument to the function.
To do: provide more explaination as to the encoding for s1 (s2 (s3 floor))

General Scheme

There is a general scheme to the representation of free structures. It is detailed in chapter 11 of Girard’s Proof and Types and is based on the fact that all structures will be typed according to the generic type structure:

In which, every type S_i will be in the general format:

Each S_i is the type of a function f_i that constructs an object of type X. f_i is typed as S1→S2→→Sn→Si and takes k_i arguments of type T1,T2,,Tki, returning a value of type X:

Recursion happens when one of the T_ik has an imbedded type X. It means a constructor will take an object of its own type as argument.

Section 1.06 The simple types

(a) The Boolean Type

Booleans are formed from two constants: T and F. Therefore, we have:

S1≡X and S2≡X

giving a general type:

with the terms defined as:

So that given terms u, v of type U:

And

(b) The Pair Type

Pairs are formed using only one constructor which takes an object of type U, another object of type V and return an object of type U×V.

The type U×V can then be defined as:

with defined as the term:

From which can be deduced the following projection terms:

So that given terms u, v of type U, V:

and

(c) The Sum Type

The sum type is defined as:

Given and , we define:

Now, when we look at the formation:

where , , and , we see that:

and

This links to the Curry-Howard isomorphism like this: An object with type (corresponding to a proof of R implies U) , an object with type (corresponding to a proof of S implies U) and an object with type (corresponding to a proof of R or S) will provide a proof of U (an object of type U)

(d) The Existential Type

The Existential type is defined as:

From which, we can define where as:

And we now see that given :

Here, the mechanical use of the construction scheme outlined by Girard seems to break down. There’s another example below where that happens again.

Section 1.07 Inductive types

Complex types are defined in exactly the same manner as simple types.

(a) Integers

The type Int(X) is created from two constructors:

A constant (0) of type Int(X)
A successor function which takes an object of type Int(X) and returns an object of type Int(X)

Which types the constructors as:

and defines the type Int(X) as:

from which, we get:

and

Where the number n is the application of a function f n times.

Given u:U and f:U→U, we get:

and

So for example, the representation of the number 2 is:

We can define the iterator function It in the following way:

We could also define the function Add as:

So for example,

(b) Lists

To form lists, two constructors are also needed, typed as:

(The type of the empty list constant)

(The type of a function that takes an object of type U, a list of type List(U) and returns a list of type List(U) the first element of which is the object of type U and the tail is the list that was passed as argument. So the List(U) type is:

and we have:

and

So for example, Attach which attaches an element to the end of a list is defined as:

Concat is:

Reverse is:

But of course, what we really want is to ensure that the elements of the list can be of any type and that the list will behave the same (all operations that are defined on the list will stay coherent)

Which is where the construction scheme seem to break down again.

We see that the terms of this object have to look like:

But then, we need to know at cons time that the list to which we’re consing is consistent in type to what we are consing it with. I don’t see how this can be done here.