On 12 Nov 2008, at 11:11, Andrew Birkett wrote:
Hi,
Is a formal proof that the Haskell language is referentially
transparent? Many people state "haskell is RT" without backing up
that claim. I know that, in practice, I can't write any counter-
examples but that's a bit handy-wavy. Is there a formal proof that,
for all possible haskell programs, we can replace coreferent
expressions without changing the meaning of a program?
(I was writing a blog post about the origins of the phrase
'referentially transparent' and it made me think about this)
I think the informal proof goes along the lines of "because that's
what the spec says" -- Haskell's operational semantics are not
specified in the report, only IIRC a wooly description of having some
sort of non-strict beta-reduction behavior.
Bob
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
