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