On 27-Jul-1999, Hans Aberg <[EMAIL PROTECTED]> wrote:
> I think there is not a big problem with breaking "referential
> transparency"; the same think happens in pure math often and it is part of
> a normal procedure of constructing mathematical objects:
>
> Referential transparency means that
> if a = b then F(a) = F(b), where "=" is semantic equality
> But "=" is in reality just one of several different possible equivalence
> relations.
Sure. But in Mercury, and in mathematics, the way it works is that
there is only one equality relation on any given type; there may be
many equivalence relations, but one of them is distinguished. If you
want to consider values with a different equivalence relation for their
equality, then you construct a new type.
In mathematics people are generally pretty sloppy about declaring the types,
instead assuming that the reader will infer the types from the context, so
this may not be so clear in mathematics as it is in Mercury or Haskell.
But nevertheless knowing the type (and hence knowing which equivalence
relation is being used for equality) is crucial to understanding the
mathematics.
In Haskell, things are not quite as nice, semantically speaking, as they are
in Mercury and mathematics, because Haskell has two different distinguished
equivalence relations: `=' and `=='.
When you construct a new type, Haskell doesn't let you define equality (`=')
for that type, it only lets you define `=='. Haskell promises (and compilers
may rely on) referential transparency with respect to `=', but not
referential transparency with respect to `=='.
> Take an example: construct say the real numbers R as the Cauchy sequences
> of rational numbers Q modulo the equivalence relation that two sequences
> have the same limit (omitting boring mathematical details). Then a lot of
> different Cauchy sequences of rational numbers will represent the same real
> number. (So this corresponds roughly to different references of the same
> semantic object in a computer language.)
These reference have different types: one is the type of real numbers, the
other is the type of Cauchy sequences of rationale numbers.
So long as the type system keeps the distinction between a type and its
representation, constructing new types in this way doesn't break referential
transparency.
> So I think one should not bother too much about breaking referential
> transparency when allowing access to the underlying runtime covers. On the
> contrary, it seems that this exactly what one should expect to happen.
When you break open the underlying runtime covers (cross an abstraction
boundary) what you get is nondeterminism. But there's no reason why
this should be or needs to be done in a way that breaks referential
transparency.
This comment applies as much to mathematics as to Haskell.
In mathematics, `x = y => f(x) = f(y)' is an axiom,
and so if you define a function which violates this axiom,
you have an inconsistent system.
If you want your mathematics to be based on sound foundations,
then you need to keep track of the types, so that you can avoid such
inconsistencies.
--
Fergus Henderson <[EMAIL PROTECTED]> | "I have always known that the pursuit
WWW: <http://www.cs.mu.oz.au/~fjh> | of excellence is a lethal habit"
PGP: finger [EMAIL PROTECTED] | -- the last words of T. S. Garp.
