用于类型推断的OCaml LET REC类型规则

我目前正在尝试使用静态类型系统实现一个类型分析器,该系统使用OCaml语言实现。

我使用的算法是首先生成类型方程,然后使用统一算法求解这些方程。我已经能够很好地实现代码,除了递归 letrec-exp

这是我的建议 完整代码 :

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
;;

generate_eqns . 它以空类型环境、表达式和初始类型作为参数,调用方式如下: generate_eqns TypeEnv.empty (NUM 3) (new_typevar ()) .

我在执行该命令时遇到问题 LETREC 递归调用。我一直在网上寻找资料,但它们似乎对我的问题没有太大帮助。

编程语言要点(3e)&弗里德曼;魔杖 :

有人能给我一些建议吗?

非常感谢。