[Haskell-cafe] Test on identity?

[Joachim Durchholz]

Am 09.07.20 um 20:26 schrieb Olaf Klinke:
> Joachim Durchholz wrote:
>> This "identity is equality under change" definition captures not
>> just
>> two objects at identical addresses, but also proxies, network
>> objects,
>> files, and whatever there is.
>>
>> Step 3: Realize that if you have an immutable object, there is no
>> relevant difference between equality and identity anymore. (You can
>> make
>> various formal statements about this.)
> 
> Is that what is called "extensional equality"? Values a,b :: A are
> extensionally equal if they behave the same in all contexts.

To fully treat this, you have to explore some pretty interesting waters.

First, "all contexts" can mean pretty different things.
E.g. in Haskell (without unsafe* and similar), everything is immutable, 
so you have contexts that exist in languages with mutability but not in 
Haskell, and you'd have to define what "all contexts" means for a 
general term like "extensional equality".

Second, "behave the same" means that for all functions, the result it equal.
That's a recursive definition. You need fixed-point theory to turn that 
statement into an actual definition.
And that's surprisingly tricky.

One fixed point is to say "the largest set of equal objects", which 
means everything is equal to everything - fits the above definition 
(applying any function to anything will trivially return results that 
are equal under this definition), but is obviously not what we wanted.

Another one would be to have what we'd intuitively define as equality. 
Say, in Haskell, the minimum set of equalities that makes different 
constructor calls unequal. (Plus a handful of clerical definitions to 
catch special cases like integers.)

Another one would be to have what we'd intuitively define as identity.

Plus various other fixed points.

For example, consider proxies - say, an object that talks to a remote 
machine to produce its function results.
Now if you assume a proxy for integer values, is the proxy equal to an 
arbitrary integer you may have locally?
Again, this depends on what fixed point you choose for your equality 
definition. You can define that as an exception, you consider two 
objects equal if their functions return equal results, except for those 
that inspect the proxy-specific state; then proxy and local value are 
equal. Or you don't make an exception, then the two are not equal.
 From a mathematical standpoint, either fixed point will satisfy the 
above recursive definition (definition template, if you will). From a 
computing standpoint, you'll find that depending on context, you want 
one or the other!

There are different types of proxy objects, and you can have different 
kinds of equality depending on how you treat them.

That multitude of equality functions is pretty useless in a programming 
context; nobody wants to mentally deal with a gazillion of subtly 
different equalities!
So I belive what one should do in practice is to have converter 
functions. E.g. one that turns an Int proxy into an Int, merely by 
stripping the proxy-specific functions.
That keeps the special cases to the place where they belong - all those 
types that have funky special kinds of equality.
Mutable data is another case of this. The equality of a mutable object 
can be defined as identity, and a converter function returns an 
immutable copy so that equality is what's usually considered "value 
equality" (equals() in Java).
(Languages that do not cleanly separate mutable and immutable types will 
still have to deal with two equalities, value equality and identity... 
well, the above is type and language design theory, practical languages 
are always a set of trade-offs, restricted by the limited knowledge and 
experience of the language designer. I guess that's why we have so many 
programming languages.)

Regards,
Jo