RE: [Haskell-cafe] Proof that Haskell is RT

It's possible that there's some more direct approach that represents types as some kind of runtime values, but nobody (to my knowledge) has done that.

It don't think its possible - I tried it and failed. Consider: show (f []) Where f has the semantics of id, but has either the return type [Int] or [Char] - you get different results. Without computing the types everywhere, I don't see how you can determine the precise type of []. Thanks Neil

...

On Wed, Nov 12, 2008 at 3:21 AM, Jules Bean wrote:

...

Andrew Birkett wrote:

...

Hi,

Is a formal proof that the Haskell language is

referentially transparent?

...

Many people state "haskell is RT" without backing up

On Wed, Nov 12, 2008 at 12:39 PM, Luke Palmer wrote: 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.

Haskell 98 does not seem that big to me (it's not teeny, but it's nothing like C++), yet we are continually embarrassed about not having any formal semantics. What are the challenges preventing its creation?

Luke _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

============================================================================== Please access the attached hyperlink for an important electronic communications disclaimer: http://www.credit-suisse.com/legal/en/disclaimer_email_ib.html ==============================================================================