At the time, these uses didn't seem like a direct-enough encoding of the operational semantics to include in the writeup. There have been enough requests for operational semantics in that document that I'll put something in, probably by the end of the week -- shouldn't be hard. Richard On Apr 29, 2013, at 12:00 PM, Simon Peyton-Jones wrote:

That's not really true though. The compiler implements beta-reduction; and inlining; and directly implements the "Push" rules in exprIsConApp_maybe.

S

| -----Original Message----- | From: Richard Eisenberg [mailto:eir@cis.upenn.edu] | Sent: 29 April 2013 14:30 | To: Simon Peyton-Jones | Cc: 'Norman Ramsey'; ghc-devs@haskell.org; Simon Marlow | Subject: Re: GHC internals | | 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 | 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 | >