17.3 Typing

---

17.3 Typing

The typechecking function is a straightforward extension of the typeof function from earlier implementations. The main change is the application clause, where we perform a subtype check between the argument type and the type expected by the function. We also add two new clauses for record construction and projection.

   let rec typeof ctx t =     match t with       TmRecord(fi, fields) →         let fieldtys =           List.map (fun (li,ti) → (li, typeof ctx ti)) fields in         TyRecord(fieldtys)     | TmProj(fi, t1, l) →         (match (typeof ctx t1) with             TyRecord(fieldtys) →               (try List.assoc l fieldtys                with Not_found → error fi ("label "∧l∧" not found"))           | _ → error fi "Expected record type")     | 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 subtype tyT2 tyT11 then tyT12               else error fi "parameter type mismatch"           | _ → error fi "arrow type expected") 

The record clauses introduce a few features of OCaml that we have not seen before. In the TmRecord clause, we calculate the list of field names and types fieldtys from the list of names and terms fields by using List.map to apply the function

   fun (li,ti) → (li, typeof ctx ti) 

to each name/term pair in turn. In the TmProj clause, we use List.assoc again to look up the type of the selected field; if it raises Not_found, we raise our own error message (∧ is string concatenation).

17.3.1 Exercise [⋆⋆⋆]

§16.3 showed how adding booleans and conditionals to a language with subtyping required extra support functions for calculating the least upper bounds of a given pair of types. The proof of Proposition 16.3.2 (see page 522) gave mathematical descriptions of the necessary algorithms.

The joinexercise typechecker is an incomplete implementation of the simply typed lambda-calculus with subtyping, records, and conditionals: basic parsing and printing functions are provided, but the clause for TmIf is missing from the typeof function, as is the join function on which it depends. Add booleans and conditionals (and joins and meets) to this implementation.

17.3.2 Exercise [⋆⋆]

Add a minimal Bot type to the rcdsub implementation, following the description in §16.4.

17.3.3 Exercise [⋆⋆ ↛]

If the subtype check in the application rule fails, the error message that our typechecker prints may not be very helpful to the user. We can improve it by including the expected parameter type and the actual argument type in the error message, but even this may be hard to understand. For example, if the expected type is

   {x:{},y:{},z:{},a:{},b:{},c:{},d:{},e:{},f:{},g:{}} 

and the actual type is

   {y:{},z:{},f:{},a:{},x:{},i:{},b:{},e:{},g:{},c:{},h:{}} 

it is not immediately obvious that what's missing from the second type is a d field. Error reporting can be greatly improved by changing the subtype function so that, instead of returning true or false, it either returns a trivial value (the unit value ()) or else raises an exception. Since the exception is raised at the point in the types where something actually failed to match, it can be more precise about what the problem was. Notice that this change doesn't affect the "end-to-end" behavior of the checker: if the subtype checker returns false, the typechecker is always going to raise an exception (by calling error) anyway at that point.

Reimplement the typeof and subtype functions to make all of the error messages as informative as possible.

17.3.4 Exercise [⋆⋆⋆ ↛]

In §15.6 we defined a coercion semantics for a language with records and subtyping using a translation from typing and subtyping derivations into terms of the pure simply typed lambda-calculus. Implement these transformations by modifying the subtype function presented above so that it constructs and returns a coercion function represented as a term), and similarly modifying the typeof function so that it returns both a type and a translated term. The translated term (rather than the original input term) should then be evaluated, and the result printed as usual.

---