What is this call-by-push-value thing that everybody's talking about?
It's a calculus that combines functional and imperative behaviour in a subtle way.
I am researching the semantics of MyLang. Is call-by-push-value relevant to my research?
If MyLang contains both
then CBPV is definitely relevant to your research.
- higher-order functions, and
- some computational effect, such as divergence (as in PCF) or control operators (as in lambda-mu calculus)
It's an empirical fact that semantics of such languages exhibit CBPV structure. Once you're familiar with CBPV, you'll notice it everywhere.
Amazing! Give me some examples, please.
Domains, games, continuations, possible worlds, models of nondeterminism. Operational semantics too.
Does this apply to semantics of call-by-value languages, or call-by-name?Both. There is a decomposition of call-by-value into call-by-push-value that you can see in all these semantics of call-by-value languages. And likewise for call-by-name.
What is the CBPV decomposition of functionspace?
- The call-by-name functionspace is decomposed into UA -> B.
- The call-by-value functionspace is decomposed into U(A -> FB).
But linear logic has taught me to decompose call-by-name functionspace into !A -o B. That is present in some models but not others (e.g. Hyland-Ong game semantics). Whereas the CBPV decomposition is ubiquitous.
And monads have taught me to decompose call-by-value functionspace into A -> TB.
That is suited to some models, but makes others more complicated (e.g. possible world semantics). Whereas the CBPV decomposition is evident even in these models.
CBPV looks very similar to monad calculi of Moggi and Filinski. These were a major influence on the theory of CBPV. The main difference is that CBPV distinguishes a computation from its thunk, which is a value. The distinction is very noticeable in some models, such as possible world semantics. Another difference is that CBPV decomposes the monad into an adjunction.
CBPV looks very similar to Laurent's LLP. The main difference is that all models of LLP are continuation models, whereas CBPV has many other models. Furthermore, in game semantics, the LLP connectives ! and ? relate to Opponent/Player labelling, whereas the CBPV connectives U and F relate to Question/Answer labelling.
Is CBPV a metalanguage?You can certainly use CBPV as a metalanguage. It's ideal for writing both domain equations and predomain equations (and that cannot be done in any of the monad calculi usually employed). Moreover, your equations can then be interpreted in many different models.
On the other hand, CBPV can also be studied as an object language. Because it is so fine-grain, each semantic definition is simpler than those for call-by-name or call-by-value.
So I should give MyLang a miss, and study CBPV instead? Science is reductionism. Once the fine structure has been exposed, why ignore it?
But I like call-by-name, because its categorical semantics is so easy.That belief is a consequence of a longstanding bias (going back to Church) towards functionspace, at the expense of other connectives. Try formulating a categorical semantics for sum type in call-by-name, or even for boolean type. You'll soon see that CBPV is easier.
Where can I learn more?The best place is my book; please email me for more information on this. Also my papers.
I have lots more questions. Then email me.