Types and Programming Languages

10.2 Terms and Types

The syntax of types is transcribed directly into an ML datatype from the abstract syntax in Figures 8-1 and 9-1.

type ty = TyBool | TyArr of ty * ty

The representation of terms is the same as we used for the untyped lambda-calculus (p. 84), just adding a type annotation to the TmAbs clause.

type term = TmTrue of info | TmFalse of info | TmIf of info * term * term * term | TmVar of info * int * int | TmAbs of info * string * ty * term | TmApp of info * term * term