OCaml LET REC typing rule for type inference

Question

I'm currently trying to implement a type analyzer using a static type system, implemented using the OCaml language.

The algorithm that I'm using is to first generate type equations, then solve these equations using the unification algorithm. I've been able to implement the code fairly well, except for a recursive letrec-exp binding type.

Here's the full code:

type program = exp
and exp = 
  | NUM of int
  | VAR of var
  | SUM of exp * exp
  | DIFF of exp * exp
  | MULT of exp * exp
  | DIV of exp * exp
  | ZERO of exp
  | IF of exp * exp * exp
  | LET of var * exp * exp
  | LETREC of var * var * exp * exp
  | FUNC of var * exp
  | CALL of exp * exp
and var = string
;;

type typ = TypeInt | TypeBool | TypeFun of typ * typ | TypeVar of tyvar
and tyvar = string
;;
type type_equation = (typ * typ) list;;

module TypeEnv = struct
  type t = var -> typ

  let empty
  = fun _ -> raise (Failure "Type Env is empty")

  let extend (x, t) tenv
  = fun y -> if x = y then t else (tenv y)

  let find tenv x = tenv x
end
;;

let typevar_num = ref 0;;

let new_typevar () = (typevar_num := !typevar_num + 1; (TypeVar ("t" ^ string_of_int !typevar_num)));;

let rec generate_eqns : TypeEnv.t -> exp -> typ -> type_equation 
= fun tenv e ty ->
  match e with
  | NUM n -> [(ty, TypeInt)]
  | VAR x -> [(ty, TypeEnv.find tenv x)]
  | SUM (e1, e2) -> let eq1 = [(ty, TypeInt)] in
                      let eq2 = generate_eqns tenv e1 TypeInt in
                        let eq3 = generate_eqns tenv e2 TypeInt in
                          eq1 @ eq2 @ eq3
  | DIFF (e1, e2) -> let eq1 = [(ty, TypeInt)] in
                      let eq2 = generate_eqns tenv e1 TypeInt in
                        let eq3 = generate_eqns tenv e2 TypeInt in
                          eq1 @ eq2 @ eq3
  | DIV (e1, e2) -> let eq1 = [(ty, TypeInt)] in
                      let eq2 = generate_eqns tenv e1 TypeInt in
                        let eq3 = generate_eqns tenv e2 TypeInt in
                          eq1 @ eq2 @ eq3
  | MULT (e1, e2) -> let eq1 = [(ty, TypeInt)] in
                      let eq2 = generate_eqns tenv e1 TypeInt in
                        let eq3 = generate_eqns tenv e2 TypeInt in
                          eq1 @ eq2 @ eq3
  | ISZERO e -> let eq1 = [(ty, TypeBool)] in
                  let eq2 = generate_eqns tenv e TypeInt in
                    eq1 @ eq2
  | IF (e1, e2, e3) -> let eq1 = generate_eqns tenv e1 TypeBool in
                         let eq2 = generate_eqns tenv e2 ty in
                           let eq3 = gen_equations tenv e3 ty in
                             eq1 @ eq2 @ eq3
  | LET (x, e1, e2) -> let t1 = new_typevar () in
                         let eq1 = generate_eqns tenv e1 t1 in
                           let eq2 = generate_eqns (TypeEnv.extend (x, t1) tenv) e2 ty in
                             eq1 @ eq2
  | LETREC (f, x, e1, e2) -> (* let t1 = new_typevar () in
                           let new_env = TypeEnv.extend (x, t1) tenv in
                             let eq1 = generate_eqns new_env f *)
  | FUNC (x, e) -> let t1 = new_typevar () in
                     let t2 = new_typevar () in
                       let eq1 = [(ty, TypeFun (t1, t2))] in
                         let eq2 = generate_eqns (TypeEnv.extend (x, t1) tenv) e t2 in
                           eq1 @ eq2
  | CALL (e1, e2) -> let t1 = new_typevar () in
                       let eq1 = generate_eqns tenv e1 (TypeFun (t1, ty)) in
                         let eq2 = generate_eqns tenv e2 t1 in
                           eq1 @ eq2
;;

The main function that performs the type equation generating is generate_eqns. It takes an empty type environment, expression, and initial type as arguments and is called like this: generate_eqns TypeEnv.empty (NUM 3) (new_typevar ()).

I'm having trouble implementing the LETREC recursive call. I've been trying to look for material online but they don't seem to be too helpful to my problem.

In particular, I've been trying to analyze this typing rule from Essentials of Progrmaming Languages (3e) - Friedman & Wand:

Would anybody be kind enough to give me some pointers or advice?

Thank you.

Answer 1

So I skimmed through your code, this untested, etc. But at first glance I suppose it should be something along these lines,

  | LETREC (f, x, e1, e2) ->
     let tx  = new_typevar ()    in (** type of x   **)
     let tfx = new_typevar ()    in (** type of f x **)
     let tf  = TypeFun (tx, tfx) in (** type of f   **)
     let tenvf  = TypeEnv.extend (f, tf) tenv  in (** f in env **) 
     let tenvxf = TypeEnv.extend (x, tx) tenvf in (** x and f in env **) 
     let eq1 = generate_eqns tenvxf e1 tfx in (** type e1 = type (f x) **)
     let eq2 = generate_eqns tenvf  e2 ty  in (** type e2 = typ **)
         eq1 @ eq2