[Haskell-cafe] Proof that Haskell is RT

[Thomas Davie]

On 12 Nov 2008, at 11:11, 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)

I think the informal proof goes along the lines of "because that's  
what the spec says" -- Haskell's operational semantics are not  
specified in the report, only IIRC a wooly description of having some  
sort of non-strict beta-reduction behavior.

Bob