System F

System F is a type system historically developed independently by Jean-Yves Girard and John Reynolds. It enriches simply typed lambda calculus with an impredicative universal quantifier over types.

Logically, it corresponds to second order minimal logic, that is, a second order logic without first-order quantifiers. The idea of having second order quantifications, but not first order ones, stems from the observation that first order quantiication doesn’t have a clear computational interpretation.

Definition

Let us define inductively types as follows

𝑇 ≔ 𝛼 | 𝑇 \to 𝑇 | \forall 𝛼 . 𝑇

then terms

\begin{aligned} 𝑡 ≔ & 𝜆 𝑥 . 𝑡 | 𝑡 𝑡 \\ | & Λ 𝛼 . 𝑡 | 𝑡 𝑇 \\ | & 𝑥 \end{aligned}

We define straightforwardly the typing judgement

𝑥 : 𝐴 \in Γ

Γ ⊢ 𝑥 : 𝐴

Γ, 𝑥 : 𝐴 ⊢ 𝑡 : 𝐵

Γ ⊢ 𝜆 𝑥 . 𝑡 : 𝐴 \to 𝐵

I_{\to}

Γ ⊢ 𝑢 : 𝐴 \to 𝐵

Γ ⊢ 𝑣 : 𝐴

Γ ⊢ 𝑢 𝑣 : 𝐵

E_{\to}

Γ ⊢ 𝑡 : 𝐴

𝛼 \notin fv (Γ)

Γ ⊢ Λ 𝛼 . 𝑡 : \forall 𝛼, 𝐴

I_{\forall}

Γ ⊢ 𝑡 : \forall 𝛼, 𝐴

Γ ⊢ 𝑡 𝑇 : 𝐴 [𝛼 \mapsto 𝑇]

E_{\forall}

Encodings

Impredicative encodings are extremely powerful, as they are enough to define a large class of inductive types with their plain recursor.

The trick is to encode a type as the type of (polymorphic) recursors. Thus, encodings are similar to Church encodings in plain $𝜆$ -calculus.

It should be noted that, although these encodings are logically enough to be as expressive as inductive types, they are computationally bad encodings, in the sense that they are very wasteful. Natural numbers, for instance, end up being represented in a unary form that additionally has extra overhead than plain unary numbers.

Empty type

The empty type is encoded as

𝟎 ≔ \forall 𝛼, 𝛼

Indeed, if I have a term $𝑡 : 𝟎$ , and any type $𝑇$ , one can derive a witness $𝑡 𝑇 : 𝑇$ of $𝑇$ , which makes $𝟎$ validate the ex falso quodlibet principle.

Unit type

The unit type is encoded as

𝟏 ≔ \forall 𝛼, 𝛼 \to 𝛼

as well as having a constructor

⋆ ≔ Λ 𝛼 . 𝜆 𝑥 . 𝑥 : 𝟏

We will prove that every closed value $𝑣 : 𝟏$ has the canonicity property:

𝑣 \equiv ⋆

This will stem from a more general adequacy result.

Natural numbers

Natural numbers are encoded as

ℕ ≔ \forall 𝛼, (𝛼 \to 𝛼) \to 𝛼 \to 𝛼

with

\begin{aligned} 0 & ≔ Λ 𝛼 . 𝜆 𝑠 . 𝜆 𝑧 . 𝑧 \\ 𝑛 + 1 & ≔ Λ 𝛼 . 𝜆 𝑠 . 𝜆 𝑧 . 𝑛 (𝛼, 𝑠 𝑧) \end{aligned}

Product type

Let $𝑈$ , $𝑉$ be two types. We can define

𝑈 \times 𝑉 ≔ \forall 𝛼, (𝑈 \to 𝑉 \to 𝛼) \to 𝛼

and, for $𝑢 : 𝑈$ and $𝑣 : 𝑉$ , we have

(𝑢, 𝑣) ≔ Λ 𝛼 . 𝜆 𝑓 . 𝑓 (𝑢, 𝑣)

Sum type

Let $𝑈$ , $𝑉$ be two types. We can define

𝑈 + 𝑉 ≔ \forall 𝛼, (𝑈 \to 𝛼) \to (𝑉 \to 𝛼) \to 𝛼

and

\begin{aligned} 𝜄_{1} & ≔ 𝜆 𝑢 . Λ 𝛼 . 𝜆 𝑓 . 𝜆 𝑔 . 𝑓 𝑢 \\ 𝜄_{2} & ≔ 𝜆 𝑣 . Λ 𝛼 . 𝜆 𝑓 . 𝜆 𝑔 . 𝑔 𝑣 \end{aligned}

Existential type

Let $𝑈$ be a type, we can define

\exists 𝛼, 𝑈 ≔ \forall 𝛽, (\forall 𝛼, 𝑈 \to 𝛽) \to 𝛽

Meta-theoretic properties

Meta-properties of System F are mainly established through two ways.

Firstly, by reduction to $𝜆$ -calculus: System F introduces type binders and application, but that’s an extremely tame calculus because it

doesn’t interfere with itself: reducing a redex $(Λ 𝛼 . 𝑡) 𝑇$ cannot create an other similar redex
doesn’t interfere with the standard $𝛽$ reduction: reducing a redex as above cannot create a $𝛽$ redex

Hence one can essentially erase all the second order part from a System F term to retrieve important properties of the $𝜆$ -calculus, such as confluence.

Secondly, by crafting adequate logical relations, as with STLC. Note, however, that historically this second part has been considered a hard problem, because System F’s impredicativity breaks the naive way to make logical relations. Indeed, System F’s strong normalisation (which follows directly from being able to define logical relations) need the meta theory to itself have impredicativity, and it cannot be proved, for instance, in MLTT.

Logical relations

For this section, let $𝑛 : ℕ$ be a natural number, which is a parameter of our logical relation construction. $𝑛$ will define the arity of the logical relation. Common values are $𝑛 = 1, 2$ .

We will define, by induction on $𝑇$ , an $𝑛$ -ary relation ${V ⟦ 𝑇 ⟧}_{𝜌}^{𝑛}$ , where $fv (𝑇) \subseteq dom 𝜌$ , and $𝜌$ is a family of $𝑛$ -ary relations on values of System F, used to interpret free variables of $𝑇$ .

\begin{aligned} {V ⟦ 𝛼 ⟧}_{𝜌}^{𝑛} & ≔ 𝜌 (𝛼) \\ {V ⟦ 𝐴 \to 𝐵 ⟧}_{𝜌}^{𝑛} & ≔ {(𝑓_{1}, \dots, 𝑓_{𝑛}) \in {Value}^{𝑛} | \forall (𝑢_{1}, \dots, 𝑢_{𝑛}) \in {V ⟦ 𝐴 ⟧}_{𝜌}^{𝑛}, (𝑓_{1} 𝑢_{1}, \dots, 𝑓_{𝑛} 𝑢_{𝑛}) \in {E ⟦ 𝐵 ⟧}_{𝜌}^{𝑛}} \\ {V ⟦ \forall 𝛼, 𝑇 ⟧}_{𝜌}^{𝑛} & ≔ {(𝑢_{1}, \dots, 𝑢_{𝑛}) \in {Value}^{𝑛} | \forall 𝑅 \subseteq {Value}^{𝑛}, (𝑢_{1}, \dots, 𝑢_{𝑛}) \in {V ⟦ 𝑇 ⟧}_{𝜌 [𝛼 \mapsto 𝑅]}^{𝑛}} \end{aligned}

where

{E ⟦ 𝑇 ⟧}_{𝜌}^{𝑛} ≔ {(𝑡_{1}, \dots, 𝑡_{𝑛}) \in {Term}^{𝑛} | \exists (𝑣_{1}, \dots, 𝑣_{𝑛}) \in {V ⟦ 𝑇 ⟧}_{𝜌}^{𝑛}, \forall 𝑖 \in {1, \dots, 𝑛}, 𝑡_{𝑖} {\underset{𝛽}{⟶}}^{*} 𝑣_{𝑖}}

Note that, crucially, the interpretation of a universal type requires an impredicative universal quantification in the meta-theory.

Theorem Fundamental theorem of logical relations Let $𝑇$ be a type with free variables in $Γ$ , and $𝑢 : Term$ such that $⊢ 𝑢 : 𝑇$ . For any environment $𝜌$ , it holds that

(𝑢, \dots, 𝑢) \in {E ⟦ 𝑇 ⟧}_{𝜌}^{𝑛}

Proof.

By induction on $𝑇$ :

$⊢ 𝑢 : 𝛼$ .

Strong normalisation

Decidability problems

System F is a simple extension of previewSTLC, that is expressive enough to be used as a programming language: for instance, the core type system of OCaml is a subset of System F.

Yet, System F is not used for programming languages in practice, because of a fundamental limitation:

Theorem In System F, type checking and type inference are undecidable.

Type checking

The precise statement of the theorem is: for $𝑡$ a term, and $𝑇$ a type, it is undecidable to know whether

⊢ 𝑡 : 𝑇

Type inference

For $𝑡$ a term, it is undecidable whether there exists a type $𝑇$ such that

⊢ 𝑡 : 𝑇

Mitigation

Undecidability of System F can be mitigated using an intrinsic presentation of its calculus, rather than an extrinsic one.

However, even intrinsic System F is rarely used in practice, because programming languages that abandon decidable type checking (and thus, in the general case, need user annotations) usually go for even more expressive type theories, for instance with higher kinded types (see System F^$𝜔$), or even with full type dependency (see the Calculus of Constructions).