[Haskell-cafe] Proof that Haskell is RT

Janis Voigtlaender voigt at tcs.inf.tu-dresden.de
Wed Nov 12 05:21:32 EST 2008

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

More information about the Haskell-Cafe mailing list