Chapter 25: An ML Implementation of System F

---

We now extend our implementation of λ_→ from Chapter 10 to include the universal and existential types from Chapters 23 and 24. Since the rules defining this system are syntax directed (like λ_→ itself, but unlike calculi with subtyping or equi-recursive types), its OCaml realization is quite straightforward. The most interesting extension to the implementation of λ_→ is a representation for types that may include variable bindings (in quantifiers). For these, we use the technique of de Bruijn indices introduced in Chapter 6.

25.1 Nameless Representation of Types

We begin by extending the syntax of types with type variables and universal and existential quantifiers.

   type ty =       TyVar of int * int     | TyArr of ty * ty     | TyAll of string * ty     | TySome of string * ty 

The conventions here are exactly the same as for the representation of terms in §7.1. Type variables consist of two integers: the first specifies the distance to the variable's binder, while the second, as a consistency check, specifies the expected total size of the context. Quantifiers are annotated with a string name for the variable they bind, as a hint for the printing functions.

We next extend contexts to carry bindings for type variables in addition to term variables, by adding a new constructor to the binding type:

   type binding =       NameBind     | VarBind of ty     | TyVarBind 

As in our earlier implementations, the NameBind binder is used only by the parsing and printing functions. The VarBind constructor carries a type, as before. The new TyVarBind constructor carries no additional data value, since (unlike term variables) type variables in this system are not annotated with any additional assumptions. In a system with bounded quantification (Chapter 26) or higher kinds (Chapter 29), we would add an appropriate annotation to each TyVarBind.

---