Looking for recent works on STG

[Sebastian Graf]

Hey Rodrigo,

With any kind of semantics, often the most important question is: What do
you want to achieve with it?

Generally speaking, I think it would be tedious, but not all that hard, to
define an STG-style semantics for Core that "simply" anfises on the fly.
I did that for example in my denotational interpreter for Core here
<https://gitlab.haskell.org/ghc/ghc/-/blob/64ae8fff5239b7c2c58692ce3b0e03f63f01bca1/compiler/GHC/Core/Semantics.hs#L161>,
generating a trace in a Sestoft-style small-step operational semantics.
It works quite well (until it encounters an import or a primop which I
haven't implemented), see here
<https://mastodon.online/@sgraf/111715016532134390>.
If you really insist on modelling the STG machine (the prime advantage of
which is that it can be efficiently compiled to hardware), then you would
need to figure out the manifest arity of functions before you put them in
the heap, etc..
But even that should not be hard, taking the STG operational semantics from
the eval/apply paper
<https://www.microsoft.com/en-us/research/wp-content/uploads/2016/07/eval-apply.pdf>,
which should be amenable to mechanised formalisation. It's still tedious
unless you really need to observe some STG-specific detail in your work.

So yeah, what is your end goal here?

Cheers,
Sebastian

Am So., 26. Mai 2024 um 14:03 Uhr schrieb Moritz Angermann <
moritz.angermann at gmail.com>:

> I don’t know myself, but I would suggest reaching out to Csaba. I believe
> he might have a good grasp on the STG literature.
>
> On Sun, 26 May 2024 at 7:40 PM, Rodrigo Mesquita <
> rodrigo.m.mesquita at gmail.com> wrote:
>
>> Dear all,
>>
>> Do you know of any recent works on the STG?
>>
>> In particular, I am looking for a result connecting STG's execution and
>> Core’s call-by-need semantics when written in structural operational
>> semantics style.
>>
>> Nonetheless, I’m also interested in possibly more recent formulations of
>> STG (e.g. a mechanized one?) beyond the original paper.
>>
>> Cheers
>> Rodrigo Mesquita
>> _______________________________________________
>> ghc-devs mailing list
>> ghc-devs at haskell.org
>> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
>>
> _______________________________________________
> ghc-devs mailing list
> ghc-devs at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-devs/attachments/20240526/d08e8a64/attachment.html>