[Camllist] Polymorphic variants
[
Home
]
[ Index:
by date

by threads
]
[ Message by date: previous  next ] [ Message in thread: previous  next ] [ Thread: previous  next ]
[ Message by date: previous  next ] [ Message in thread: previous  next ] [ Thread: previous  next ]
Date:   (:) 
From:  John Max Skaller <skaller@o...> 
Subject:  Re: [Camllist] How to compare recursive types? 
Andreas Rossberg wrote: >This is highly offtopic, 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 equirecursive >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 (n1) lenv renv (List.assoc i lenv) y  _,LFix i > cmp (n1) 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:61296600850  To unsubscribe, mail camllistrequest@inria.fr Archives: http://caml.inria.fr Bug reports: http://caml.inria.fr/bin/camlbugs FAQ: http://caml.inria.fr/FAQ/ Beginner's list: http://groups.yahoo.com/group/ocaml_beginners