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

[John Skaller <skaller@users.sourceforge.net>]

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