[Haskell-cafe] "show" for functional types

[Robert Dockins]

[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