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
<[EMAIL PROTECTED]> 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 <[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
