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