At 17:15 +1000 1999/07/28, Fergus Henderson wrote:
>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.
Actually, it is just an illusion that referential transparency is broken by
> ref 27 <=> ref 27
>
>yields False.
Because the semantic runtime meaning of this is that two different objects,
a location holding information about "27", and the address (or reference)
itself. The compiler, as a convenience to the user (called "abuse of
language" by the Bourbaki team; see below), allows one to not indicate all
information about "27" in the computer code itself.
If we write out the full semantic information, then it would have looked as
(27, ref1) <=> (27, ref2)
and it is pretty clear that it would cause false as a result if ref1 is not
equal to ref2.
The same problem would happen with
27 <=> 27
if the compiler is allowed to infer say the type Int in the first case and
the type Integer in the second case, and the two different "27"'s are
considered different.
So the paradox seems to arise because the compiler is allowed to generate
semantic information about the runtime objects which is not explicitly
describes in the language.
This is pretty common with math notation of course. The above mentioned
Bourbaki team wanted to describe math as exactly as possible, without the
ambiguities of classical math. But they then realized that the notation
became unmanageable to humans; hence they started with this "abuse of
language" notion, that is, allowing deliberate sloppiness in notation, in
order to make the math more readable to humans.
As for a math description of references, one could take the view that one
always constructs objects a, with references r. Then what is indicated in
the language is often the object pairs (a, r) modulo the equivalence
relation that the references differ.
Strictly speaking, one should then not have a class Ref, but a class Deref
which removes the references. The code should look as (in pseudo- C++)
Ref r1, r2
(27, r1) <=> (27, r2) -- Yields false
(27, r1) <=> (27, r1) -- Yields true
deref (27, r1) <=> deref (27, r2) -- Yields false
As a convenience to the user, one is allowed to write
deref { -- Need not indicate references explicitly
27 <=> 27 -- Yields true.
}
Hans Aberg
* Email: Hans Aberg <mailto:[EMAIL PROTECTED]>
* Home Page: <http://www.matematik.su.se/~haberg/>
* AMS member listing: <http://www.ams.org/cml/>
