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.
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Reply via email to