Type abstraction and (polymorphic) equality

Type abstraction and (polymorphic) equality

[Christophe TROESTLER]

[-- 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) }

Re: [Caml-list] Type abstraction and (polymorphic) equality

[Jon Harrop]

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

Re: [Caml-list] Type abstraction and (polymorphic) equality

[Jean-Christophe Filliatre]

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

Re: [Caml-list] Type abstraction and (polymorphic) equality

[Andreas Rossberg]

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

Re: [Caml-list] Type abstraction and (polymorphic) equality

[Christophe TROESTLER]

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

Re: [Caml-list] Type abstraction and (polymorphic) equality

[William Lovas]

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

Re: [Caml-list] Type abstraction and (polymorphic) equality

[sejourne_kevin]

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

Re: [Caml-list] Type abstraction and (polymorphic) equality

[Christophe TROESTLER]

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

Re: [Caml-list] Type abstraction and (polymorphic) equality

[John Skaller]

[-- 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 --]

Re: [Caml-list] Type abstraction and (polymorphic) equality

[brogoff]

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

Re: [Caml-list] Type abstraction and (polymorphic) equality

[Christophe Raffalli]

[-- 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 --]

Re: [Caml-list] Type abstraction and (polymorphic) equality

[Andreas Rossberg]

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

Re: [Caml-list] Type abstraction and (polymorphic) equality

[Andreas Rossberg]

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

Re: [Caml-list] Type abstraction and (polymorphic) equality

[Alain Frisch]

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

Re: [Caml-list] Type abstraction and (polymorphic) equality

[padiolea]

> 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
>

Re: [Caml-list] Type abstraction and (polymorphic) equality

[Alain Frisch]

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

Re: [Caml-list] Type abstraction and (polymorphic) equality

[brogoff]

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

Re: [Caml-list] Type abstraction and (polymorphic) equality

[Andreas Rossberg]

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

Re: [Caml-list] Type abstraction and (polymorphic) equality

[John Skaller]

[-- 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 --]

Re: [Caml-list] Type abstraction and (polymorphic) equality

[John Skaller]

[-- 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 --]

Re: [Caml-list] Type abstraction and (polymorphic) equality

[Alain Frisch]

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

Re: [Caml-list] Type abstraction and (polymorphic) equality

[Andreas Rossberg]

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