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. -- 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
