[Haskell-cafe] "show" for functional types
Robert Dockins
robdockins at fastmail.fm
Wed Apr 5 11:25:07 EDT 2006
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
More information about the Haskell-Cafe
mailing list