equality

Hamilton Richards Jr. ham@cs.utexas.edu
Thu, 3 Jul 1997 12:28:20 -0500


At 4:24 PM +0200 7/3/97, veldhvz wrote:

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

---------------------

This raises a meta-question: Is RT worth it?

As veldhvz notes, it's not without its costs. The question often arises
when imperative programmers encounter functional programming's restrictions
for the first time. Not only are they unused to these restrictions in
particular, but they tend to find the very notion of restrictions absurd.
After all, isn't software supposed to be a field in which whatever we can
imagine can be built, unfettered by the mundane constraints of the physical
world?

Older disciplines, such as engineering and the arts, have less trouble with
the notion of restrictions. The composers of sonnets and sonatas willingly
accept rigid formal limits; designers of skyscrapers accept restrictions
imposed by gravity and the strength of their materials.

Software engineering has grudgingly accepted a few restrictions. The
"go-to" wars seem to have subsided, and ADTs (which restrict access to
their implementations) are positively fashionable (under the banner of
"object orientation"). Nevertheless, our field clearly hasn't found the
right set of restrictions yet-- our skyscrapers are still too expensive,
and they keep falling over.
   Functional programming can be viewed as an experiment, testing the
proposition that RT is a useful restriction, akin to the rules that enable
engineers to build trustworthy skyscapers. Perhaps we can't yet claim to
have proved that RT is a key, but there's more than enough evidence already
(prominently including the Clean group's achievements) to keep me enrolled
in the experiment.

Regardless of the evidence, it's going to be an uphill fight. Many of our
colleagues are temperamentally opposed to the very notion of rules and
restrictions. They're a bit like the cattle barons (a simile that may be
more effective here in Texas than in The Netherlands) who fought the
fencing of the range which was a precondition for farming and other
enterprises that couldn't stand being walked over by stray cattle.
   No analogy is perfect, however. The range wars broke out because the
range was finite, but in the software arena there's plenty of space for the
"free range" and various kinds of fenced ranges --software "provinces",
each with its rules and principles-- to coexist. In the fullness of time,
the worth of each province's constitutional principles will be apparent in
its products.
   In the mean time, a newcomer to a software province should recognize the
essential nature of its principles. S/he should either accept them or move
on --perhaps to found a new province! For programmers who find RT irksome,
the province of Scheme and ML is a short journey away.

--Ham (who obviously has too much time on his hands)



------------------------------------------------------------------
Hamilton Richards Jr.            Department of Computer Sciences
Senior Lecturer                  Mail Code C0500
512-471-9525                     The University of Texas at Austin
Taylor Hall 5.116                Austin, Texas 78712-1188
------------------------------------------------------------------