[Haskell-cafe] "show" for functional types
brianh at metamilk.com
Wed Apr 5 10:49:05 EDT 2006
Robert Dockins wrote:
> On Apr 1, 2006, at 3:23 PM, Brian Hulley wrote:
>> " 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
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.
More information about the Haskell-Cafe