[Haskell-cafe] "show" for functional types

[Brian Hulley]

Robert Dockins wrote:
> On Saturday 01 April 2006 11:53 am, Brian Hulley wrote:
>> Claus Reinke wrote:
>>> the usual way to achieve this uses the overloading of Nums in
>>> Haskell: when you write '1' or '1+2', the meaning of those
>>> expressions depends on their types. in particular, the example
>>> above uses 'T Double', not just 'Double'.
>>
>> However there is nothing in the functions themselves that restricts
>> their use to just T Double. Thus the functions can be compared for
>> equality by supplying an argument of type T Double but used
>> elsewhere in the program with args of type (plain) Double eg:
>
> Overloaded functions instantiated at different types are not (in
> general) the same function.  If you mentally do the
> dictionary-translation, you'll see why.
>
> In particular for f, g :: XYZ a => a -> b, and types n m such that
> (XYZ n) and (XYZ m),
>
> f :: (n -> b) === g :: (n -> b)
>
> does *not* imply
>
> f :: (m -> b) === g :: (m -> b)
>
>
> That is where your argument falls down.

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). It is the inequality that is the key to breaking 
referential transparency, because the discovery of an inequality implies 
different code.

Regards, Brian.