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?
The (well, a natural approach to a) formal proof would be to give a
formal semantics for haskell.
Referential transparency would be an obvious property of the semantics.
Soundness would show that it carried over to the language.
Jules
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
