[Haskell-cafe] "show" for functional types
Robert Dockins
robdockins at fastmail.fm
Tue Apr 4 10:02:13 EDT 2006
On Apr 1, 2006, at 3:23 PM, Brian Hulley wrote:
> Robert Dockins wrote:
>> [snip]
>> 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).
>
> Ok I see now! :-) I was confusing the concept of referential
> transparency with a kind of global code equivalence, so the rest of
> my argument is irrelevant. Thus I should have said:
>
> " For particular types T1 and T2, if (f (x::T1))::T2 === g x for
> all x in T1 then f :: T1->T2 and g ::T1->T2 can be freely
> substituted since the context T1->T2 cannot tell them apart."
Having thought about this a bit more, I realize that this statement
is also too strong. In the lambda calculus, extensionality is
equivalent to the validity of eta-conversion (Plotkin, Call-by-value,
Call-by-name and the lambda calculus, 1975). However, in Haskell,
eta-conversion is not valid (ie, meaning-preserving). Observe:
f, g :: a -> b
f = undefined
g = \x -> undefined x
forall x::a, f x === g x === _|_. However, 'seq' can tell them apart.
seq f 'a' === _|_
seq g 'a' === 'a'
So f and g are not replaceable in all term contexts (in particular,
not in 'seq' contexts).
As I understand it, it is exactly this issue that causes some to want
'seq' to be a class member from which functions are specifically
excluded.
Rob Dockins
Speak softly and drive a Sherman tank.
Laugh hard; it's a long way to the bank.
-- TMBG
More information about the Haskell-Cafe
mailing list