equality

[veldhvz]

> >A question: "Is it possible to implement in Clean
> >an operator that checks for token-identity?"
>
> The question calls for making an explicit distinction between two kinds of
> equality-- extensional equality (often called "equivalence") and
> intensional equality (often called "identity"). Obviously identity implies
> equivalence, but not vice versa.
> 
> In pure functional languages such as Clean, the  notion of referential
> transparency (RT henceforth) is a fundamental principle. It's the basis for
> the style of reasoning that makes correctness proofs in these languages so
> much more direct than in languages that don't adhere to it. It also
> underlies important aspects of the implementation, such as graph reduction,
> lazy evaluation, and many optimization techniques.
> 
> The principle of RT means that a subexpression can be replaced by an
> *equivalent* subexpression without changing the value of any expression to
> which it belongs. Clearly we're talking about equivalence here, not
> identity (replacing an expression with itself doesn't get much work done!).
> 
> Now imagine that Clean were to offer (as Lisp does) two distinct equality
> operators:
> 
>         `eq`    equivalence     a `eq` b <=> a and b have
>                                 the same value
> 
>         `id`    identity        a `id` b <=> a and b occupy
>                                 the same location
> 
> Suppose we have two expressions
> 
>         x = 2+2
> 
>         y = 1+3
> 
> which are equivalent but not identical:
> 
>         x `eq` y  ==>  True     (0)
>         x `id` y  ==>  False    (1)
> 
> And of course
> 
>         x `id` x  ==>  True     (2)
> 
> Now compare (1) and (2): Replacing the subexpression x with an equivalent
> subexpression y has changed the value of the expression to which it
> belongs. The conclusion is that if `id` comes into a language, RT goes out.
> 
> It would be quite permissible for the *implementation* of an equivalence
> operator to test for identity, as a shortcut. But the test has to be
> performed outside the functional language-- if `id` is admitted to the
> language, its logical foundation is fatally undermined.

Thank you for pointing this out to me. I was aware that something
like this might be the case, but I didn't see exactly what was 
the problem.

However, there remains to be a problem with the effecient
*implementation* of the equality operator as it is defined 
now in Clean. This is because the programmer can define
an instance that returns False even when the arguments are 
token-identical. This means that the notion of equivalence
that is used to define referential transparency is not
the same as that defined by the == operator.

So let me rephrase my original question:
Why isn't there a restriction defined on the instances of the
== operator so that x==x  must always yield True?
This restriction would allow the compiler to make the suggested
optimization.

Or is the Clean compiler even more clever than I thought possible,
and does it already check whether a particular instance of == satisfies
the restriction and generates the shortcut code accordingly?

-- 
Gert Veldhuijzen van Zanten
---------------------------------------------------
IPO, Center for Research on User-System Interaction
phone: +31 40 2475260,          fax: +31 40 2431930             
URL: http://www.tue.nl/ipo/people/veldhvz
e-mail: veldhvz@ipo.tue.nl  
P.O. Box 513, 5600 MB  Eindhoven, the Netherlands     
---------------------------------------------------