[Haskell-cafe] Proof that Haskell is RT

[Janis Voigtlaender]

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:voigt at tcs.inf.tu-dresden.de