See "What is a purely functional language" by Sabry. Not quite a formal proof about *Haskell*, but then we would first need a formal semantics of Haskell to be able to do that proof ;-) On 12 Nov 2008, at 10: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)
Andrew
-- - http://www.nobugs.org - _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe