[Haskell-cafe] formal semantics

[Kristopher Micinski]

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