[Haskell-cafe] formal semantics

[Jay Sulzberger]

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
(internal) Core.

>
>> 2. The Type Inference Subsystem, which using some constraint
>> solver calculates the type to be assigned to the value of Haskell
>> expressions.
>>
>
> 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,

Ah, thanks!

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

   http://web.archive.org/web/20060206074101/http://www.cse.ogi.edu/~mpj/thih/TypingHaskellInHaskell.html

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

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.

oo--JS.