equality between functions

equality between functions

[Martin Mueller]

I am just wondering, why CAML light decided to allow for 

#let g x = x in g=g;;

to succeed with 

-: bool = true

but fail on (eg) 

#(function x -> x) = (function x -> x);;
Uncaught exception: Invalid_argument "equal: functional value"

I understand that there are reasons to avoid 
equality between functions, but then should not equality and
inequality be handled symmetrically?
For instance, SML/NJ does so and fails on 

- let fun g x= x in g=g end;

std_in:0.0-0.0 Error: operator and operand don't agree (equality type required)
  operator domain: ''Z * ''Z
  operand:         ('Y -> 'Y) * ('X -> 'X)
  in expression:
    = (g,g)


Could someone shed some light onto that issue? I would also 
be interested in pointers to the literature on that topic.
Is there a basic reference on equality types? 

-- Martin M"uller

---
Martin M"uller,   DFKI,  Stuhlsatzenhausweg 3,  D-66123 Saarbruecken,   Germany
Tel: +49 681 302-5329;   Fax: +49 681 302-5341;    Net: mmueller@dfki.uni-sb.de

equality between functions

[Pierre Weis]

[Martin M"uller asked a question about equality in Caml Light.]

Equality in ML is a hard problem, since it cannot be a regular
polymorphic function: the ``='' primitive has to know something about
the stucture of its arguments to recursively test their components.
That's why equality is always treated especially in polymorphic
languages: Haskell uses its class feature and runtime dictionaries,
and SML features these ad hoc equality types and equality type
variables just to handle the primitive equality. In Caml, there is no
such mechanism specific to equality: equality is a polymorphic
primitive applicable to any type. This has some advantages and some
drawbacks: it is very convenient for the user to have a fully
polymorhic equality since it is very simple to use and understand. On
the other hand, there obviously exists some data types for which
equality has no meaning (at least no computable meaning) such as
functional values. These cases may be handled statically or dynamically:
in Haskell or SML theses failures are reported by the typechecker (no
functional type admit equality), while in Caml it is detected at
runtime by the ``='' primitive (when applied to an argument which is a
closure).

In fact in Caml equality on functional values is undefined: the result
is unreliable.

In practice in actual implementations, ``='' tests if its argument are
physically the same (stored in the same memory location). So, if ``=''
returns true when applied to functional values then the associated
closures are physically the same, and the corresponding functions are in
fact equal in the mathematical sense. If the closures are not
physically equal the primitive may either return false, as in Caml
V3.1, or fail as in Caml Light.

To exemplify this behaviour, note that your example works perfectly
in Caml V3.1:

   CAML (decstation) (V3.1.2) by INRIA Thu Feb 4 

#(function x -> x) = (function x -> x);;
true : bool

This cannot be exercised to more complex examples. For instance, we have:

#(function x -> x+1) = (function x -> x+1);;
true : bool

and

#(function x -> x+1) =  (function x -> x);;
false : bool

but if we bind two distinct instances of the same function to two
identifiers, these identifiers are bound to two distinct values that
cannot be proved the same by the ``='' primitive:

#let f x = x + 1;;
Value f is <fun> : int -> int

#let g x = x + 1;;
Value g is <fun> : int -> int

#f = g;;
false : bool

This is a current research area in the Projet Cristal to design a
mechanism to improve the treatment of equality in Caml. A paper
has been submitted to Popl 95 (and rejected from Popl 94!) on the
notion of generic polymorphic functions: this is a generalization of
the correct treatment of ``='' to other polymorphic primitives such as
input and output of values (for instance our system provides a
polymorphic print function) and user's defined ad hoc polymorphic
functions. An INRIA research report will occur very soon, and we can
send it to interested people.

Pierre Weis
----------------------------------------------------------------------------
Projet Cristal
INRIA, BP 105, F-78153 Le Chesnay Cedex (France)
E-mail: Pierre.Weis@inria.fr
Telephone: +33 1 39 63 55 98
Fax: +33 1 39 63 53 30
----------------------------------------------------------------------------