Idea: lambda abstraction over type variables, defining functions over types.

---

System F (also known as the polymorphic lambda calculus) = ${\lambda }^{\to }$ + parametric polymorphism.

As an example, the fact that the identity function can have any type of the form $\mathrm{A}\to \mathrm{A}$ would be formalized in System F as the judgment

The upper-case $\Lambda$ is traditionally used to denote type-level functions, as opposed to the lower-case $\lambda$ which is used for value-level functions. (The superscripted $\alpha$ means that the bound x is of type $\alpha$; the expression after the colon is the type of the lambda expression preceding it.)

Environment rules for $\forall$

Kinding rules for $\forall$

System F extends ${\lambda }^{\to }$ with a type-level operator $\forall \alpha ::\ast .$ − that binds a variable $\alpha$ within a particular scope.

There are two new kinding rules:

The $\text{ kind- }\forall$ rule builds universal types $\forall \alpha ::K.A$

The tyvar rule is a type-level analogue of the tvar rule: it allows type variables to appear within type expressions, making it possible to build open types (i.e. types with free variables).

These rules involve a new kind of variable into the language. Type variables are bound by $\forall$ and (as we shall see) by $\Lambda$, and can be used in place of concrete types in expressions.

Typing rules for $\forall$

Since we have a new type constructor $\forall$, we need a new pair of introduction and elimination rules:

The $\forall \text{ -intro }$ rule shows how to build values of type $\forall \alpha ::K.A$ — that is, polymorphic values.

The $\forall \text{ -elim }$ rule shows how to use values of polymorphic type via a second form of application: applying a (suitably-typed) term to a type.

Extensions

Adding Existentials

A value of type $\exists X.T$ is a package with a witness type $T^{\prime }$ for $X$ and a value term $t:[X=>T^{\prime }]T$

It turns out that there is indeed a useful notion of $\exists$ types: just as $\forall$ is used for terms which can be instantiated at any type, $\exists$ can be used to form types for which we have some implementation, but prefer to leave the details abstract.

In fact, it is possible to encode existential types using universal types. But for the time being, will find it more convenient to introduce them directly as an extension to System F.

Kinding rules for $\exists$

Typing rules for $\exists$

The $\exists -intro$ rule shows how to build values of existential type using a new construct, pack.

The $\exists -elim$ rule shows how to use values of existential type using a new construct open

Encoding data types in System F