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 <[EMAIL PROTECTED]> wrote:
On Wed, Nov 12, 2008 at 3:21 AM, Jules Bean <[EMAIL PROTECTED]> 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@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
