Simple Bool with Nat, Let, Records from Types and Programming Languages, simplified based on https://github.com/hsk/simpletapl

sb4.ml

type ty =
| TArrow of ty * ty
| TBool
| TNat
| TRecord of (string * ty) list

type exp =
| EVar of string
| EAbs of string * ty * exp
| EApp of exp * exp
| ETrue
| EFalse
| EIf of exp * exp * exp
| ENat of int
| EAdd of exp * exp
| EIsZero of exp
| ELet of string * exp * exp
| ERecord of (string * exp) list
| EProj of exp * string

let rec typeof env = function
| EVar var -> List.assoc var env
| EAbs(var, t1, e1) -> TArrow(t1, typeof ((var,t1)::env) e1)
| EApp(e1, e2) ->
  (match typeof env e1 with
   | TArrow(t11, t12) where t11 = typeof env e2 -> t12
   | TArrow _ -> failwith "parameter type mismatch"
   | _ -> failwith "non-arrow type in function position")
| ETrue | EFalse -> TBool
| EIf(e1,e2,e3) ->
  if typeof env e1 != TBool
    then failwith "guard of conditional not boolean"
    else
      let t2 = typeof env e2 in
      if typeof env e3 != t2 then failwith "type mismatch in arms of conditional"
      else t2
| ENat _ -> TNat
| EAdd(e1,e2) ->
  if typeof env e1 = TNat && typeof env e2 = TNat then TNat
  else failwith "non-nat argument(s) to add"
| EIsZero e ->
  if typeof env e = TNat then TBool
  else failwith "non-nat argument to iszero"
| ELet(var,e1,e2) -> typeof ((var, typeof env e1)::env) e2
| ERecord les -> TRecord (List.map (fun (l,e)->(l, typeof env e)) les)
| EProj(e,l) -> (match typeof env e with
    | TRecord(lts) -> List.assoc l lts
    | _ -> failwith "record type expected")