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

sb8.ml

type ty =
| TArrow of ty * ty
| TBool
| TNat
| TRecord of (string * ty) list
| TVariant of (string * ty) list
| TUnit
| TRef of ty
| TBottom

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
| ETag of string * exp * ty
| ECase of exp * (string * (string * exp)) list
| EFix of exp
| ERef of exp
| EDeref of exp
| EAssign of exp * exp
| EError
| ETry of exp * exp

let rec is_subtype t1 t2 = match t1, t2 with
  | _, _ when t1 = t2 -> true
  | TBottom, _ -> true
  | TArrow(targ1,tret1), TArrow(targ2,tret2) ->
    targ1 = targ2 && is_subtype tret1 tret2
  | TRecord lts1, TRecord lts2 ->
    List.map fst lts1 = List.map fst lts2 && 
    List.for_all2 is_subtype (List.map snd lts1) (List.map snd lts2)
  | _ -> false

let rec eq_upto_subtype t1 t2 = match t1, t2 with
  | _, _ when t1 = t2 -> true
  | TBottom, _ | _, TBottom -> true
  | TArrow(targ1,tret1), TArrow(targ2,tret2) ->
    targ1 = targ2 && eq_upto_subtype tret1 tret2
  | TRecord lts1, TRecord lts2 ->
    List.map fst lts1 = List.map fst lts2 && 
    List.for_all2 eq_upto_subtype (List.map snd lts1) (List.map snd lts2)
  | _ -> false

let rec join t1 t2 = match t1, t2 with
| _, _ when is_subtype t1 t2 -> t2
| _, _ when is_subtype t2 t1 -> t1
| TArrow(targ1,tret1), TArrow(targ2,tret2) ->
  if targ1 = targ2
    then TArrow(targ1, join tret1 tret2)
    else failwith "type mismatch in function params"
| TRecord lts1, TRecord lts2 ->
  let labels = List.map fst lts1 in
  if labels = List.map fst lts2
    then TRecord (List.combine labels  (List.map2 join (List.map snd lts1) (List.map snd lts2)))
    else failwith "label mismatch in record"
| _ -> failwith "unable to join types"

let rec contains_bottom = function
| TBottom -> true
| TArrow(_,t) -> contains_bottom t 
| TRecord lts -> List.exists contains_bottom (List.map snd lts)
| _ -> false

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) when is_subtype (typeof env e2) t11 -> t12
   | TArrow _ -> failwith "parameter type mismatch"
   | TBottom -> TBottom
   | _ -> failwith "non-arrow type in function position")
| ETrue | EFalse -> TBool
| EIf(e1,e2,e3) ->
  if not (is_subtype (typeof env e1) TBool)
    then failwith "guard of conditional not boolean"
    else join (typeof env e2) (typeof env e3)
| ENat _ -> TNat
| EAdd(e1,e2) ->
  if is_subtype (typeof env e1) TNat && is_subtype (typeof env e2) TNat then TNat
  else failwith "non-nat argument(s) to add"
| EIsZero e ->
  if is_subtype (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 ->
  let lts = (List.map (fun (l,e)->(l, typeof env e)) les) in
  if List.exists (fun (_,t) -> t = TBottom) lts then TBottom
  else TRecord lts
| EProj(e,l) -> (match typeof env e with
    | TRecord(lts) -> List.assoc l lts
    | TBottom -> TBottom
    | _ -> failwith "record type expected")
| ETag(l,e,t) -> (match t with
    | TVariant lts -> 
      let t' = List.assoc l lts in
      if is_subtype (typeof env e) t' then t
      else failwith "field does not have expected type"
    | _ -> failwith "annotation is not a variant type")
| ECase(e, cases) -> (match typeof env e with
    | TVariant lts ->
      let labels = List.map fst cases in
      let is_label_in_type l = List.mem_assoc l lts in
      if not (List.for_all is_label_in_type labels) then failwith "label mismatch between case and type";
      let typeof_case_exp (l,(var,exp)) = typeof ((var,List.assoc l lts)::env) exp in
      let ts = List.map typeof_case_exp cases in
      List.fold_left join TBottom ts
    | TBottom -> TBottom
    | _ -> failwith "variant type expected")
| EFix e -> (match typeof env e with
    | TArrow(t11,t12) when is_subtype t12 t11 -> t11
    | TArrow _ -> failwith "type mismatch between parameter and return of fix"
    | TBottom -> TBottom
    | _ -> failwith "arrow type expected")
| ERef e ->
  let t = typeof env e in
  if contains_bottom t then failwith "type containing bottom passed to ref"
  else TRef t
| EDeref e -> (match typeof env e with
    | TRef t -> t
    | TBottom -> TBottom
    | _ -> failwith "non-ref passed to deref")
| EAssign(e1,e2) -> (match typeof env e1 with
    | TRef t when is_subtype (typeof env e2) t -> TUnit 
    | TRef _ -> failwith "type mismatch between ref and value"
    | TBottom -> ignore @@ typeof env e2; TUnit
    | _ -> failwith "ref type expected")
| EError -> TBottom
| ETry(e1, e2) -> join (typeof env e1) (typeof env e2)