OCaml 静态类型检查器的错误

Question

2010210088 这是来自的扩展：

type exp = 
  | CONST of int
  | VAR of var
  | ADD of exp * exp
  | SUB of exp * exp
  | ISZERO of exp
  | IF of exp * exp * exp
  | LET of var * exp * exp
  | PROC of var * exp
  | CALL of exp * exp
and var = string

(* raise this exception when the program is determined to be ill-typed *)
exception TypeError

(* type *)
type typ = TyInt | TyBool | TyFun of typ * typ | TyVar of tyvar
and tyvar = string

(* type equations are represented by a list of "equalities" (ty1 = ty2)  *)
type typ_eqn = (typ * typ) list

(* generate a fresh type variable *)
let tyvar_num = ref 0
let fresh_tyvar () = (tyvar_num := !tyvar_num + 1; (TyVar ("t" ^ string_of_int !tyvar_num)))

(* type environment : var -> type *)
module TEnv = 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

(* substitution *)
module Subst = struct
  type t = (tyvar * typ) list
  let empty = []
  let find x subst = List.assoc x subst

  (* walk through the type, replacing each type variable by its binding in the substitution *)
  let rec apply : typ -> t -> typ
  =fun typ subst ->
    match typ with
    | TyInt -> TyInt
    | TyBool -> TyBool 
    | TyFun (t1,t2) -> TyFun (apply t1 subst, apply t2 subst)
    | TyVar x -> 
      try find x subst
      with _ -> typ

  (* add a binding (tv,ty) to the subsutition and propagate the information *)
  let extend tv ty subst = 
    (tv,ty) :: (List.map (fun (x,t) -> (x, apply t [(tv,ty)])) subst)
end

let rec gen_equations : TEnv.t -> exp -> typ -> typ_eqn 
=fun tenv e ty -> match e with
| CONST n -> [(ty, TyInt)]
| VAR x -> [(ty, TEnv.find tenv x)]
| ADD (e1,e2) ->
    let l1 = [(ty, TyInt)] in
    let l2 = gen_equations tenv e1 TyInt in
    let l3 = gen_equations tenv e2 TyInt in
    l1@l2@l3
| SUB (e1,e2) ->
    let l1 = [(ty, TyInt)] in
    let l2 = gen_equations tenv e1 TyInt in
    let l3 = gen_equations tenv e2 TyInt in
    l1@l2@l3
| ISZERO e ->
    let l1 = [(ty, TyBool)] in
    let l2 = gen_equations tenv e TyInt in
    l1@l2
| IF (e1,e2,e3) ->
    let l1 = gen_equations tenv e1 TyBool in
    let l2 = gen_equations tenv e2 ty in
    let l3 = gen_equations tenv e3 ty in
    l1@l2@l3
| LET (x,e1,e2) ->
    let t = fresh_tyvar () in
    let l1 = gen_equations tenv e1 t in
    let l2 = gen_equations (TEnv.extend (x,t) tenv) e2 ty in
    l1@l2
| PROC (x,e) ->
    let t1 = fresh_tyvar () in
    let t2 = fresh_tyvar () in
    let l1 = [(ty, TyFun (t1,t2))] in
    let l2 = gen_equations (TEnv.extend (x,t1) tenv) e t2 in
    l1@l2
| CALL (e1,e2) ->
    let t = fresh_tyvar () in
    let l1 = gen_equations tenv e1 (TyFun (t,ty)) in
    let l2 = gen_equations tenv e2 t in
    l1@l2
| _ -> raise TypeError

(* this is where the error comes up *)
let solve : typ_eqn -> Subst.t
=fun eqn -> unifyall eqn Subst.empty

let rec unify : typ -> typ -> Subst.t -> Subst.t
=fun t1 t2 s -> match (t1,t2) with
| (TyInt,TyInt) -> s
| (TyBool,TyBool) -> s
| (t,TyVar a) -> unify (TyVar a) t s
| (TyVar t1,t2) -> Subst.extend t1 t2 s
| (TyFun (t1,t2), TyFun (t1',t2')) ->
    let s' = unify t1 t1' s in
    let t1'' = Subst.apply t2 s' in
    let t2'' = Subst.apply t2' s' in
    unify t1'' t2'' s'

let rec unifyall : typ_eqn -> Subst.t -> Subst.t
=fun eqn s -> match eqn with
| [] -> s
| (t1,t2)::u ->
    let s' = unify (Subst.apply t1 s) (Subst.apply t2 s) s in
    unifyall u s'

let typeof : exp -> typ 
=fun exp -> 
  let new_tv = fresh_tyvar () in
  let eqns = gen_equations TEnv.empty exp new_tv in
  let subst = solve eqns in
  let ty = Subst.apply new_tv subst in
    ty

这是来自 OCaml 过程函数的静态类型检查器。除了 'solve' 功能部分外，所有功能都运行良好。错误说，

Error: This expression has type typ_eqn/3404 = (typ/3398 * typ/3398) list but an expresson was expected of type typ_eqn/3179 = (typ/3173 * typ/3173) list Type typ/3398 is not compatible with type typ/3173

/ 旁边那个大数字是什么？为什么没有效果？

Answer 1

在 OCaml 中很容易有两个同名的类型。为了让事情不那么混乱，编译器用一个唯一的数字标记一个重复的名字。在开始执行此操作之前，错误消息确实令人困惑："expected type abc but saw type abc".

发生这种情况的一种方式是，如果您在 OCaml 顶层的运行期间有多个定义。如果您在顶层工作，您可以尝试从头开始。

我刚刚快速尝试了您的代码，但没有看到您报告的错误。相反，我看到一个未定义的符号错误。这实际上是证据因为它是顶层重新定义的问题。

OCaml 静态类型检查器的错误

errors on static type checker for OCaml

ocaml

typechecking