GHC internals

[Richard Eisenberg]

It's true that the document in GHC doesn't include operational semantics, but that's because GHC doesn't ever really implement a concrete operational semantics for Core, at least that I'm aware of. There are various places that a certain operational semantics is assumed. However, I don't think there's one place that really states the semantics in any concrete way. The goal of the document you attached is to have an easy-to-read and easy-to-maintain version of Core, with a direct connection to the implementation. With the operational semantics never stated, including those rules seemed to go against that goal.

That said, it wouldn't be hard for me to imagine an operational semantics and add it to the document -- I just don't know how I would check my imagined version against the implemented one.

Richard

On Apr 29, 2013, at 8:38 AM, Simon Peyton-Jones <simonpj at microsoft.com> wrote:

> Norman
> 
> |    - Is there anything published about the implementation of GHCi?
> |      Or perhaps something on the Developers' Wiki that explains how it works?
> 
> If you mean the details of bytecode compilation and the bytecode interpreter, I'm really not sure that there is.  That's bad; there should be. I'm ccing Simon M in case he knows of something.
> 
> |    - What is the best paper (or papers) to consult on the semantics
> |      of GHC core?
> 
> Many of these papers
> 	http://research.microsoft.com/en-us/um/people/simonpj/papers/ext-f/
> give syntax, static semantics, and operational semantics of Core. 
> 
> Moreover, Richard Eisenberg has developed a specification of the Real Core in GHC, kept in the source tree in docs/core-spec
> 
> I enclose a typeset version.  
> 
> Sadly it doesn't include operational semantics, but I don't think that'd be hard to add, would it Richard?  The papers on the above link give several versions of the operational semantics, which is largely straightforward.
> 
> Simon
> <core-spec.pdf>