[Haskell-cafe] Proof that Haskell is RT
martin.sulzmann at gmail.com
Wed Nov 12 09:26:50 EST 2008
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.
> -- 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:
>>>> 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
>> Haskell-Cafe mailing list
>> Haskell-Cafe at haskell.org
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
More information about the Haskell-Cafe