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