natural deduction metalanguage, practical foundations
type theory (dependent, intensional, observational type theory, homotopy type theory)
computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory
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.
Models of System F can be described as a form of hyperdoctrine:
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
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.
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:
The reflexive graph/fibrational view of parametricity:
Last revised on August 17, 2022 at 08:57:19. See the history of this page for a list of all contributions to it.