nLab System F

Idea

System F, also known as the polymorphic lambda-calculus or second-order lambda-calculus, is an extension of simply typed lambda-calculus to include a type of impredicative universal quantification.

Semantics

Models of System F can be described as a form of hyperdoctrine:

1. A category K of kinds with cartesian products.
2. A functor $P \colon K^o \to CCC$, i.e., a contravariant functor from $K$ to the category of cartesian closed categories and functors preserving the CC structure.
3. A representing object $U \in K$, i.e., $K(-,U) \cong P_0$ where $P_0 : K^o \to Set$ is the presheaf of objects of the corresponding CCC.
4. Such that for any $\Delta \in K$, the functor $P(\pi) \colon P(\Delta) \to P(\Delta \times U)$ induced from the projection $\pi \colon \Delta \times U \to \Delta$ has a right adjoint $\forall \colon P(\Delta \times U) \to P(\Delta)$ satisfying a Beck-Chevalley condition.

Typically, the objects of the category of kinds are restricted to be generated by products of $U$.

Note that this models the $\beta\eta$ equivalence of System F only, not the more complex notion of relational parametricity?. A relationally parametric model of System F is

1. A model of System F internal to the category of reflexive graphs
2. Such that the functor $(s,t) : P_e(\Delta_e) \to P_v(s(\Delta_e)) \times P_v(t(\Delta_e))$ is a fibration.

Note that by taking the “vertex” component of such a model, we get an underlying ordinary “equational” model of System F, and so we can see a relatonally parametric model as an extension of an equational model. The internalization to reflexive graphs models the relational structures: the “edge” components are the relations, the source/target maps ensure that each relation lies over an ordinary structure, and the reflexive edge models the notion of an identity/equality relation. The fibration requirement then provides a rich supply of relations: given a relation R and morphisms $f_s : B_s \to s(R)$ and $f_t : B_t \to t(R)$, the fibration structure defines a “weakest pre-relation” $R[f_s,f_t]$ with source and target $B_s,B_t$. Notably, if $R$ is an identity relation and one of $f_s,f_t$ is the identity, this is a kind of graph relation of a morphism. Compare the definition of a virtual equipment, where the reflexive edges are analogous to the units and the fibration structure is analogous to the restrictions.

Related concepts

• dependent type theory with type variables

References

The calculus now called System F was developed independently in the following works:

• Jean-Yves Girard, Interprétation functionelle et élimination des coupures dans l’arithmétique d’ordre supérieure, Ph.D. thesis, Université Paris VII (1972) [pdf, pdf]

• John C. Reynolds, Towards a theory of type structure, Programming Symposium, 1974 (doi)

The hyperdoctrine-like notion of model:

• R.A.G. Seely, Categorical Semantics for Higher Order Polymorphic Lambda Calculus, Journal of Symbolic Logic, Vol. 52, Issue 4, December 1987 (doi)

The reflexive graph/fibrational view of parametricity:

• Brian Dunphy and Uday Reddy, Parametric Limits, Logic in Computer Science 1994 (doi)