Re: [Caml-list] How to compare recursive types?

[John Max Skaller <skaller@ozemail.com.au>]

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.
>Interesting...
>
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
>argument? 
>
Yes. In one of the arguments.

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

>From
>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
equal
(fix 1 * int) as 1
(fix 1 * int) as 1
equal
-----------------------------------------------------

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) ->
    LPair
    (
      bind' env n labels t1,
      bind' env n labels t2
    )
  | Name s ->
    if List.mem_assoc s labels
    then LFix (List.assoc s labels)
    else
      LBind
      (
        n,
        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');;

print_endline
(
  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);;

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



-- 
John Max Skaller, mailto:skaller@ozemail.com.au
snail:10/1 Toxteth Rd, Glebe, NSW 2037, Australia.
voice:61-2-9660-0850
-------------------
To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr
Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners