[Haskell-cafe] formal semantics
jays at panix.com
Sat Aug 25 21:38:57 CEST 2012
On Sat, 25 Aug 2012, Kristopher Micinski <krismicinski at gmail.com> wrote:
>> I do not know Haskell. It looks to me as though there are
>> several pieces of the mechanism:
>> 1. There is, once the extensions are specified, a particular Type
>> System, that is, a formal system with, on the syntactic side, at
>> least, assumptions, judgements, rules of inference, terms lying
>> in some lambda calculus, etc..
> That's right. Extensions get complex too, however, and can't be
> necessarily easily dismissed (not to imply you were doing so),
> RankNTypes, for example,
I suspected that some of these extensions might cause Haskell
expressions to be hard to type. One thing I am not clear on is
whether any standard extensions require modifications to
>> 2. The Type Inference Subsystem, which using some constraint
>> solver calculates the type to be assigned to the value of Haskell
> Yes, that's right, for core haskell this is typically damas milner
> (let bound) polymorphism
Ah, yes, thank you. I almost believe in Hindley-Damas-Milner but
have not yet attempted the standard initiation course.
>> 3. The machine which does "reduction", perhaps "execution", on
>> the value of Haskell expressions. This is, by your account, the
>> STG machine.
> Yes, notably graph reduction allows sharing, which is an important
> part of Haskell's semantics,
>> There is a textual version of Haskell's Core. If it were
>> executable and the runtime were solid and very simple and clear
>> in its design, I think we would have something close to a "formal
>> semantics". We'd also require that the translation to STG code
>> be very simple.
> Yes, that's right. The translation to STG (or something like it,
> another core language) can be found in many books and articles,
This is good. I will look at the references given in this
thread. The account at
is, I think, one part of what I was looking for.
> But others here have also specified some good references for
> executable versions of Core. Still unsure if the translation from
> Haskell to Core has been verified, I would suspect not, as I haven't
> heard of any such thing.
This part of the project I am less interested in, due to my fear,
I am an old Lisper, that the luxuriant syntactic undergrowth
might be hard to hack through. If we had an executable Core,
which might have to be extended (after perhaps some subtraction)
with a simple notation for type annotations, and the rest of the
apparatus, I think this would be very useful. Even though we
would not gain one of the claimed advantages of
rigor-all-the-way, that is, better bug suppression for ordinary
Haskell as she is spoke.
More information about the Haskell-Cafe