Browse thread
[Caml-list] equality over functional value
[
Home
]
[ Index:
by date
|
by threads
]
[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
Date: | 2001-04-23 (07:56) |
From: | Xavier Leroy <Xavier.Leroy@i...> |
Subject: | Re: [Caml-list] equality over functional value |
> Hi, > > A friend of mine is just starting with ocaml. He was puzzled by the > following result: > > # let a i = i;; > val a : 'a -> 'a = <fun> > # let b i = i;; > val b : 'a -> 'a = <fun> > # a=b;; > Uncaught exception: Invalid_argument "equal: functional value". > # a=a;; > - : bool = true > # > > That is 'a=a' does not return the expected exception. Actually it > first hit this "curiosity" when creating a polymorphic 'sort' function > on lists - and by applying it to a [sort;sort..] list. It worked. > > Is this a bug? It's a questionable behavior. As Alain Frisch said, polymorphic structural equality is implemented by first testing physical (pointer) equality. Besides speed, this has the advantage that x == y implies x = y. However, this causes a = a where a is a function to return true instead of raising an exception as you expect. (Another weird consequence of this implementation of physical equality is that (nan, nan) = (nan, nan) returns true, which is incorrect according to the IEEE specs: the NaN float is not equal to itself!) The special case (first test pointer equality) in structural equality could be eliminated, although I don't know how big a performance impact this would have. More generally, equality between functions can be interpreted in several ways: 1- Extensional, pessimistic: f = g iff for all x, f x = g x, and since this is undecidable, equality always raises an exception when passed function values. 2- Extensional, approximated: same definition as above, but we return "true" in some cases where the two functions are guaranteed to be extensionally equal, e.g. f and g point to the same closure, or even f and g have the same code pointer and contain equal values in their environments. Otherwise, we raise an exception. 3- By representation: two functions are equal iff their closures are structurally equal, i.e. they have the same code pointer and contain equal values in their environment. Interpretation 3- is useless I think, because it depends very much on the compiler's closure representation strategy. In other terms, while a "true" result guarantees that the two functions are extensionally equal, a "false" result does not mean anything. The current interpretation 2- is semantically more sound: if it returns "true", then the two functions are extensionally equal; and it never returns "false", so it never claims that two functions are extensionally different! Still, it is rather unintuitive. Also, the current implementation exposes too much the order of the tests, i.e. "(0, f) = (1, g)" returns "false", but "(f, 0) = (g, 1)" raises an exception. Interpretation 1- is easiest to explain, although it entails a bit of a performance penalty as I said above. Food for thoughts... - Xavier Leroy ------------------- To unsubscribe, mail caml-list-request@inria.fr. Archives: http://caml.inria.fr