[Haskell-cafe] Proof that Haskell is RT

[Jules Bean]

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