[Haskell-cafe] Proof that Haskell is RT

[Martin Sulzmann]

Correct Lennart. The below mentioned papers assume some
evidence translation of type class programs. If you need/want
a direct semantics/translation of programs you'll need to
impose some restrictions on the set of allowable type class programs.

For such an approach see

   Martin Odersky, Philip Wadler, Martin Wehr: A Second Look at 
Overloading. FPCA 1995:

Roughly, the restriction says, you can overload the argument but not the 
result (types).

- Martin


Lennart Augustsson wrote:
> 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
>>>
>>>