type typ = | TInt | TFun of typ * typ type expr = | EInt of int | EVar of string | ELam of string * typ * expr | EApp of expr * expr type env = (string * typ) list let rec tc a = function | EInt n -> TInt | EVar x -> List.assoc x a | ELam (x, t, e) -> let t' = tc ((x,t)::a) e in TFun (t, t') | EApp (e1, e2) -> let TFun (d,r) = tc a e1 in let t2 = tc a e2 in assert (d = t2); r