[Haskell-cafe] Proof that Haskell is RT

[Lennart Augustsson]

I had a quick look at "Stuckey and Sulzmann, A Theory of Overloading"
and it looks to me like the semantics is given by evidence
translation.  So first you do evidence translation, and then give
semantics to the translated program.  So this looks like the two step
approach I first mentioned.
Or have I misunderstood what you're doing?

What I meant hasn't been done is a one step semantics directly in
terms of the source language.
I guess I also want it to be compositional, which I think is where
things break down.

  -- Lennart

On Wed, Nov 12, 2008 at 2:26 PM, Martin Sulzmann
<martin.sulzmann at gmail.com> wrote:
> Lennart Augustsson wrote:
>>
>> 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.
>>
>>
>
> This has been done. For example, check out the type class semantics given in
>
> Thatte, Semantics of type classes revisited, LFP '94
> Stuckey and Sulzmann, A Theory of Overloading, TOPLAS'05
>
> Harrison: A Simple Semantics for Polymorphic Recursion. APLAS 2005
> is also related I think.
>
> The ICFP'08 poster
>
> Unified Type Checking for Type Classes and Type Families , Tom Schrijvers
> and Martin Sulzmann
>
> suggests that a type-passing semantics can even be programmed by (mis)using
> type families.
>
> - Martin
>
>
>>  -- 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
>>>
>>>
>>
>> _______________________________________________
>> Haskell-Cafe mailing list
>> Haskell-Cafe at haskell.org
>> http://www.haskell.org/mailman/listinfo/haskell-cafe
>>
>