Sat Jul 11 14:19:07 UTC 2020

```> 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
> >
> > 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.)
>

I find it easier to intuitively define what extensional inequality
means: As a domain theorist I declare two values unequal if there is an
open set (a semi-decidable property) containing one but not the other
value. For pure types t (not involving IO) that means there is a
function
semidecide :: t -> ()
that returns () for the one value and bottom for the other. I can not
say how this would extend to impure types and I tend to agree with you
that the notion of equality then depends on the intended semantics.
Below the semidecision would have type t -> I0 ()

However, using StableName (thanks, Zemyla and Viktor!) indeed one is
able to detect sharing. It works only after forcing the values, though.
Apparently StableName does not work on thunks.

Olaf

ghci> import System.Mem.StableName
ghci> import  Control.Applicative
ghci> data Ex = Val Int | Add Ex Ex deriving (Show)
ghci> a = Add (Val 1) (Val 1)
ghci> b = let v = Val 1 in Add v v
ghci> show a