On 28-Jul-1999, Lennart Augustsson <[EMAIL PROTECTED]> wrote:
> Fergus Henderson wrote:
>
> > equal x y = unsafePerformIO $ do
> > ptrEq <- ptrEqual x y
> > return (ptrEq || deep_equals x y)
> >
> > Note that unlike `req', `equal' here _is_ referentially transparent.
>
> No, it's not. If x and y are both bottom you can get unexpected
> results, i.e., sometimes it terminates, sometimes it doesn't.
Sorry, you're absolutely right. And the same problem arises with
exceptions too -- if x and y are both `raise "oops"' then sometimes it
returns `True' and other times it returns `raise "oops"'. Oops indeed!
I'm not sure off-hand what the best fix would be. One possible solution
would be to force evaluation of the arguments if they are equal:
equal x y = unsafePerformIO $ do
ptrEq <- ptrEqual x y
return (if ptrEq then x `hyperseq` True else deep_equals x y)
However, this compromises the nice O(1) performance in that case.
Another possible fix would be to rename `equal' as `unsafe_equal',
noting that it is referentially transparent so long as neither of its
arguments contains bottom or any exceptional value; it would then be
the programmer's responsibility to check that all callers ensure that
this condition is satisfied for all calls to `unsafe_equal'.
The second fix is probably best. But it's still rather ugly.
P.S.
I'm just glad that the same problem doesn't arise in Mercury :-)
The analagous Mercury code would be
:- type bool ---> yes ; no.
:- func equal(T, T) = bool.
:- func deep_equals(T, T) = bool.
:- pred ptr_equal(T::in, T::in, bool::out) is cc_multi.
equal(X, Y) = promise_only_solution((pred(Res::out) is cc_multi :-
ptr_equal(X, Y, PtrEq),
( PtrEq = yes, Res = yes
; Res = (if deep_equals(X, Y) then yes else no)
)
)).
In Mercury, for cases such as `equal(throw("oops"), throw("oops"))'
or `equal(loop, loop)' (where `loop' is defined by `loop = loop.'),
the declarative semantics says that the result must be `yes'. The
operational semantics, however, exhibits the same nondeterminism as
the Haskell code did. This is OK in Mercury because in Mercury
although the operational semantics is required to be sound w.r.t. the
declarative semantics, it is not required to be complete; in cases
where the declarative semantics says that the result is `yes', it may
still be acceptable for the implementation to throw an exception
rather than computing the result `yes'. In Mercury, if you want to
reason about whether your program will terminate or throw exceptions,
you need to use the operational semantics rather than the declarative
semantics.
--
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.
