[Haskell-cafe] "show" for functional types

[Brian Hulley]

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.