Create a gist now

Instantly share code, notes, and snippets.

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) ->
TyBool
| 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"
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment