Re: [Caml-list] Improper generic equality in Caml (Rossberg's SML vs Caml)

[rossberg@ps.uni-sb.de]

Diego Olivier Fernandez-Pons wrote:
>
> What does Andreas Rossberg in his SML vs. Caml page
>
>     http://www.ps.uni-sb.de/~rossberg/SMLvsOcaml.html
>
> mean when he says that
>
>    [Caml] Does not have a proper generic equality
>    on one hand (1, r) != (1, r), on the other (1, r) = (1, ref 1)

To clarify: "proper" refers to "generic".

The problem example is the one given on the left-hand side of the table.
Let me elaborate.

OCaml has two equalities: one fully structural, the other physical. Both
work fine in special cases, but neither has the "right" semantics in the
general case, where you deal with an arbitrary mixture of structural and
mutable types. By "right" I mean equality in the standard Leibniz sense,
where you can always replace equals with equals, without changing the
outcome. Neither of OCaml's operators has this property.

More conretely, given

  let r = ref 1

then the pairs (1, r) and (1, ref 1) are distinguishable by the effect of
assignment. Still, OCaml's = considers them equal. On the other hand, it
is not observable (by other means) whether the pair (1, r) is constructed
once or twice, but == distinguishes these cases. Consequently, neither
operator implements equality "correctly" on type (int * int ref), because
either delivers a "wrong" result for one of these two examples.

This problem can sometimes make translation from SML (which has Leibniz
equality) to OCaml subtly difficult (that the inverse direction is
potentially difficult is more obvious).

Cheers,
- Andreas