Version française
Home     About     Download     Resources     Contact us    

This site is updated infrequently. For up-to-date information, please visit the new OCaml website at

Browse thread
[Caml-list] Polymorphic variants
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
Date: -- (:)
From: John Max Skaller <skaller@o...>
Subject: Re: [Caml-list] How to compare recursive types?
Andreas Rossberg wrote:

>This is highly off-topic, but anyway...
Aw, come on. I'm writing a compiler using Ocaml.
Who else would I ask about a typing problem than people
who regularly use ocaml to implement compilers?
I don't read news, I subscribe to exactly one mailing list (this one)
and I'm neither an academic or a student.

>John Max Skaller wrote:
>>How to compare recursive types?
>>[Or more generally, datya structures ..]
>>Here is my best solution so far.
>>For sake of argment types are either
>>  a) primitive
>>  b) binary product
>>  c) typedef (alias) name
>OK, so you don't have type lambdas (parameterised types).
Not yet no... they're next :-)

> In that case
>any type term can be interpreted as a rational tree. 
.. what's that?

>If you add lambdas (under recursion) things get MUCH harder. Last time I
>looked the problem of equivalence of such types under the equi-recursive
>interpretation you seem to imply (i.e. recursion is `transparent') was
>believed to be undecidable.
In the first instance, the client will have to apply type functions
to create types ..

>>We compare the type expressions structurally and recursively,
>>also passing a counter value:
>>  cmp 99 e1 e2
>>When we reach a typedef name,
>>we decrement the counter argument.
>>If the counter drops
>>to zero, we return true, otherwise we
>>replace the name by the expression it denotes
>>and continue (using the decremented counter).
>So you return true for any infinite (i.e. recursive) type.
No of course not. Obviously, you return false if you reach
two different primitives, or a product and a primitive.

>Seriously, what do you mean by "reaching a typedef name"? In one
Yes. In one of the arguments.

>In both simultanously? What if you reach different names? 
No, and irrelevant given that.

>the second paragraph it seems that you have only considered one special
>case. For the others, if your counter dropped to 0, you had to return
>false for the sake of termination, which renders the algorithm incorrect
>(or incomplete, if you want to put it mildly).
I don't understand: probably because my description of the algorithm
was incomplete, you didn't follow my intent. Real code below.

>>It is "obvious" that for a suitably large counter,
>>this algorithm always terminates and gives the
>>correct result. [The proof would follow from
>>some kind of structural induction]
>I doubt that ;-) In fact it is obvious that your algorithm is incorrect.
>[The proof is a simple counter example like (cmp n t1 t2) where
>t1=prim*t1, t2=prim*t2.]
No, that case is handled easily. Output of code below:
(((fix 1 * float) as 2 * int) as 1 * float)
((fix 1 * int) as 2 * float) as 1
(fix 1 * int) as 1
(fix 1 * int) as 1

type node_t =
  | Prim of string
  | Pair of node_t * node_t
  | Name of string

type env_t = (string * node_t) list

type lnode_t =
  | LPrim of string
  | LPair of lnode_t * lnode_t
  | LBind of int * lnode_t
  | LFix of int

let rec bind' env n labels t = match t with
  | Prim s -> LPrim s
  | Pair (t1, t2) ->
      bind' env n labels t1,
      bind' env n labels t2
  | Name s ->
    if List.mem_assoc s labels
    then LFix (List.assoc s labels)
        bind' env (n+1) ((s,n)::labels) (List.assoc s env)

let bind env t =  bind' env 1 [] t

let rec str t = match t with
  | LPrim s -> s
  | LPair (t1,t2) -> "(" ^ str t1 ^ " * " ^ str t2 ^ ")"
  | LBind (i,t) -> str t ^ " as " ^ string_of_int i
  | LFix i -> "fix " ^ string_of_int i

let rec cmp n lenv renv x y =
  if n = 0 then true
  else match x, y with
  | LPrim s, LPrim r -> s = r
  | LPair (a1,a2), LPair (b1,b2) ->
    cmp n lenv renv a1 b1 &&
    cmp n lenv renv a2 b2
  | LBind (i,a),_ ->
    cmp n ((i,a)::lenv) renv a y
  | _, LBind (i,b) ->
    cmp n lenv ((i,b)::renv) x b
  | LFix i,_ ->
    cmp (n-1) lenv renv (List.assoc i lenv) y
  | _,LFix i ->
    cmp (n-1) lenv renv x (List.assoc i renv)
  |  _ -> false
let env = [
  "x", Pair (Name "y", Prim "int");  (* typedef x = y * int *)
  "y", Pair (Name "x", Prim "float") (* typedef y = x * float *)

(* t1 = x * float, this equals y *)
let t1 = Pair (Name "x", Prim "float")
let t1' = bind env t1
let t2' = bind env (Name "y")

print_endline (str t1');;
print_endline (str t2');;

  match cmp 10 [] [] t1' t2' with
  | true -> "equal"
  | false -> "not equal"

let env = [
  "x", Pair (Name "x", Prim "int");
  "y", Pair (Name "y", Prim "int")

let t1 = bind env (Name "x")
let t2 = bind env (Name "y")

print_endline (str t1);;
print_endline (str t2);;

  match cmp 10 [] [] t1 t2 with
  | true -> "equal"
  | false -> "not equal"

John Max Skaller,
snail:10/1 Toxteth Rd, Glebe, NSW 2037, Australia.
To unsubscribe, mail Archives:
Bug reports: FAQ:
Beginner's list: