Tmabs let ctx addbinding ctx varbind let tyt typeof ctx tyarr

	< Free Open Study >

10.2 Terms and Types

< Free Open Study >

	< Free Open Study >

| 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"

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'

	< Free Open Study >