[Haskell-cafe] Test on identity?

[Olaf Klinke]

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

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
"Add (Val 1) (Val 1)"
ghci> show b
"Add (Val 1) (Val 1)"
ghci> let f :: Ex -> IO Bool; f (Val _) = return False; f (Add x y) =
liftA2 eqStableName (makeStableName x) (makeStableName y)
ghci> f a
False
ghci> f b
True