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