[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
http://wwwtcs.inf.tu-dresden.de/~voigt/
mailto:voigt at tcs.inf.tu-dresden.de
More information about the Haskell-Cafe
mailing list