System F

System F, also referred to as the polymorphic \lambda-calculus (PLC), is a typed \lambda-calculus that allows abstraction and application of types.

System F has multiple uses:

• Computationally, System F is the quintessential system that encodes the notion of parametric polymorphism in programming languages.
• Proof-theoretically, it is a presentation of proofs of second-order propositional logic.
• Logically, it supports a functional interpretation of second-order Heyting arithmetic.

Syntax

There are many sligthly different but equivalent ways to introduce System F. Perhaps the cleanest one is to adopt two judgments, one for types and one for terms.

The pre-types of System F are introduced by the grammar

T ::=\ X\ \mid T \to T \mid\ \forall X. T

where X comes from a finite set of type variables.

The types of System F are best given by a judgment. This has the form \Delta \vdash A \textsf{ type} where \Delta is a finite list of type variables. If \Delta = X_1, \ldots X_n, the intended meaning is that A is a type assuming the X_i are.

There are no basic types (!), but two type constructors: functions, and universal quantification.

\frac{}{\Delta, X, \Delta' \vdash X \textsf{ type}}
\qquad
\frac{
	\Delta \vdash A \textsf{ type}
  \quad
  \Delta \vdash B\textsf{ type}
}{
	\Delta \vdash A \rightarrow B \textsf{ type}
}
\qquad
\frac{
	\Delta, X \vdash B \textsf{ type}
}{
	\Delta \vdash \forall X. B \textsf{ type}
}

The typing rules are of the form \Delta \mid \Gamma \vdash M : A, where \Delta is a variable context (as above), and \Gamma is the usual list of pre-types assigned to variables x : A. We have the usual rules of the simply-typed \lambda-calculus, which are given parametrically in \Delta:

\frac{}{
	\Delta \mid \Gamma, x : A, \Gamma' \vdash x : A
}
\qquad
\frac{
	\Delta \mid \Gamma, x : A \vdash M : B
}{
	\Delta \mid \Gamma \vdash \lambda x : A.\ M : A \to B
}
\qquad
\frac{
	\Delta \mid \Gamma \vdash M : A \to B
  \quad
  \Delta \mid \Gamma \vdash N : A
}{
	\Delta \mid \Gamma \vdash M\,N : B
}

The novel part is the rules for polymorphic/universal abstraction and application:

\frac{
	\Delta, X \mid \Gamma \vdash M : A
}{
	\Delta \mid \Gamma \vdash \Lambda X. M : \forall X. A
}
\qquad
\frac{
	\Delta \mid \Gamma \vdash M : \forall X. A
  \quad
  \Delta \vdash B \textsf{ type}
}{
	\Delta \mid \Gamma \vdash M(B) : A[B/X]
}

The first one abstracts away a variable in the type context, hence introducing a polymorphic type \forall X. A. The second one allows you to apply a polymorphic term to a type. This makes the quantifier vanish, and replaces the type variable X with the type B in the type A.

Recall that the context \Gamma consists of pairs of variables and pre-types. We have the following 'presupposition-type' lemma: if \Delta \vdash A_i \textsf{ type} for every x_i : A_i \in \Gamma, and \Delta \mid \Gamma \vdash M : A, then \Delta \vdash A \textsf{ type} already.

Insert example derivation of \lambda X. \lambda x : X.\ x.

The reduction rules for System F are based on straightforward \beta-reductions both term and type abstraction:

(\lambda x : T. M)(N) \longmapsto M[N/x]
\qquad
(\Lambda X. M)(B) \longmapsto M[B/X]

Expressive power

There are two ways to discuss the expressive power of System F:

• as a programming language
• on computing natural numbers

As a programming language

System F is exceptionally powerful as a formalism for programming, as it can encode many data types of interest through a device called Church encoding. To quote Cardelli 1997:

It turns out that virtually any basic type of interest can be encoded within F_2.Similarly ,product types, sum types, existential types, and some recursive types, can be encoded within F_2: polymorphism has an amazing expressive power.

As such, it is (somewhat) tenable to think of System F as an analogue of the untyped \lambda-calculus at the type level. The problem is that System F terms always normalize, so it is not expressive enough to be a real programming language; this can be mended by adding a fixed point combinator as an additional term Pitts 2000.

The standard references for encoding data types are Leivant 1983, Bohm and Berrarduci 1985, Proofs and types Chapter 11, and Reynolds and Plotkin 1993.

However, it should be noted that the encodings of various data types (lists, trees, etc.) is computationally adequate, but does not satisfy various extensionality principles - in fact, not even \eta! This corresponds to being able to construct only weak initial algebas for an algebraic signature Reynolds and Plotkin 1993.

Thus, while many data types can be encoded in System F, reasoning about them is not particularly easy, as many useful principles do not hold. Incidentally, this is the reason why Coq switched from being based on the Calculus of Constructions - which used Church encodings for all user-defined data types - to the Calculus of Inductive Constructions.

On natural numbers

Suppose we encode natural numbers in System F using a simple Church encoding:

\textsf{Int} = \forall X. X \to (X \to X) \to X

The question is then: which functions f : \mathbb{N} \to \mathbb{N} can be encoded as terms \vdash M : \textsf{Int} \to \textsf{Int}?

It was shown by Girard that

Theorem. The functions representable in F are the ones that can be proved to be total by second-order Peano arithmetic (\textbf{PA}_2).

For a proof see Proofs and Types, chapter 15.

Semantics

Please expand.

Set-theoretic models

In his first paper on System F, Reynolds 1984 sketched a set-theoretic semantics for System F. However, he almost immediately realized that such a model cannot exist, because of cardinality constraints Reynolds 1984b. The technical argument of why this cannot happen is generalized and simplified by Reynolds and Plotkin 1993.

However, the cardinality argument is vaguely classical. Pitts 1987 and Longo and Moggi 1991 proved that there can be set-theoretic models of System F, as long as the ambient set theory itself is intuitionistic. However, even that is subject to limitations, in that the polymorphic types cannot be the obvious kind of 'big product': Pitts 1989 proves that no powerset of a type can be contained in a polymorphic type, in any model that can be embedded in a topos.

References

• There are textbook treatments of System F in TAPL (ch. 23), PFPL (2nd ed, ch. 16), and Proofs and Types (ch. 11).

• System F was first introduced by Jean-Yves Girard around 1970 in his thesis:

@phdthesis{girard_interpretation_1972,
	type = {Th\`{e}se d'\'{E}tat},
	title = {Interpr\'{e}tation fonctionelle et élimination des coupures de l'arithm\'{e}tique d'ordre sup\'{e}rieur},
	school = {Universit\'{e} Paris VII},
	author = {Girard, Jean-Yves},
	year = {1972}
}

• Completely independently, Reynolds also discovered the same system:

@inproceedings{reynolds_1984,
	address = {Amsterdam},
	title = {Types, {Abstraction}, and {Parametric} {Polymorphism}},
	booktitle = {Information {Processing} 83: {Proceedings} of the {IFIP} 9th {World} {Computer} {Congress}, {Paris}, {France}, {September} 19-23, 1983},
	publisher = {Elsevier Science Publishers B. V. (North-Holland)},
	author = {Reynolds, John C.},
	editor = {Mason, R. E. A},
	year = {1984},
	pages = {513--523},
}

• The expressive power of System F is documented in Chapter 11 of Proofs and Types, as well as the following original papers:

@article{bohm_1985,
	title = {Automatic synthesis of typed Λ-programs on term algebras},
	volume = {39},
	doi = {10.1016/0304-3975(85)90135-5},
	journal = {Theoretical Computer Science},
	author = {Böhm, Corrado and Berarducci, Alessandro},
	year = {1985},
	pages = {135--154},
}

@inproceedings{leivant_reasoning_1983,
	title = {Reasoning about functional programs and complexity classes associated with type disciplines},
	doi = {10.1109/SFCS.1983.50},
	booktitle = {24th {Annual} {Symposium} on {Foundations} of {Computer} {Science} (sfcs 1983)},
	publisher = {IEEE},
	author = {Leivant, Daniel},
	year = {1983},
	pages = {460--469},
}

@article{reynolds_functors_1993,
	title = {On {Functors} {Expressible} in the {Polymorphic} {Typed} {Lambda} {Calculus}},
	volume = {105},
	doi = {10.1006/inco.1993.1037},
	number = {1},
	journal = {Information and Computation},
	author = {Reynolds, J.C. and Plotkin, G.D.},
	year = {1993},
	pages = {1--29},
}

• The argument that there are no set-theoretic models of polymorphism in a classical setting is given in

@incollection{reynolds_1984b,
	address = {Berlin, Heidelberg},
	title = {Polymorphism is not set-theoretic},
	volume = {173},
	booktitle = {Semantics of {Data} {Types}},
	publisher = {Springer Berlin Heidelberg},
	author = {Reynolds, John C.},
	editor = {Wirth, N. and Kahn, Gilles and MacQueen, David B. and Plotkin, Gordon},
	year = {1984},
	doi = {10.1007/3-540-13346-1_7},
	series = {Lecture Notes in Computer Science},
	pages = {145--156},
}

@article{reynolds_functors_1993,
	title = {On {Functors} {Expressible} in the {Polymorphic} {Typed} {Lambda} {Calculus}},
	volume = {105},
	doi = {10.1006/inco.1993.1037},
	number = {1},
	journal = {Information and Computation},
	author = {Reynolds, J.C. and Plotkin, G.D.},
	year = {1993},
	pages = {1--29},
}

• The argument that polymorphism can be given set-theoretic models constructively is given in

@incollection{pitts_1987,
	title = {Polymorphism is set theoretic, constructively},
	volume = {283},
	isbn = {978-3-540-18508-6},
	url = {https://www.cl.cam.ac.uk/~amp12/papers/polist/polist.pdf},
	booktitle = {Category {Theory} and {Computer} {Science}},
	publisher = {Springer, Berlin, Heidelberg},
	author = {Pitts, A. M.},
	editor = {Pitt, D.H. and Poigné, A. and Rydeheard, D.E.},
	year = {1987},
	doi = {10.1007/3-540-18508-9_18},
	note = {ISSN: 16113349},
	pages = {12--39},
	file = {Pitts - 1987 - Polymorphism is set theoretic, constructively.pdf:C\:\\Users\\Alex\\Zotero\\storage\\S55W8DH6\\Pitts - 1987 - Polymorphism is set theoretic, constructively.pdf:application/pdf},
}

@article{longo_1991,
	title = {Constructive natural deduction and its ‘ω-set’ interpretation},
	volume = {1},
	doi = {10.1017/S0960129500001298},
	number = {2},
	journal = {Mathematical Structures in Computer Science},
	author = {Longo, Giuseppe and Moggi, Eugenio},
	year = {1991},
	pages = {215--254},
}

@inproceedings{pitts_1989,
	title = {Non-trivial power types can't be subtypes of polymorphic types},
	doi = {10.1109/LICS.1989.39154},
	booktitle = {[1989] {Proceedings}. {Fourth} {Annual} {Symposium} on {Logic} in {Computer} {Science}},
	publisher = {IEEE Computer Society Press},
	author = {Pitts, A.M.},
	year = {1989},
	pages = {6--13},
}