System F, also referred to as the polymorphic -calculus (PLC), is a typed -calculus that allows abstraction and application of types.
System F has multiple uses:
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
where comes from a finite set of type variables.
The types of System F are best given by a judgment. This has the form where is a finite list of type variables. If , the intended meaning is that is a type assuming the are.
There are no basic types (!), but two type constructors: functions, and universal quantification.
The typing rules are of the form , where is a variable context (as above), and is the usual list of pre-types assigned to variables . We have the usual rules of the simply-typed -calculus, which are given parametrically in :
The novel part is the rules for polymorphic/universal abstraction and application:
The first one abstracts away a variable in the type context, hence introducing a polymorphic type . The second one allows you to apply a polymorphic term to a type. This makes the quantifier vanish, and replaces the type variable with the type in the type .
Recall that the context consists of pairs of variables and pre-types. We have the following 'presupposition-type' lemma: if for every , and , then already.
Insert example derivation of .
The reduction rules for System F are based on straightforward -reductions both term and type abstraction:
There are two ways to discuss the expressive power of System F:
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 .Similarly ,product types, sum types, existential types, and some recursive types, can be encoded within : polymorphism has an amazing expressive power.
As such, it is (somewhat) tenable to think of System F as an analogue of the untyped -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 ! 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.
Suppose we encode natural numbers in System F using a simple [Church encoding]:
The question is then: which functions can be encoded as terms ?
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 ().
For a proof see Proofs and Types, chapter 15.
Please expand.
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.
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:
Girard, Jean-Yves. 1972. ‘Interprétation Fonctionelle et Élimination Des Coupures de l’arithmétique d’ordre Supérieur’. Thèse d’État, Université Paris VII.
[pdf]
@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}
}
Reynolds, John C. ‘Types, Abstraction, and Parametric Polymorphism’. In Information Processing 83: Proceedings of the IFIP 9th World Computer Congress, Paris, France, September 19-23, 1983, edited by R. E. A Mason, 513–23. Amsterdam: Elsevier Science Publishers B. V. (North-Holland), 1984. [pdf]
@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},
}
Böhm, Corrado, and Alessandro Berarducci. ‘Automatic Synthesis of Typed Λ-Programs on Term Algebras’. Theoretical Computer Science 39 (1985): 135–54. https://doi.org/10.1016/0304-3975(85)90135-5.
@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},
}
Leivant, Daniel. ‘Reasoning about Functional Programs and Complexity Classes Associated with Type Disciplines’. In 24th Annual Symposium on Foundations of Computer Science (Sfcs 1983), 460–69. IEEE, 1983. https://doi.org/10.1109/SFCS.1983.50.
@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},
}
Reynolds, J.C., and G.D. Plotkin. ‘On Functors Expressible in the Polymorphic Typed Lambda Calculus’. Information and Computation 105, no. 1 (1993): 1–29. https://doi.org/10.1006/inco.1993.1037. [pdf]
@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},
}
@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},
}
Reynolds, J.C., and G.D. Plotkin. ‘On Functors Expressible in the Polymorphic Typed Lambda Calculus’. Information and Computation 105, no. 1 (1993): 1–29. https://doi.org/10.1006/inco.1993.1037. [pdf]
@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},
}
Pitts, A. M. ‘Polymorphism Is Set Theoretic, Constructively’. In Category Theory and Computer Science, edited by D.H. Pitt, A. Poigné, and D.E. Rydeheard, 283:12–39. Springer, Berlin, Heidelberg, 1987. https://doi.org/10.1007/3-540-18508-9_18. [pdf]
@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},
}
Longo, Giuseppe, and Eugenio Moggi. ‘Constructive Natural Deduction and Its “ω-Set” Interpretation’. Mathematical Structures in Computer Science 1, no. 2 (1991): 215–54. https://doi.org/10.1017/S0960129500001298. [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},
}
Pitts, A.M. ‘Non-Trivial Power Types Can’t Be Subtypes of Polymorphic Types’. In [1989] Proceedings. Fourth Annual Symposium on Logic in Computer Science, 6–13. IEEE Computer Society Press, 1989. https://doi.org/10.1109/LICS.1989.39154. [pdf]
@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},
}