Simon Peyton-Jones wrote:
> let x = (a,b) in x `req` x = True
> but
> (a,b) `req` (a,b) = False
>
> So referential transparency is lost. This is a high price to pay.
> You are right that *something* is needed; but I don't yet know what.
Couldn't we treat it as an optimization? If I define a class
>class REq a where
> equal :: a -> a -> Bool
> {- equal x x === True -}
Say I want to use more efficient tree comparison. As usual I write
>data Tree a = Nil | Node a (Tree a) (Tree a)
>equalTree :: Eq a => Tree a -> Tree a -> Bool
>equalTree Nil Nil = True
>equalTree (Node x t1 t2) (Node y t1' t2') =
> (x == y) && (equalTree t1 t2) && (equalTree t1 t2)
But let say I prove (eqaulTree x x = True) for all x. Then I can declare
>instance Eq a => REq (Tree a) where
> equal = equalTree
and compiler is free to try a fast pointer equality before applying the
definition of equalTree. If I hadn't defined equalTree to be reflexive,
referential transparency would have been lost. But the assumption is
that all
REq instances are reflexive. There does not seem to be an easy way to
enforce
this, but there are similar problems with Monad class, aren't there?
(Though
I admit monad laws do not appear to be as fundamental for reasoning
about
programs as referential transparency).
Viktor
