[Haskell-cafe] "show" for functional types

[Robert Dockins]

On Apr 5, 2006, at 10:49 AM, Brian Hulley wrote:

> 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.

I had in mind "has the same denotational semantics", but the notation  
is a little sloppy.

On the other hand, you could turn the definition around and say that  
=== means two expression which can be freely substituted.  To prove  
properties about ===, you then need to have a very precise definition  
of the semantics of the programming language.  Unfortunately, I don't  
think Haskell's semantics are developed to quite that point.

> 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.

There is a fair bit of disagreement about what referential  
transparency means.  I found the following link after googling around  
a bit; it seems to address some of these issues.

http://www.cs.indiana.edu/~sabry/papers/purelyFunctional.ps


> Regards, Brian.


Rob Dockins

Speak softly and drive a Sherman tank.
Laugh hard; it's a long way to the bank.
           -- TMBG