functional-programmingocamltype-equivalence

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

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

type typ_eqn = (typ * typ) list

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

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) -> [(ty, TyInt)]@
    [gen_equations (tenv, e1, TyInt)]@
    [gen_equations (tenv, e2, TyInt)]

Hi, I'm trying to implement the type equation generator that I recently learned in class.

But when I tried implementing the ADD expression using the above method, I get an error saying, "This expression has type ('a -> 'b -> typ_eqn) list, but an expression was expected of type (typ * typ) list."

Isn't appending two or more typ_eqn type lists basically the same thing as (typ * typ) list?

edit:

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

I've tried this method too, but this gives me an error message:

"This expression has type (typ * typ) list, but an expression was expected of type (typ * typ)."

Why is this suddenly expecting something different???


Solution

  • In your first version you write [gen_equations (tenv, e1, TyInt)], but gen_equations already returns a list. You might try writing just gen_equations tenv e1 TyInt (note change from uncurried to curried form).

    In your second version, you're using :: to join two lists. But :: is for joining an element to a list. You might try l1 @ l2 @ l3.

    Update

    In both versions, you're calling gen_equations in uncurried form, but it is defined in curried form. Call like this: gen_equations tenv e1 TyInt.