polymorphic equality and overloading

polymorphic equality and overloading

[Eijiro Sumii]

Dear Caml Developers/Users,

(sorry that I don't know French)

This might be an FAQ, but could someone please give a rationale to the
polymorphic (in)equalities such as = and < in Caml?  While they have a
parametric polymorphic type 'a -> 'a -> bool, their semantics is ad
hoc rather than parametric with respect to the type 'a (for example,
they are undefined for functions), which I found confusing to some
users---at least, a friend of mine was confused, and chose Haskell
(which has type classes) over Caml!

// Eijiro Sumii <sumii@saul.cis.upenn.edu>
//
// currently visiting: Department of Computer and Information Science,
// School of Engineering and Applied Science, University of Pennsylvania

Re: polymorphic equality and overloading

[Brian Rogoff]

On Thu, 29 Jun 2000, Eijiro Sumii wrote:
> Dear Caml Developers/Users,
> 
> (sorry that I don't know French)
> 
> This might be an FAQ, but could someone please give a rationale to the
> polymorphic (in)equalities such as = and < in Caml?

(Note: I'm no type theorist, just a humble programmer)

Equality really is overloaded, but since overloading isn't easily
integrated into ML style type systems, some other solution is chosen. 
In SML, it is eqtypes, in OCaml, it is polymorphic (in)equality. 
People are working furiously on better solutions as we write. I 
read in the "ML-2000" design paper that eqtypes would go away in the 
next (standard) ML, so clearly not everyone is happy with the SML 
solution either.

> While they have a
> parametric polymorphic type 'a -> 'a -> bool, their semantics is ad
> hoc rather than parametric with respect to the type 'a (for example,
> they are undefined for functions),

Well, there is a little decidability problem for function equality... :-)

> which I found confusing to some
> users---at least, a friend of mine was confused, and chose Haskell
> (which has type classes) over Caml!

I agree that polymorphic equality is a hack, but I'd advise patience. 
It isn't clear that type classes are the best solution, and Jun Furuse 
and Pierre Weiss are working on adding some form of overloading to OCaml. 
There have been some threads on this topic in the Caml list. See 

http://caml.inria.fr/caml-list/2216.html
http://caml.inria.fr/caml-list/2218.html

-- Brian

Re: polymorphic equality and overloading

[Eijiro Sumii]

> Equality really is overloaded, but since overloading isn't easily
> integrated into ML style type systems, some other solution is chosen. 

So, I'm wondering why equality is overloaded in Caml, unlike addition
(+ for integers, +. for floats, ^ for strings, etc.) for example.  Or,
why is equality automatically defined for tuples and datatypes, while
addition isn't?  Is that just because it is often useful?

Eijiro

Re: polymorphic equality and overloading

[Jacques Garrigue]

> > Equality really is overloaded, but since overloading isn't easily
> > integrated into ML style type systems, some other solution is chosen. 
> 
> So, I'm wondering why equality is overloaded in Caml, unlike addition
> (+ for integers, +. for floats, ^ for strings, etc.) for example.  Or,
> why is equality automatically defined for tuples and datatypes, while
> addition isn't?  Is that just because it is often useful?

The answer is in your sentence: how do you define addition on tuples ?
Or even on strings: ^ is not addition but concatenation;
fun s1 s2 -> string_of_float (float_of_string s1 +. float_of_string s2)
will give you a very different result.

The only form of overloading currently accepted in Caml is universal
overloading, that is operations available at all types.
Comparison is just "naturally" defined on almost anything, the only
exceptions being function closures which have no identity, and C data
when no custom operation is defined.
There is some arbitrary part in this definition, but even so
being able to compare values is useful anyway (Set and Map modules).
I do not really see what would be the use of an underspecified
addition on algebraic datatypes, for instance.

If you want other candidates for universal overloading, print would be a
better choice. Theoretically all values can be printed in a way or
another, and there may be uses for that. However this requires much
more runtime type information.

Regards,

---------------------------------------------------------------------------
Jacques Garrigue      Kyoto University     garrigue at kurims.kyoto-u.ac.jp
		<A HREF=http://wwwfun.kurims.kyoto-u.ac.jp/~garrigue/>JG</A>

Re: polymorphic equality and overloading

[Eijiro Sumii]

> The answer is in your sentence: how do you define addition on tuples ?

Just in the same way as equality is defined: element-wise.  Such
automatically defined "polymorphic addition" may not make sense, but
neither may the automatically defined polymorphic equality.  For
example, the polymorphic equality doesn't make sense for fractions
represented as tuples of a denominator and a numerator, polynomials
represented as lists of coefficients, complex numbers represented as
tuples of a magnitude and an angle, etc.

> Or even on strings: ^ is not addition but concatenation;
> fun s1 s2 -> string_of_float (float_of_string s1 +. float_of_string s2)
> will give you a very different result.

So will "fun s1 s2 -> string_of_float (float_of_string s1 =
float_of_string s2)" too.

> The only form of overloading currently accepted in Caml is universal
> overloading, that is operations available at all types.
> Comparison is just "naturally" defined on almost anything,

As I wrote above, I'm wondering whether the "naturally defined"
polymorphic (in)equalities make more sense than the element-wise
defined polymorphic addition.

> There is some arbitrary part in this definition, but even so
> being able to compare values is useful anyway (Set and Map modules).

Again, I doubt how often polymorphic (in)equalities work---for
instance, what if one represents a finite partial function "f" from
complex numbers (in the polar representation) to booleans, define "f
(0.0, 0.0)" to be true, and define "f (0.0, pi)" to be false using the
Map module?

> I do not really see what would be the use of an underspecified
> addition on algebraic datatypes, for instance.

Neither do I, and I also don't see whether the polymorphic
(in)equalities are more useful than the "polymorphic addition".  That
was (and is) my question.

Eijiro

Re: polymorphic equality and overloading

[Jacques Garrigue]

Hello Eijiro,

Your answer seems to be a little twisted from mine (and mine might
have been so too).

The point I was trying to make is just that Ocaml, to avoid
complications in the type system, only allows universal overloading,
that is overloaded operators which are defined at all types, and with
minimal runtime support (in practice little more than what would be
strictly necessary for the GC).

Comparison, hashing and marshalling are thus defined on almost
everything, with notable exceptions like functions, and C values when
no custom operations are provided.

I think hashing and marshalling will not bother you: they are not
expected to have any particular meaning, other than being reversible
(for marshalling) and fulfill a few properties (for hashing).

I really believe comparison (not only equality) must be understood in
the same way: operations that make easier to use some data structures.
Comparison may not be always the one you expect, but in practice this
is enough to define efficient sets and maps. It is the finest grain
relation available (without using physical equality), so that you will
have to define you own comparison if you need something coarser
(or a different order, but again generic comparison is not really
intended to give you the best order).  But it is meaningful (it
has some meaning) and useful (it has some uses).

Now the discussion is rather that having such "arbitrary" comparison
may be confusing. You see sometimes messages on the caml-list coming
from misunderstanding generic comparisons, on rationals for instance.
There is a tradeoff between simplicity and intuition.
I don't know why the choice has been so in Caml, but there are good
reasons on both sides.

Haskell's solution may seem more intuitive, but it uses a much more
complex type system, and puts the burden of writing comparisons on the
user. This is partly automatized, but with just the same problems you
indicated for Caml: the default definition of comparison may not be
the one you want.

Jacques

> > The answer is in your sentence: how do you define addition on tuples ?
> 
> Just in the same way as equality is defined: element-wise.  Such
> automatically defined "polymorphic addition" may not make sense, but
> neither may the automatically defined polymorphic equality.  For
> example, the polymorphic equality doesn't make sense for fractions
> represented as tuples of a denominator and a numerator, polynomials
> represented as lists of coefficients, complex numbers represented as
> tuples of a magnitude and an angle, etc.
> 
> > Or even on strings: ^ is not addition but concatenation;
> > fun s1 s2 -> string_of_float (float_of_string s1 +. float_of_string s2)
> > will give you a very different result.
> 
> So will "fun s1 s2 -> string_of_float (float_of_string s1 =
> float_of_string s2)" too.
> 
> > The only form of overloading currently accepted in Caml is universal
> > overloading, that is operations available at all types.
> > Comparison is just "naturally" defined on almost anything,
> 
> As I wrote above, I'm wondering whether the "naturally defined"
> polymorphic (in)equalities make more sense than the element-wise
> defined polymorphic addition.
> 
> > There is some arbitrary part in this definition, but even so
> > being able to compare values is useful anyway (Set and Map modules).
> 
> Again, I doubt how often polymorphic (in)equalities work---for
> instance, what if one represents a finite partial function "f" from
> complex numbers (in the polar representation) to booleans, define "f
> (0.0, 0.0)" to be true, and define "f (0.0, pi)" to be false using the
> Map module?
> 
> > I do not really see what would be the use of an underspecified
> > addition on algebraic datatypes, for instance.
> 
> Neither do I, and I also don't see whether the polymorphic
> (in)equalities are more useful than the "polymorphic addition".  That
> was (and is) my question.
> 
> Eijiro
 

Re: polymorphic equality and overloading

[Eijiro Sumii]

Hi Jacques (and Camlers),

> The point I was trying to make is just that Ocaml, to avoid
> complications in the type system, only allows universal overloading,

That's clear, I believe, and my question was "why overload the
(in)equalities".

> I think hashing and marshalling will not bother you:

No, they don't.

> Comparison may not be always the one you expect, but in practice
> this is enough to define efficient sets and maps.

I'm not sure why it is "enough in practice", for...

> you will have to define you own comparison if you need something
> coarser

this reason, but I agree that it has some uses as you wrote.

> Haskell's solution may seem more intuitive, but it uses a much more
> complex type system, and puts the burden of writing comparisons on the
> user.

I agree.  By the way, I myself am not a Haskell devotee---I just have
a friend who has chosen Haskell over Caml because of the issues on
overloading.  I hope to see what he says after he finish the "Gentle
Introduction to Haskell" tutorial.:-)

So, to summarize everyone's replies, the polymorphic (in)equalities
exist because they are of "some" use, though they might be somewhat
confusing---Is this correct?

Eijiro

Re: polymorphic equality and overloading

[Pierre Weis]

> Neither do I, and I also don't see whether the polymorphic
> (in)equalities are more useful than the "polymorphic addition".  That
> was (and is) my question.

Look at mathematics: equality is polymorphic. Addition is just overloaded.

Best regards,

Pierre Weis

INRIA, Projet Cristal, Pierre.Weis@inria.fr, http://cristal.inria.fr/~weis/

Re: polymorphic equality and overloading

[Eijiro Sumii]

> Look at mathematics: equality is polymorphic. Addition is just overloaded.

But as you know (and as I wrote in my previous messages), the
polymorphic equality in Caml is not at all the "equality in
mathematics" for many (or most?) datatypes.

Re: polymorphic equality and overloading

[Pierre Weis]

> > Look at mathematics: equality is polymorphic. Addition is just overloaded.
> 
> But as you know (and as I wrote in my previous messages), the
> polymorphic equality in Caml is not at all the "equality in
> mathematics" for many (or most?) datatypes.

No. As you know (and as I wrote in the Caml FAQ) the polymorphic
equality in Caml is the "equality in mathematics" for many (or most?)
datatypes. A few exceptions are (as in maths)
-- functions, for which mathematical equality needs complex demonstrations
-- quotient types using complex equivalence relations, such as
rational numbers or even reals or complex numbers.

Note that for those values equality is simply undecidable in general.
Note also that polymorphic equality is just pratical and useful, and
not confusing at all if you know something about mathematical entities
involved in the values manipulated by Caml programs. I would not
expect mathematical equality to decide if any two real numbers are
equal or not, since I know this is not decidable. I just would like to
be able to demonstrate the equality of 2 particular real numbers, and
hope the equality to be an extension of equality on simpler numbers,
such as integers or decimal point numbers or even rational numbers,
because I need a valid answer in those simple cases.  Unless for the
rational case, it is exactly what is now the Caml polymorphic
equality; going further to extend equality for rational numbers or
even any other user's defined data type is difficult and a current
research area. In the meantime, current polymorphic equality is the
simplest way of handling semantic equality in a polymorphic language.
Put it another way: polymorphic equality in Caml has some drawbacks,
some of them you should expect, since they are directly burried from
mathematics, few others you have to learn, but it is worth the
(little) effort.

Choosing Haskell for the treatment of equality in the language is just
a kind of misunderstanding of this powerful language and its profund
differences wrt other traditional programming languages. Tell me you
would prefer Haskell's clean lazy semantics, over Caml's strict
interpretation of computation. Tell me also you would prefer monads
and their fascinating categorical origin and propertie, over Caml's
trivial and traditional way of handling loops and sequences and side
effects. Tell me again you hate Caml's oversimplified printf compared
to the so versatile and complex Haskell's make_string. If you tell me
this kind of thing I will be glad to tell you Caml is not for you; I
will just warn you that all this Haskel powerful new stuff is really a
bit confusing for the beginner. But no doubt that if you can pay the
price it is worth the investment. You might also come back to Caml
after a while, just because it handles trivially a lot of useful
features (such as debugging); anyway, you will have learn a lot of
interesting things about programming in using Haskell. May be in the
first place, not to rely too much on polymorphic equality in your
programs, but to define your own complex equivalence relations on your
own complex data types.

All the best for your experiments with modern programming languages

Pierre Weis

INRIA, Projet Cristal, Pierre.Weis@inria.fr, http://cristal.inria.fr/~weis/

Re: polymorphic equality and overloading

[Eijiro Sumii]

Dear Dr. Pierre Weis,

> No. As you know (and as I wrote in the Caml FAQ) the polymorphic
> equality in Caml is the "equality in mathematics" for many (or most?)
> datatypes. A few exceptions are (as in maths)
> -- functions, for which mathematical equality needs complex demonstrations
> -- quotient types using complex equivalence relations, such as
> rational numbers or even reals or complex numbers.

Are the exceptions really "a few"?  For example---apart from (some
representations of) mathematical entities such as rational numbers,
complex numbers, polynomials, etc.---simple database entries like
"type student = { id : int; name : string; address : string }" would
have an equality different from the polymorphic equality (in the Set
and Map modules, for instance).

> Note also that polymorphic equality is just pratical and useful,

That is exactly what I asked in my second message ("Is that just
because it is often useful?"), and if the answer is yes, that's ok for
me.

> and not confusing at all if you know something about mathematical
> entities involved in the values manipulated by Caml programs.

Unfortunately, the different treatments of equality and addition (for
example) *did* confuse a friend of mine.  (He has a master's degree in
computer science in the University of Tokyo---as I also do---and
definitely knows much about mathematics and computer science.)

> Choosing Haskell for the treatment of equality in the language is just
(snip)
> All the best for your experiments with modern programming languages

Oh, I *love* OCaml.:-) As I wrote in a previous message, I'm not a
Haskell advocator.  (By the way, I've been programming in "modern"
languages---such as Scheme, Standard ML, Caml and Haskell---for 5
years, or 15 years if you admit LOGO as a modern language.)

Best wishes,

// Eijiro Sumii <sumii@saul.cis.upenn.edu>
//
// currently visiting: Department of Computer and Information Science,
// School of Engineering and Applied Science, University of Pennsylvania

Re: polymorphic equality and overloading

[Benjamin Werner]

> 
> > Look at mathematics: equality is polymorphic. Addition is just overloaded.

Sorry, but I cannot resist adding my two cents :)

It depends in what formalism you are doing mathematics in. In set
theory, equality is monomorphic, since all objects live in the same
universe.

Addition is overloaded indeed.


Cheers,

Benjamin


> 
> But as you know (and as I wrote in my previous messages), the
> polymorphic equality in Caml is not at all the "equality in
> mathematics" for many (or most?) datatypes.
> 

Re: polymorphic equality and overloading

[John R Harrison]

Eijiro Sumii writes:

| But as you know (and as I wrote in my previous messages), the
| polymorphic equality in Caml is not at all the "equality in
| mathematics" for many (or most?) datatypes.

Probably "most" is an exaggeration. But there are quite a few examples.
One I haven't seen mentioned in this thread is the type of floating point
numbers. The equality relation defined in the main standard for binary
floating point arithmetic (IEEE 754) is not reflexive. Specifically x = x
is false if x is a NaN ("not a number"). So again, this is really an
instance of overloading in CAML:

  #let x = 0.0 /. 0.0;;
  x : float = nan.0
  #x = x;;
  - : bool = false
  #x == x;;
  - : bool = true

Nevertheless, I find the CAML polymorphic equality and orderings pretty
useful and superficially simple, even if they sometimes have a touch of
arbitrariness about them.

Is it possible using just equality, not orderings, to write a set-compare
operation on polymorphic lists using fewer than 0(n^2) operations?
Trivially, using orderings, one can just sort both lists in O(n log n)
operations then run along them in order. Is there something comparably
efficient just using equality?

John.