Not sure the thunk implementation at runtime for levy is correct

[mstewartgallus]

Hi,

I happened to be experimenting with using call by push value as part of a compiler IR for my own lazy functional language. I still don't really understand call by push value so I'm asking as much for my own learning but I don't think that the thunk implementation is strictly correct.

I mostly learned from this tutorial https://www.cs.bham.ac.uk/~pbl/papers/cbpvefftt.pdf . The way Levy presents his language a "thunk" at runtime doesn't actually need to be a closure necessarily. Thunk is just an arbitrary monad "T". T would be some sort of IO monad or something or some sort of operational monad like in https://apfelmus.nfshost.com/articles/operational-monad.html .

Basically, in my understanding of how call by push value is presented a thunk is more about delaying performing a side effect (of course nontermination is a side effect) than about delaying pure computation.

I feel like the implementation of Forcing is also a little off. In my understanding it is actually "Let" that executes the actual side effect. M is just a description of the actual side effect to be performed in my understanding.

Obviously you can shuffle things around a bit with the same end result but mostly I just want to clarify things for my own understanding.

Thanks

[andrejbauer]

Can you give an example which shows what's incorrect about thunk and force?

Note that we have both let and do. Your description of let sounds like what do is supposed to be doing.