[Haskell-cafe] formal semantics

[Jay Sulzberger]

On Sat, 25 Aug 2012, Kristopher Micinski <krismicinski at gmail.com> wrote:

> On Thu, Aug 23, 2012 at 12:23 PM, Ramana Kumar
> <Ramana.Kumar at cl.cam.ac.uk> wrote:
>> Dear Haskell Cafe
>>
>> I'm looking for information on past and current attempts to write semantics
>> for Haskell.
>> Features I'm particularly interested in are:
>>
>> formal
>> mechanised
>> maintainable
>> up to date
>>
>> Of course, if nothing like that exists then partial attempts towards it
>> could still be useful.
>>
>> My ultimate aims include:
>>
>> Make it viable to define Haskell formally (i.e. so mechanised semantics can
>> take over the normative role of the Haskell reports).
>> Write a verified (or verify an existing) Haskell compiler (where verified
>> means semantics preserving).
>>
>> Cheers,
>> Ramana
>>
>
> Ramana,
>
> If you look through the Haskell reports, you'll see that the language
> is typically explained by its desugaring to a "core" language which
> has the semantics you'd "expect," in the sense that it's a call by
> need abstract machine implemented by means of graph reduction in form
> of the STG machine.
>
> Thus, you typically want to think about the semantics of "core
> Haskell," in which you might try understanding the semantics of the
> STG machine.
>
> You can certainly look at the classic article [1] that describes the
> behavior, at a high level.  You might ask whether the high level
> description of the STG machine really "makes sense," at which point
> I'd direct you to a number of other articles (the one that sticks in
> my memory, but I haven't really read deeply, is [2]).
>
> It sounds, however, that you are looking for a more full description
> of the language's semantics in a formal manner, going from "real"
> Haskell to core Haskell, I feel such a reduction must surely exist but
> I'm not sure I can recall one.
>
> If you were to write a verified compiler, you would need a semantics
> for the STG machine and show that it obeyed the rules you'd expect (a
> call by name semantics), and then compose your proof for that with
> your reduction of real Haskell to core Haskell..
>
> kris
>
> [1] "Implementing lazy functional languages on stock hardware: the
> Spineless Tagless G-machine," Simon L. Peyton Jones,
> http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.53.3729
> [2] "The Spineless Tagless G-machine, naturally," Jon Mountjoy,
> http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.13.8726

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

2. The Type Inference Subsystem, which using some constraint
solver calculates the type to be assigned to the value of Haskell
expressions.

3. The machine which does "reduction", perhaps "execution", on
the value of Haskell expressions.  This is, by your account, the
STG machine.

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.

I think I have now mostly just repeated what you said.

oo--JS.