25.5 Typing

< Free Open Study >

The new clauses of the typeof function also follow directly from the typing rules for type abstraction and application and for packing and opening existentials. We show the full definition of typeof, so that the new TmTAbs and TmTApp clauses may be compared with the old clauses for ordinary abstraction and application.

   let rec typeof ctx t =     match t with       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, typeShift (-1) 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")     | TmTAbs(fi,tyX,t2) →         let ctx = addbinding ctx tyX TyVarBind in         let tyT2 = typeof ctx t2 in         TyAll(tyX,tyT2)     | TmTApp(fi,t1,tyT2) →         let tyT1 = typeof ctx t1 in         (match tyT1 with              TyAll(_,tyT12) → typeSubstTop tyT2 tyT12            | _ → error fi "universal type expected")     | TmPack(fi,tyT1,t2,tyT) →         (match tyT with             TySome(tyY,tyT2) →               let tyU = typeof ctx t2 in               let tyU' = typeSubstTop tyT1 tyT2 in               if (=) tyU tyU' then tyT               else error fi "doesn't match declared type"           | - → error fi "existential type expected")     | TmUnpack(fi,tyX,x,t1,t2) →         let tyT1 = typeof ctx t1 in         (match tyT1 with             TySome(tyY,tyT11) →               let ctx' = addbinding ctx tyX TyVarBind in               let ctx" = addbinding ctx' x (VarBind tyT11) in               let tyT2 = typeof ctx" t2 in               typeShift (-2) tyT2           | _ → error fi "existential type expected")

The most interesting new clause is the one for TmUnpack. It involves the following steps. (1) We check the subexpression t₁ and ensure that it has an existential type {$X.T₁₁}. (2) We extend the context Г with a type-variable binding X and a term-variable binding x:T₁₁, and check that t₂ has some type T₂. (3) We shift the indices of free variables in T₂ down by two, so that it makes sense with respect to the original Г. (4) We return the resulting type as the type of the whole let...in... expression.

Clearly, if X occurs free in T₂, then the shift in step (3) will yield a nonsensical type containing free variables with negative indices; typechecking must fail at this point. We can ensure this by redefining typeShiftAbove so that it notices when it is about to construct a type variable with a negative index and signals an error instead of returning nonsense.

   let typeShiftAbove d c tyT =     tymap       (fun c x n → if x>=c then                        if x+d<0 then err "Scoping error!"                        else TyVar(x+d,n+d)                     else TyVar(x,n+d))       c tyT

This check will report a scoping error whenever the type that we calculate for the body t₂ of an existential elimination expression let {X,x}=t₁ in t₂ contains the bound type variable X.

   let {X,x}=({*Nat,0} as {$X,X}) in x; ▸ Error: Scoping error!

< Free Open Study >