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

sb2.ml

type ty =
| TArrow of ty * ty
| TBool
| TNat

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

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"