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)
Answering this question, or actually even formalizing the statement you want to prove, is more or less equivalent to writing down a full denotational candidate semantics for Haskell in a compositional style, and proving that it is equivalent to the *actual* semantics of Haskell Nobody has done this. Well, there is no *actual* semantics anywhere around to which you one could prove equivalence. So, to be precise, the question you are interested in cannot even really be asked at the moment. Ciao, Janis. -- Dr. Janis Voigtlaender http://wwwtcs.inf.tu-dresden.de/~voigt/ mailto:voigt@tcs.inf.tu-dresden.de