skaller wrote:
> On Sun, 2006-09-17 at 07:08 +0200, rossberg@ps.uni-sb.de wrote:
>
>> This problem can sometimes make translation from SML (which has Leibniz
>> equality)
>
> It does? I'm curious how it handles
>
> (a) functions
> (b) abstract types

By statically ruling out the use of generic equality on them. That's the
purpose of eqtypes in SML.

For the latter, the implementor of the abstract type can choose to allow
generic equality if the abstract equality coincides with representational
equality.

Of course, this solution comes with its own set of problems...

Btw, SML'97 even goes as far as disallowing the use of generic equality on
floats, because IEEE equality does not meet the requirements. You have to
use a special operator Real.== to compare them.

- Andreas