Re: [Haskell-cafe] formal semantics

On Sat, 25 Aug 2012, Kristopher Micinski wrote:

On Thu, Aug 23, 2012 at 12:23 PM, Ramana Kumar 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.