[Haskell-cafe] Proof that Haskell is RT

[Martin Sulzmann]

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
>