[Haskell-cafe] Proof that Haskell is RT

[Lennart Augustsson]

You can't write a straightforward dynamic semantics (in, say,
denotational style) for Haskell.
The problem is that with type classes you need to know the types
compute the values.
You could use a two step approach: first make a static semantics that
does type inference/checking and translates Haskell into a different
form that has resolved all overloading.
And, secondly, you can write a dynamic semantics for that language.

But since the semantics has to have the type inference engine inside
it, it's going to be a pain.

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.

  -- Lennart

On Wed, Nov 12, 2008 at 12:39 PM, Luke Palmer <lrpalmer at gmail.com> wrote:
> On Wed, Nov 12, 2008 at 3:21 AM, Jules Bean <jules at jellybean.co.uk> 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 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 at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>