From mboxrd@z Thu Jan 1 00:00:00 1970 Received: by pauillac.inria.fr; Fri, 26 Aug 94 13:50:27 +0200 Received: by pauillac.inria.fr; Fri, 26 Aug 94 13:49:52 +0200 From: Pierre Weis Message-Id: <9408261149.AA01884@pauillac.inria.fr> Subject: equality between functions To: caml-list@pauillac.inria.fr Date: Fri, 26 Aug 1994 13:49:51 +0200 (MET DST) X-Mailer: ELM [version 2.4 PL21] Content-Type: text/plain Sender: weis@pauillac.inria.fr [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 : int -> int #let g x = x + 1;; Value g is : 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 ----------------------------------------------------------------------------