Chapter 17: An ML Implementation of Subtyping

---

This chapter extends the OCaml implementation of the simply typed lambda-calculus developed in Chapter 10 with the extra mechanisms needed to support subtyping-in particular, a function for checking the subtype relation.

17.1 Syntax

The datatype definitions for types and terms follow the abstract syntax in Figures 15-1 and 15-3.

   type ty =       TyRecord of (string * ty) list     | TyTop     | TyArr of ty * ty   type term =       TmRecord of info * (string * term) list     | TmProj of info * term * string     | TmVar of info * int * int     | TmAbs of info * string * ty * term     | TmApp of info * term * term 

The new constructors, compared with the pure simply typed lambda-calculus, are the type TyTop, the type constructor TyRecord, and the term constructors TmRecord and TmProj. We represent records and their types in the simplest possible way, as a list of field names and associated terms or types.

---