System FAn introduction by Franck Binard
In which, every type Si will be in the general format:
Each Si is the type of a function fi that constructs an object of type X. fi is typed as S1→S2→→Sn→Si and takes ki arguments of type T1,T2,,Tki, returning a value of type X:
Recursion happens when one of the Tik has an imbedded type X. It means a constructor will take an object of its own type as argument.
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:
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:
The sum type is defined as:
Given and , we define:
Now, when we look at the formation:
where , , and , we see that:
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)
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.
Complex types are defined in exactly the same manner as simple types.
The type Int(X) is created from two constructors:
Which types the constructors as:
and defines the type Int(X) as:
from which, we get:
Where the number n is the application of a function f n times.
Given u:U and f:U→U, we get:
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,
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:
So for example, Attach which attaches an element to the end of a list is defined as:
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.
Franck J.L. Binard
School of Information Technology and Engineering (SITE)
University of Ottawa
800 King Edward Ave.
Ottawa, Ontario, Canada, K1N 6N5
Tel: (613) 562-5800 x6727, Fax: (613) 562-5664
Office: 4-035 SITE
Contactez: L'cole d'ingnierie et de technologie de l'information
Contact: School of Information Technology and Engineering
Copyright 2001 Universit d'Ottawa / University of Ottawa
Webmestre / Webmaster