Robert Dockins wrote:
On Apr 1, 2006, at 3:23 PM, Brian Hulley wrote:
[snip] " 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).
I should not have used functions, since in any case for full generality rt is about allowing equivalent expressions to be substituted eg as in: "For a particular type T, if f::T === g then f::T and g::T can be freely substituted since the context T cannot tell them apart" This of course begs the question of how === is defined and so perhaps is not that useful. If === must be defined extensionally then not all contexts in Haskell are referentially transparent since seq is referentially opaque, but this would render the whole notion of referential transparency useless for Haskell since there would be no way for a user of a library function to know whether or not the argument context(s) are transparent or opaque. At the moment I can't think of a non-extensional definition for === but there must be one around somewhere so that equational reasoning can be used. Regards, Brian.