Skip to content

Instantly share code, notes, and snippets.



Created Feb 20, 2014
What would you like to do?
Simple Typed Lambda Calculus Typechecking Function in OCaml
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, 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")
| TmTrue(fi) ->
| TmFalse(fi) ->
| 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"
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment