[Haskell-cafe] Proof that Haskell is RT
jules at jellybean.co.uk
Wed Nov 12 05:21:45 EST 2008
Andrew Birkett wrote:
> 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.
More information about the Haskell-Cafe