| < 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 t1 and ensure that it has an existential type {$X.T11}. (2) We extend the context Г with a type-variable binding X and a term-variable binding x:T11, and check that t2 has some type T2. (3) We shift the indices of free variables in T2 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 T2, 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 t2 of an existential elimination expression let {X,x}=t1 in t2 contains the bound type variable X.
let {X,x}=({*Nat,0} as {$X,X}) in x; ▸ Error: Scoping error!
| < Free Open Study > |
|