* Type abstraction and (polymorphic) equality @ 2005-06-29 0:31 Christophe TROESTLER 2005-06-29 9:12 ` [Caml-list] " Jon Harrop ` (4 more replies) 0 siblings, 5 replies; 22+ messages in thread From: Christophe TROESTLER @ 2005-06-29 0:31 UTC (permalink / raw) To: O'Caml Mailing List [-- Attachment #1: Type: Text/Plain, Size: 2898 bytes --] Hi, I'd like here to present a problem that I think is fairly common (and likely probably discussed) to have suggestions about what is the best way to deal with it. Let me start with a little story that happened to me recently. Suppose one has a module A declaring an abstract type t and some functions. You are happy with the interface of A and have a working implementation so you go on and write programs using A. Later on, you realize that you could improve A implementation by attaching additional information to each variable of type t (this does not change the interface of A). Then all of a sudden, your programs start to die with Out_of_memory exceptions... The problem was that the attached information (an additional field in a record) was a cyclic data structure. From there on, all equality tests became deadly! (I would have preferred to have the exception Invalid_argument "equal: abstract value".) What made matters worse is that the compiler could not help me to find the locations of such problems -- which can be hidden e.g. in List.mem. Not a nice job to do... One may argue that its my fault: I should have declared from the start a function val eq : t -> t -> bool While that would have solved some of the problems I have, it would have introduced new ones. In particular, some functions relying on equality couldn't be used anymore (but, again, without the compiler helping to fund them). An example is List.mem. Of course, there is List.exists to achieve the same goal but maybe one uses a library declaring internally type 'a s = X | Y of 'a and using equality on values of type ['a s] (here the default structural equality is arguably what we want). You may not even be aware that the library does so if you did not write it. However, for values of type [t s] on needs a special equality... which in practice precludes the use of this library! Here one sees that the problems with equality stand in the way of abstraction and code reusability. Now the questions are: * Is there a solution in the current state of OCaml? (I'll be glad if there is.) * If the first answer is "no", is there a medium term perspective to bring a solution to this problem? I can see two: - one allows to redefine equality for new types, say with a syntax like type t = ... with compare x y = ... as this is already done for blocks with custom tags. (BTW, why aren't Big_int such blocks with an appropriate compare?) - One introduces the same capability of providing a special equality (comparison) for certain types but, during compilation, "expand" functions till the type for "=" is given by known functions (something like a "generic" equality). I guess however that that may cause problems with separate compilation... I'll be glad to hear similar experiences and comments about the above ideas. Regards, ChriS [-- Attachment #2: a.mli --] [-- Type: Text/Plain, Size: 27 bytes --] type t val x : t val y : t [-- Attachment #3: b.ml --] [-- Type: Text/Plain, Size: 44 bytes --] let () = Printf.printf "%b\n" (A.x = A.y) [-- Attachment #4: a.ml --] [-- Type: Text/Plain, Size: 133 bytes --] type t = { a : int; b : t * t; (* extra info for optimization *) } let rec x = { a=1; b = (x, y) } and y = { a=1; b = (y,x) } ^ permalink raw reply [flat|nested] 22+ messages in thread
* Re: [Caml-list] Type abstraction and (polymorphic) equality 2005-06-29 0:31 Type abstraction and (polymorphic) equality Christophe TROESTLER @ 2005-06-29 9:12 ` Jon Harrop 2005-06-29 10:06 ` Andreas Rossberg ` (3 more replies) 2005-06-29 9:45 ` Jean-Christophe Filliatre ` (3 subsequent siblings) 4 siblings, 4 replies; 22+ messages in thread From: Jon Harrop @ 2005-06-29 9:12 UTC (permalink / raw) To: caml-list On Wednesday 29 June 2005 01:31, Christophe TROESTLER wrote: > One may argue that its my fault: I should have declared from the start > a function > > val eq : t -> t -> bool Yes, if you're doing anything which you think may be extended later then I think it is a good idea to try to discipline yourself in this way (don't use built-in polymorphic equality). > * Is there a solution in the current state of OCaml? (I'll be glad if > there is.) I do not believe so. IIRC, SML has equality types to help with this problem. > * If the first answer is "no", is there a medium term perspective to > bring a solution to this problem? I can see two: > > - one allows to redefine equality for new types, say with a syntax > like > > type t = ... with compare x y = ... > > as this is already done for blocks with custom tags. (BTW, why > aren't Big_int such blocks with an appropriate compare?) That looks lovely. Apparently a similar facility is available in Haskell. However, there are disadvantages. Unless you're doing whole-program compilation, you'll need to carry a compare function with every datum. That's a huge performance cost and it probably isn't too easy to optimise it away. > - One introduces the same capability of providing a special equality > (comparison) for certain types but, during compilation, "expand" > functions till the type for "=" is given by known functions > (something like a "generic" equality). I guess however that that > may cause problems with separate compilation... Yes. It seems that this kind of thing is best done by a MLton-like compiler. If this is a trade-off then I prefer OCaml's current position - MLton is an order of magnitude slower to compile small programs, no dynamic code loading, no marshalling etc. > I'll be glad to hear similar experiences and comments about the above > ideas. I had a similar problem when I extended an AST type to include lazily evaluated information. I suddenly got comparisons raising "function type" exceptions everywhere. The best solution recommended to me was to temporarily replace "=" with my own monomorphic version. That's hardly elegant and only works well if you've only used "=" on the one type that you're interested in. I was convinced that there must be a simpler solution to this problem, using a static checker. However, the more I looked into my seemingly great idea, the harder it got... :-) -- Dr Jon D Harrop, Flying Frog Consultancy Ltd. Technical Presentation Software http://www.ffconsultancy.com/products/presenta ^ permalink raw reply [flat|nested] 22+ messages in thread
* Re: [Caml-list] Type abstraction and (polymorphic) equality 2005-06-29 9:12 ` [Caml-list] " Jon Harrop @ 2005-06-29 10:06 ` Andreas Rossberg 2005-06-29 13:32 ` Christophe TROESTLER ` (2 subsequent siblings) 3 siblings, 0 replies; 22+ messages in thread From: Andreas Rossberg @ 2005-06-29 10:06 UTC (permalink / raw) To: caml-list Jon Harrop wrote: > > I do not believe so. IIRC, SML has equality types to help with this problem. Equality types only provide half a solution (preventing accidental (ab)use of polymorphic equality). Solving the whole problem (enabling user-defined equality on user-defined types) requires something more general, e.g. type classes. - Andreas -- Andreas Rossberg, rossberg@ps.uni-sb.de Let's get rid of those possible thingies! -- TB ^ permalink raw reply [flat|nested] 22+ messages in thread
* Re: [Caml-list] Type abstraction and (polymorphic) equality 2005-06-29 9:12 ` [Caml-list] " Jon Harrop 2005-06-29 10:06 ` Andreas Rossberg @ 2005-06-29 13:32 ` Christophe TROESTLER 2005-06-29 23:39 ` brogoff 2005-06-29 20:27 ` Christophe TROESTLER 2005-06-29 20:37 ` John Skaller 3 siblings, 1 reply; 22+ messages in thread From: Christophe TROESTLER @ 2005-06-29 13:32 UTC (permalink / raw) To: jon; +Cc: caml-list On Wed, 29 Jun 2005, Jon Harrop <jon@ffconsultancy.com> wrote: > > > - One introduces the same capability of providing a special equality > > (comparison) for certain types but, during compilation, "expand" > > functions till the type for "=" is given by known functions > > (something like a "generic" equality). I guess however that that > > may cause problems with separate compilation... > > Yes. It seems that this kind of thing is best done by a MLton-like > compiler. If this is a trade-off then I prefer OCaml's current > position - MLton is an order of magnitude slower to compile small > programs, no dynamic code loading, no marshalling etc. Well I was more thinking of overloading equality in a GCaml manner (http://www.yl.is.s.u-tokyo.ac.jp/~furuse/gcaml/) which offers you more, not less. However, I do not know how much GCaml actually tries to reduce the performance hit by compiling monomorphically whenever possible... Cheers, ChriS ^ permalink raw reply [flat|nested] 22+ messages in thread
* Re: [Caml-list] Type abstraction and (polymorphic) equality 2005-06-29 13:32 ` Christophe TROESTLER @ 2005-06-29 23:39 ` brogoff 2005-06-30 7:46 ` Christophe Raffalli 0 siblings, 1 reply; 22+ messages in thread From: brogoff @ 2005-06-29 23:39 UTC (permalink / raw) To: Christophe TROESTLER; +Cc: caml-list On Wed, 29 Jun 2005, Christophe TROESTLER wrote: > Well I was more thinking of overloading equality in a GCaml manner > (http://www.yl.is.s.u-tokyo.ac.jp/~furuse/gcaml/) which offers you > more, not less. That's one way to go about it, though GCaml still provides polymorphic equality, so if you write your generic function so that there's a catch all 'a-> 'a -> bool branch which uses that equality, the bug/flaw can still bite you. It would be best if GCaml (and OCaml?) do away with polymorphic equality, or at least give it some ugly name to prevent it's accidental misuse. Type classes would be another option, but people don't like the redundancy with the ML module system. Maybe some future ML will be based on type classes and a simple non-parameterized module system, so However, I do not know how much GCaml actually tries > to reduce the performance hit by compiling monomorphically whenever > possible... There's not even a native code compiler yet, so I wouldn't worry to much about it just now. -- Brian ^ permalink raw reply [flat|nested] 22+ messages in thread
* Re: [Caml-list] Type abstraction and (polymorphic) equality 2005-06-29 23:39 ` brogoff @ 2005-06-30 7:46 ` Christophe Raffalli 0 siblings, 0 replies; 22+ messages in thread From: Christophe Raffalli @ 2005-06-30 7:46 UTC (permalink / raw) To: brogoff; +Cc: Christophe TROESTLER, caml-list [-- Attachment #1: Type: text/plain, Size: 820 bytes --] A trick (dirty ?) which would not slow down much performance of the polymorphic equal would be to detect cyclic structure using the bit used by the GC (the equallity will not trigger GC ?), and when you detect a cycle, you either raise an exception or use physical equality depending on the value of a global variable. -- Christophe Raffalli Université de Savoie Batiment Le Chablais, bureau 21 73376 Le Bourget-du-Lac Cedex tél: (33) 4 79 75 81 03 fax: (33) 4 79 75 87 42 mail: Christophe.Raffalli@univ-savoie.fr www: http://www.lama.univ-savoie.fr/~RAFFALLI --------------------------------------------- IMPORTANT: this mail is signed using PGP/MIME At least Enigmail/Mozilla, mutt or evolution can check this signature. The public key is stored on www.keyserver.net --------------------------------------------- [-- Attachment #2: OpenPGP digital signature --] [-- Type: application/pgp-signature, Size: 252 bytes --] ^ permalink raw reply [flat|nested] 22+ messages in thread
* Re: [Caml-list] Type abstraction and (polymorphic) equality 2005-06-29 9:12 ` [Caml-list] " Jon Harrop 2005-06-29 10:06 ` Andreas Rossberg 2005-06-29 13:32 ` Christophe TROESTLER @ 2005-06-29 20:27 ` Christophe TROESTLER 2005-06-29 20:37 ` John Skaller 3 siblings, 0 replies; 22+ messages in thread From: Christophe TROESTLER @ 2005-06-29 20:27 UTC (permalink / raw) To: O'Caml Mailing List On Wed, 29 Jun 2005, Jon Harrop <jon@ffconsultancy.com> wrote: > > On Wednesday 29 June 2005 01:31, Christophe TROESTLER wrote: > > type t = ... with compare x y = ... > > That looks lovely. Apparently a similar facility is available in > Haskell. However, there are disadvantages. Unless you're doing > whole-program compilation, you'll need to carry a compare function > with every datum. That's a huge performance cost and it probably > isn't too easy to optimise it away. Does it need to be the case? One certainly needs to tag the types with special equality functions but these tag could be generated for each program (so as to reduce the necessary tag space), couldn't they? Then, again for each program, one would provide a special tailored equality function instead of "compare_val". Does this make sense? Cheers, ChriS ^ permalink raw reply [flat|nested] 22+ messages in thread
* Re: [Caml-list] Type abstraction and (polymorphic) equality 2005-06-29 9:12 ` [Caml-list] " Jon Harrop ` (2 preceding siblings ...) 2005-06-29 20:27 ` Christophe TROESTLER @ 2005-06-29 20:37 ` John Skaller 2005-06-30 9:53 ` Andreas Rossberg 3 siblings, 1 reply; 22+ messages in thread From: John Skaller @ 2005-06-29 20:37 UTC (permalink / raw) To: Jon Harrop; +Cc: caml-list [-- Attachment #1: Type: text/plain, Size: 4607 bytes --] On Wed, 2005-06-29 at 10:12 +0100, Jon Harrop wrote: > On Wednesday 29 June 2005 01:31, Christophe TROESTLER wrote: > > - one allows to redefine equality for new types, say with a syntax > > like > > > > type t = ... with compare x y = ... > > > > as this is already done for blocks with custom tags. (BTW, why > > aren't Big_int such blocks with an appropriate compare?) Executive Summary: I guess no wart free solution can exist. I have been considering these issues for some time for Felix, I don't see any easy solution. Felix is an ML like language which supports overloading, and whole program analysis with strictly parametric but extensional polymorphism. At present primitives can be compared like this: type int = "int"; // maps to the C representation fun eq: int * int -> bool = "$1==$2"; // C equality val a: int = 1; val b: int = 2; val e: bool = a == b; // parser maps to eq(a,b) By overloading, we have 1L == 2L // longs working too. Now consider a comparison for this type: int * long For any product of comparable types, we can use the lexicographical comparison algorithm to generate a comparator. However, if we decide to do that automatically for all algebraic types, then the user cannot also provide a comparator. Even if it were possible it is undesirable because it would be extremely fragile and very hard to know which function was called by examining the code -- a general problem with overloading, but far worse when some overloads are automatically synthesised. For generative types, we can allow something like: struct X = { x:int; y:int; } with eq: auto; where the user may supply the comparator, and if they choose to may supply the generated one. If they do not supply the comparator, one is not generated. This can't work for non-generative products: there is no place to declare the comparator. There is another problem. The user may be rather confused in this case, as is demonstrated by the equivalent problem in Ocaml with floating comparisons: fun eq: int * int -> bool; fun eq: long * long -> bool; fun isequal[t] (a:t, b:t) => a == b; // WOOPS Here there is a compiler error: there is no function named 'eq' with a signature for which t * t is a specialisation. You would have to write: fun isequal[t] (a:t, b:t, eq: t * t -> bool) => a == b; explicitly passing the comparator. Unlike C++, Felix does not permit 'two phase lookup', lookup and overload resolution are done before instantiation to ensure polymorphism is fully parametric (as in Ocaml). The user is likely to annoyed they have to write: isequal (1,2,eq of (int * int)) to solve this. Macros may help in cases that work: macro genisequal (a,b) { isequal(a,b,eq of (typeof(a) * typeof(b))); } genisequal(1,2) but I am quite dubious that, in the case of a failure, the user would have much hope of unravelling the error messages (and in Felix, implicit macro invocation is not available anyhow). The *advantage* of requiring the equality to be explicitly passed is seen in cases like: typedef complex = double * double; // double is C floating type where a lexicographical comparison is not desired. Apart from the extra verbiage, the problem is as above: although you have to pass the desired comparison to a polymorphic routine, you will get a completely different comparator in simple usage like val a: complex = 1.0,2.0; if a == a then .. //woops, lexicographical compare and you cannot fix this with an overload with 'the right' comparator -- it would, should, and must conflict with an implicitly autogenerated one. Note in Felix you can in fact model this by cheating: fun eq[t]: t * t -> bool = "$1 == $2"; // 'polymorphic' comparison module A { fun eq:int * int -> bool; ... 1 == 2 .. //uses A::eq } 1 == 2 // uses global eq but we simply cannot have implicitly generated functions being so context sensitive. Note that in the example we are cheating: only by falling back to the broken C++ system can we actually define a polymophic equality operator .. of course we will get C++ compile time errors instead of Felix compile time errors: at least the error detection isn't delayed until run time. My conclusion is: in Ocaml, the runtime failure of polymorphic comparisons when encountering abstract types (or cyclic data structures) is a wart, but there is no wart free solution. -- John Skaller <skaller at users dot sourceforge dot net> Download Felix: http://felix.sf.net [-- Attachment #2: This is a digitally signed message part --] [-- Type: application/pgp-signature, Size: 189 bytes --] ^ permalink raw reply [flat|nested] 22+ messages in thread
* Re: [Caml-list] Type abstraction and (polymorphic) equality 2005-06-29 20:37 ` John Skaller @ 2005-06-30 9:53 ` Andreas Rossberg 2005-06-30 17:08 ` brogoff 2005-06-30 19:56 ` John Skaller 0 siblings, 2 replies; 22+ messages in thread From: Andreas Rossberg @ 2005-06-30 9:53 UTC (permalink / raw) To: caml-list John Skaller wrote: > > Executive Summary: I guess no wart free solution can exist. Where do you see the wart with Haskell's approach? -- Andreas Rossberg, rossberg@ps.uni-sb.de Let's get rid of those possible thingies! -- TB ^ permalink raw reply [flat|nested] 22+ messages in thread
* Re: [Caml-list] Type abstraction and (polymorphic) equality 2005-06-30 9:53 ` Andreas Rossberg @ 2005-06-30 17:08 ` brogoff 2005-06-30 17:22 ` Andreas Rossberg 2005-06-30 19:56 ` John Skaller 1 sibling, 1 reply; 22+ messages in thread From: brogoff @ 2005-06-30 17:08 UTC (permalink / raw) To: Andreas Rossberg; +Cc: caml-list On Thu, 30 Jun 2005, Andreas Rossberg wrote: > John Skaller wrote: > > > > Executive Summary: I guess no wart free solution can exist. > > Where do you see the wart with Haskell's approach? Which one? Haskell 98's? Or the multiparameter one with functional dependencies and ... (GHC and Hugs)? I'd love to see an ML with type classes and a simple module system, just so we could get experience. G'Caml looks promising too, and the integration with modules seems straightforward. -- Brian ^ permalink raw reply [flat|nested] 22+ messages in thread
* Re: [Caml-list] Type abstraction and (polymorphic) equality 2005-06-30 17:08 ` brogoff @ 2005-06-30 17:22 ` Andreas Rossberg 0 siblings, 0 replies; 22+ messages in thread From: Andreas Rossberg @ 2005-06-30 17:22 UTC (permalink / raw) To: caml-list brogoff wrote: >> >>Where do you see the wart with Haskell's approach? > > Which one? Haskell 98's? Or the multiparameter one with functional > dependencies and ... (GHC and Hugs)? Since the topic is just equality, plain simple H98 type classes are more than enough. -- Andreas Rossberg, rossberg@ps.uni-sb.de Let's get rid of those possible thingies! -- TB ^ permalink raw reply [flat|nested] 22+ messages in thread
* Re: [Caml-list] Type abstraction and (polymorphic) equality 2005-06-30 9:53 ` Andreas Rossberg 2005-06-30 17:08 ` brogoff @ 2005-06-30 19:56 ` John Skaller 2005-07-01 12:49 ` Andreas Rossberg 1 sibling, 1 reply; 22+ messages in thread From: John Skaller @ 2005-06-30 19:56 UTC (permalink / raw) To: Andreas Rossberg; +Cc: caml-list [-- Attachment #1: Type: text/plain, Size: 412 bytes --] On Thu, 2005-06-30 at 11:53 +0200, Andreas Rossberg wrote: > John Skaller wrote: > > > > Executive Summary: I guess no wart free solution can exist. > > Where do you see the wart with Haskell's approach? That is hard to answer without knowing what Haskell's approach is, perhaps you can outline it? -- John Skaller <skaller at users dot sourceforge dot net> Download Felix: http://felix.sf.net [-- Attachment #2: This is a digitally signed message part --] [-- Type: application/pgp-signature, Size: 189 bytes --] ^ permalink raw reply [flat|nested] 22+ messages in thread
* Re: [Caml-list] Type abstraction and (polymorphic) equality 2005-06-30 19:56 ` John Skaller @ 2005-07-01 12:49 ` Andreas Rossberg 0 siblings, 0 replies; 22+ messages in thread From: Andreas Rossberg @ 2005-07-01 12:49 UTC (permalink / raw) To: caml-list John Skaller wrote: > > That is hard to answer without knowing what Haskell's approach is, > perhaps you can outline it? Look here: http://citeseer.ist.psu.edu/wadler88how.html -- Andreas Rossberg, rossberg@ps.uni-sb.de Let's get rid of those possible thingies! -- TB ^ permalink raw reply [flat|nested] 22+ messages in thread
* Re: [Caml-list] Type abstraction and (polymorphic) equality 2005-06-29 0:31 Type abstraction and (polymorphic) equality Christophe TROESTLER 2005-06-29 9:12 ` [Caml-list] " Jon Harrop @ 2005-06-29 9:45 ` Jean-Christophe Filliatre 2005-06-29 17:33 ` William Lovas ` (2 subsequent siblings) 4 siblings, 0 replies; 22+ messages in thread From: Jean-Christophe Filliatre @ 2005-06-29 9:45 UTC (permalink / raw) To: Christophe TROESTLER; +Cc: O'Caml Mailing List Christophe TROESTLER writes: > > The problem was that the attached information (an additional field in > a record) was a cyclic data structure. From there on, all equality > tests became deadly! > ... I fully agree. I bumped into this issue a few months ago and helped a friend of mine to discover the same issue no later than yesterday! It is actually not really difficult to identify this issue: first, the Out_of_memory is raised very quickly; second, there is an explicit message when the Gc verbose mode is activated; finally, it is quite easy to find it with the debugger (one "run" and then one "back" will tell you that the Out_of_memory is raised during a structual comparison). But that's not the point. I have no good solution to propose, but it would be nice if we were not allowed to apply structural comparison on abstract (or private) datatypes. Then you would have to export an explicit equality function, and even if you are going to define it as (=) most of the time, you would have to think about it at least one second. But I agree that it is quite difficult to incorporate this in the type system. -- Jean-Christophe ^ permalink raw reply [flat|nested] 22+ messages in thread
* Re: [Caml-list] Type abstraction and (polymorphic) equality 2005-06-29 0:31 Type abstraction and (polymorphic) equality Christophe TROESTLER 2005-06-29 9:12 ` [Caml-list] " Jon Harrop 2005-06-29 9:45 ` Jean-Christophe Filliatre @ 2005-06-29 17:33 ` William Lovas 2005-06-29 18:08 ` sejourne_kevin 2005-06-30 12:19 ` Alain Frisch 4 siblings, 0 replies; 22+ messages in thread From: William Lovas @ 2005-06-29 17:33 UTC (permalink / raw) To: O'Caml Mailing List On Wed, Jun 29, 2005 at 02:31:11AM +0200, Christophe TROESTLER wrote: > Let me start with a little story that happened to me recently. > [...] > > The problem was that the attached information (an additional field in > a record) was a cyclic data structure. From there on, all equality > tests became deadly! (I would have preferred to have the exception > Invalid_argument "equal: abstract value".) What made matters worse is > that the compiler could not help me to find the locations of such > problems -- which can be hidden e.g. in List.mem. Not a nice job to > do... A harrowing and tragic tale indeed! While not really a solution to your problems, you *can* obtain the "abstract value" exception behavior with a little trick; Jacques Garrigue posted about it to the list a couple of months ago: http://caml.inria.fr/pub/ml-archives/caml-list/2005/04/66b52e5c944a3bd4c45e8b68c450461a.en.html I say it's no solution because (a) it doesn't keep you from having to write your own equality predicate with a different name, and (b) the compiler gives you no static warnings about invalid uses -- might as well program in Scheme! ;) cheers, William ^ permalink raw reply [flat|nested] 22+ messages in thread
* Re: [Caml-list] Type abstraction and (polymorphic) equality 2005-06-29 0:31 Type abstraction and (polymorphic) equality Christophe TROESTLER ` (2 preceding siblings ...) 2005-06-29 17:33 ` William Lovas @ 2005-06-29 18:08 ` sejourne_kevin 2005-06-30 9:51 ` Andreas Rossberg 2005-06-30 12:19 ` Alain Frisch 4 siblings, 1 reply; 22+ messages in thread From: sejourne_kevin @ 2005-06-29 18:08 UTC (permalink / raw) Cc: O'Caml Mailing List Christophe TROESTLER a écrit : > - One introduces the same capability of providing a special equality > (comparison) for certain types but, during compilation, "expand" > functions till the type for "=" is given by known functions > (something like a "generic" equality). I guess however that that > may cause problems with separate compilation... A generic equality should be one that work with recursives. A such equality is slower than the Pervasives.(=) one. So (=) is just an optimisation of a generic one that don't have been fully implemented. When the compiler generate code he have the complete type, no ? so he can know if a type is recursives or not, so he can select the slow but recursives compliant version are the actual. Maybe that it is more complex than this, no? ___________________________________________________________________________ Appel audio GRATUIT partout dans le monde avec le nouveau Yahoo! Messenger Téléchargez cette version sur http://fr.messenger.yahoo.com ^ permalink raw reply [flat|nested] 22+ messages in thread
* Re: [Caml-list] Type abstraction and (polymorphic) equality 2005-06-29 18:08 ` sejourne_kevin @ 2005-06-30 9:51 ` Andreas Rossberg 2005-06-30 19:54 ` John Skaller 0 siblings, 1 reply; 22+ messages in thread From: Andreas Rossberg @ 2005-06-30 9:51 UTC (permalink / raw) To: O'Caml Mailing List sejourne_kevin wrote: > > A generic equality should be one that work with recursives. Not so easy. In order to be a proper equivalence test for cyclic data structures it essentially had to test graph equivalence, which is the same as testing equivalence of DFAs. So it would be a completely different algorithm, with significant complexity in space and time. > When the compiler generate code he have the complete type, no ? No, not in the presence of polymorphism. > so he > can know if a type is recursives or not, so he can select the slow but > recursives compliant version are the actual. Recursion on the type level does not necessarily imply recursion on the value level. Just consider lists, they are rarely cyclic. On the other hand, there may be recursion even where it is not visible in types, e.g. when you have implicit forms of existential quantification, like for abstract types, (non-recursive) object types, function types (closures). So this is not a useful criterium. In Alice ML, where we have recently added such a co-recursive equivalence operation, we opted for turning it into a separate operation, to avoid these issues. -- Andreas Rossberg, rossberg@ps.uni-sb.de Let's get rid of those possible thingies! -- TB ^ permalink raw reply [flat|nested] 22+ messages in thread
* Re: [Caml-list] Type abstraction and (polymorphic) equality 2005-06-30 9:51 ` Andreas Rossberg @ 2005-06-30 19:54 ` John Skaller 2005-06-30 22:24 ` Alain Frisch 0 siblings, 1 reply; 22+ messages in thread From: John Skaller @ 2005-06-30 19:54 UTC (permalink / raw) To: Andreas Rossberg; +Cc: O'Caml Mailing List [-- Attachment #1: Type: text/plain, Size: 1225 bytes --] On Thu, 2005-06-30 at 11:51 +0200, Andreas Rossberg wrote: > sejourne_kevin wrote: > > > > A generic equality should be one that work with recursives. > > Not so easy. In order to be a proper equivalence test for cyclic data > structures it essentially had to test graph equivalence, which is the > same as testing equivalence of DFAs. So it would be a completely > different algorithm, with significant complexity in space and time. I do not see that. The current algorithm is recursive descent is it not? That can also be used with a trivial modification to test graph equivalence, by simply keeping a list of visited nodes and not revisiting them. The problem of course is that the cost per node is O(N) where N is the recursion depth. Profiling indicates my code spends up to 60% of all time doing comparisons. > In Alice ML, where we have recently added such a co-recursive > equivalence operation, we opted for turning it into a separate > operation, to avoid these issues. That seems reasonable, since the client will usually know if the data structure contains cycles or not. -- John Skaller <skaller at users dot sourceforge dot net> Download Felix: http://felix.sf.net [-- Attachment #2: This is a digitally signed message part --] [-- Type: application/pgp-signature, Size: 189 bytes --] ^ permalink raw reply [flat|nested] 22+ messages in thread
* Re: [Caml-list] Type abstraction and (polymorphic) equality 2005-06-30 19:54 ` John Skaller @ 2005-06-30 22:24 ` Alain Frisch 0 siblings, 0 replies; 22+ messages in thread From: Alain Frisch @ 2005-06-30 22:24 UTC (permalink / raw) Cc: O'Caml Mailing List John Skaller wrote: > I do not see that. The current algorithm is recursive descent > is it not? That can also be used with a trivial modification > to test graph equivalence, by simply keeping a list of visited > nodes and not revisiting them. If you want the equivalence to be invariant by unfolding, you need to keep a set of pairs of nodes, not just a set of nodes. -- Alain ^ permalink raw reply [flat|nested] 22+ messages in thread
* Re: [Caml-list] Type abstraction and (polymorphic) equality 2005-06-29 0:31 Type abstraction and (polymorphic) equality Christophe TROESTLER ` (3 preceding siblings ...) 2005-06-29 18:08 ` sejourne_kevin @ 2005-06-30 12:19 ` Alain Frisch 2005-06-30 12:32 ` padiolea 4 siblings, 1 reply; 22+ messages in thread From: Alain Frisch @ 2005-06-30 12:19 UTC (permalink / raw) To: Christophe TROESTLER; +Cc: O'Caml Mailing List Christophe TROESTLER wrote: > I'll be glad to hear similar experiences and comments about the above > ideas. In my opinion, it is a good idea to always define one's own comparison (and hash) function. You know better than the compiler and the runtime system how your data is to be compared, which details should be ignored, how to deal with cycles, and so on. In addition, your custom functions will be more efficient than the generic ones. There are several tools to generate automatically comparison functions from type declarations. I often redefine the comparison operators (=), (<=), ... with dummy types at the beginning of modules to avoid using them by inadvertence (this does not catch uses of List.mem-like functions, though). -- Alain ^ permalink raw reply [flat|nested] 22+ messages in thread
* Re: [Caml-list] Type abstraction and (polymorphic) equality 2005-06-30 12:19 ` Alain Frisch @ 2005-06-30 12:32 ` padiolea 2005-06-30 12:57 ` Alain Frisch 0 siblings, 1 reply; 22+ messages in thread From: padiolea @ 2005-06-30 12:32 UTC (permalink / raw) To: Alain Frisch; +Cc: Christophe TROESTLER, O'Caml Mailing List > Christophe TROESTLER wrote: >> I'll be glad to hear similar experiences and comments about the above >> ideas. > > In my opinion, it is a good idea to always define one's own comparison > (and hash) function. I know many people who have "defunctorized" the Map and Set modules and hardcoded a call to the generic compare to be able to use Set and Map as easily as you use List. Even with this generic compare those Set and Map seems quite good enough (and far better of course that using List for representing sets and associations). > You know better than the compiler and the runtime > system how your data is to be compared, Well then you are perhaps agree with the C++ folks who think that they better know how to manage memory than the compiler and runtime system. > which details should be ignored, > how to deal with cycles, and so on. In addition, your custom functions > will be more efficient than the generic ones. > There are several tools to > generate automatically comparison functions from type declarations. Which one ? I know Tywith but it is not in the standard distribution and it requires camlp4 and there is sometimes some annoying behaviour when you use camlp4 (such as backtraces that points to wrong information) > I often redefine the comparison operators (=), (<=), ... with dummy > types at the beginning of modules to avoid using them by inadvertence > (this does not catch uses of List.mem-like functions, though). > > -- Alain > > _______________________________________________ > Caml-list mailing list. Subscription management: > http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list > Archives: http://caml.inria.fr > Beginner's list: http://groups.yahoo.com/group/ocaml_beginners > Bug reports: http://caml.inria.fr/bin/caml-bugs > ^ permalink raw reply [flat|nested] 22+ messages in thread
* Re: [Caml-list] Type abstraction and (polymorphic) equality 2005-06-30 12:32 ` padiolea @ 2005-06-30 12:57 ` Alain Frisch 0 siblings, 0 replies; 22+ messages in thread From: Alain Frisch @ 2005-06-30 12:57 UTC (permalink / raw) To: padiolea; +Cc: Christophe TROESTLER, O'Caml Mailing List padiolea@irisa.fr wrote: > I know many people who have "defunctorized" the Map and Set modules > and hardcoded a call to the generic compare to be able to use > Set and Map as easily as you use List. > Even with this generic compare those Set and Map seems quite good > enough (and far better of course that using List for representing > sets and associations). By "good", you mean "efficient", I guess. I understand that easy solutions are sometimes good enough. My claim is that in this case, the easy solution is also a risky one. An example of how using the easy solution can bite you: http://pauillac.inria.fr/bin/caml-bugs/fixed?id=2916 >>You know better than the compiler and the runtime >>system how your data is to be compared, > > > Well then you are perhaps agree with the C++ folks who think > that they better know how to manage memory than the compiler and runtime > system. No, I don't agree. I know that the runtime system can help me managing the memory. There are exceptions (I know that I need to clear explicitly some global tables or references to avoid memory leaks), but in general, the runtime system does a good job and the GC behavior is always safe, so there is no problem using it. Concerning comparisons, you currently need to choose either to rely purely on the generic function or to implement a custom one yourself. You cannot use your knowledge to improve the automatic behavior. The generic comparison is not always safe, so when you write polymorphic code, you simply cannot assume that generic comparison is ok. (I don't claim that the current situation is satisfactory, only that considering it, generic comparison is too dangerous.) >>There are several tools to >>generate automatically comparison functions from type declarations. > > > Which one ? I know Tywith but it is not in the standard distribution > and it requires camlp4 and there is sometimes some annoying > behaviour when you use camlp4 (such as backtraces that points > to wrong information) http://www.pps.jussieu.fr/~maurel/programmation/ -- Alain ^ permalink raw reply [flat|nested] 22+ messages in thread
end of thread, other threads:[~2005-07-01 12:49 UTC | newest] Thread overview: 22+ messages (download: mbox.gz / follow: Atom feed) -- links below jump to the message on this page -- 2005-06-29 0:31 Type abstraction and (polymorphic) equality Christophe TROESTLER 2005-06-29 9:12 ` [Caml-list] " Jon Harrop 2005-06-29 10:06 ` Andreas Rossberg 2005-06-29 13:32 ` Christophe TROESTLER 2005-06-29 23:39 ` brogoff 2005-06-30 7:46 ` Christophe Raffalli 2005-06-29 20:27 ` Christophe TROESTLER 2005-06-29 20:37 ` John Skaller 2005-06-30 9:53 ` Andreas Rossberg 2005-06-30 17:08 ` brogoff 2005-06-30 17:22 ` Andreas Rossberg 2005-06-30 19:56 ` John Skaller 2005-07-01 12:49 ` Andreas Rossberg 2005-06-29 9:45 ` Jean-Christophe Filliatre 2005-06-29 17:33 ` William Lovas 2005-06-29 18:08 ` sejourne_kevin 2005-06-30 9:51 ` Andreas Rossberg 2005-06-30 19:54 ` John Skaller 2005-06-30 22:24 ` Alain Frisch 2005-06-30 12:19 ` Alain Frisch 2005-06-30 12:32 ` padiolea 2005-06-30 12:57 ` Alain Frisch
This is a public inbox, see mirroring instructions for how to clone and mirror all data and code used for this inbox