[Haskell-cafe] "show" for functional types
Robert Dockins
robdockins at fastmail.fm
Sat Apr 1 13:35:40 EST 2006
[snip]
> No, it doesn't, because that wasn't my argument. Consider:
>
> f :: C a => a->a
> g :: C a => a->a
>
> Now if we can define just one instance of C, eg T1 where f (x::T1) \= g
> (x::T1), then we can tell f and g apart for all instances of C, even when
> there is another instance of C, eg T2, for which f (x::T2) == g (x::T2).
> Thus we can't just interchange the uses of f and g in the program because
> we can always use values of T1 to distinguish between uses of f :: T2 -> T2
> and g :: T2 -> T2.
> If f (x::T1) == g (x::T1) then nothing has been demonstrated, as you
> rightly point out, because there could be another instance of of C eg T3
> for which f (x::T3) \= g(x::T3).
I agree to this point.
> It is the inequality that is the key to
> breaking referential transparency, because the discovery of an inequality
> implies different code.
Here is where you make the jump that I don't follow. You appear to be
claiming that the AbsNum module coerces a Haskell compiler into breaking
referential integrity by allowing you to discover a difference between the
following two functions:
f :: (Num a) => a -> a
f x = x + 2
and
g :: (Num a) => a -> a
g x = x + 1 + 1
From an earlier post:
> > Now since f and g compute the same results for the same inputs,
> > anywhere in a program that you can use f you could just replace f
> > by g and the observable behaviour of the program would be
> > completely unaffected. This is what referential transparency means.
My essential claim is that the above statement is in error (but in a fairly
subtle way). It is only true when f and g are instantiated at appropriate
types. This is what I meant by saying that overloading was muddying the
waters. The original post did not have a type signature, so one _could_
assume that MR forced defaulting to Integer (the MR is evil, _evil_ I say),
which would then make the statement true _in that context_. However the post
with the AbsNum code instantiates f and g at a different type with different
properties, and the equality does not hold.
> Interesting! Referential transparency (as I understand it) has indeed been
> violated. Perhaps the interaction of GADTs and type classes was not
> sufficiently studied before being introduced to the language.
I believe your reasoning is correct, but you are using a false supposition.
Rob Dockins
More information about the Haskell-Cafe
mailing list