10.3 Typechecking

< Free Open Study >

The typechecking function typeof can be viewed as a direct translation of the typing rules for λ_→ (Figures 8-1 and 9-1), or, more accurately, as a transcription of the inversion lemma (9.3.1). The second view is more accurate because it is the inversion lemma that tells us, for every syntactic form, exactly what conditions must hold in order for a term of this form to be well typed. The typing rules tell us that terms of certain forms are well typed under certain conditions, but by looking at an individual typing rule, we can never conclude that some term is not well typed, since it is always possible that another rule could be used to type this term. (At the moment, this may appear to be a difference without a distinction, since the inversion lemma follows so directly from the typing rules. The difference becomes important, though, in later systems where proving the inversion lemma requires more work than in λ_→.)

   let rec typeof ctx t =     match t with       TmTrue(fi) →         TyBool     | TmFalse(fi) →         TyBool     | TmIf(fi,t1,t2,t3) →        if (=) (typeof ctx t1) TyBool then          let tyT2 = typeof ctx t2 in          if (=) tyT2 (typeof ctx t3) then tyT2          else error fi "arms of conditional have different types"        else error fi "guard of conditional not a boolean"     | TmVar(fi,i,_) → getTypeFromContext fi ctx i     | TmAbs(fi,x,tyT1,t2) →         let ctx' = addbinding ctx x (VarBind(tyT1)) in         let tyT2 = typeof ctx' t2 in         TyArr(tyT1, tyT2)     | TmApp(fi,t1,t2) →         let tyT1 = typeof ctx t1 in         let tyT2 = typeof ctx t2 in         (match tyT1 with             TyArr(tyT11,tyT12) →               if (=) tyT2 tyT11 then tyT12               else error fi "parameter type mismatch"           | _ → error fi "arrow type expected")

A couple of details of the OCaml language are worth mentioning here. First, the OCaml equality operator = is written in parentheses because we are using it in prefix position, rather than its normal infix position, to facilitate comparison with later versions of typeof where the operation of comparing types will need to be something more refined than simple equality. Second, the equality operator computes a structural equality on compound values, not a pointer equality. That is, the expression

   let t  = TmApp(t1,t2) in   let t' = TmApp(t1,t2) in   (=) t t'

is guaranteed to yield true, even though the two instances of TmApp bound to t and t′ are allocated at different times and live at different addresses in memory.

< Free Open Study >