2010210088 This is an extension from: Implementing type equation generator in OCaml
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
This is a static type checker from a procedure function in OCaml. All the functions are working well except for the 'solve' function part. The error says,
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
What is with that big number beside the / mark? and why is it not working out?
It's easily possible in OCaml to have two types with the same name. To make things less confusing is such cases, the compiler tags a duplicated name with a unique number. Before it started doing this, the error messages were truly confusing: "expected type abc but saw type abc".
One way this can happen is if you have multiple definitions during a run of the OCaml toplevel. If you're working in the toplevel, you might try starting again from scratch.
I just tried your code quickly, and I don't see the error you report. Instead I see an undefined symbol error. This is actually evidence for it being a problem of redefinition in the toplevel.