At 14:11 +0200 1999/07/27, Koen Claessen wrote:
>The contructs we add to the language are:
>
> type Ref a = ...
>
> ref :: a -> Ref a
> deref :: Ref a -> a
> (<=>) :: Ref a -> Ref a -> Bool
>
>This basically gives you ML-style but non-updatable references, but you
>can compare them for equality. You can also see it as pointer equality,
>but only on objects of a certain type, so that you have to explicit at
>creation time if you want to pointer-compare them later.
>
> let x = ref 27 in x <=> x
>
>yields True, whereas
>
> ref 27 <=> ref 27
>
>yields False.
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.
Let's rewrite it with an arbitrary equivalence relation x ~ y. Then it says
if a ~ b then F(a) ~ F(b)
In other words, one focuses on the semantic function objects F which are
homomorphisms with respect to the equivalence relation ~.
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.) In this case
if a ~ b then F(a) ~ F(b)
simply means that it is a well defined real valued function. But it does
not prevent a mathematician to consider all Cauchy sequences in such a
construction, and functions which do not satisfy
if a ~ b then F(a) ~ F(b)
One might guess that for a general purpose use, these are the interesting
functions, but that is all.
So the two conditions
if a `eq` b then F(a) `eq` F(b)
if a `req` b then G(a) `req` G(b)
will only lead to different classes of functions (homomorphisms with
respect to different properties). The latter will in math more correspond
to consider all underlying set functions, whereas in the former case one
restraints at preserving certain semantic structure.
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.
(One might guess that the referential transparency concept pops up in
functional language, because it somehow is important in constructive math.
Then it is interesting that the approach break down in describing all the
innards of the runtime object of a computers. Perhaps this is a weak spot
of constructive math relative traditional math, then.)
Hans Aberg
* Email: Hans Aberg <mailto:[EMAIL PROTECTED]>
* Home Page: <http://www.matematik.su.se/~haberg/>
* AMS member listing: <http://www.ams.org/cml/>
