Adjunction models for call-by-push-value with stacks

authors: Paul Blain Levy
year: 2003
url: https://www.cs.bham.ac.uk/ pbl/papers/ctcs02journal.pdf
publisher: Elsevier BV
abstract: Call-by-push-value (CBPV) is a new paradigm, which has been claimed to provide the semantic primitives from which call-by-value and call-by-name are built. We present its operational semantics in the form of a Felleisen-Friedman style CK-machine, and see how this machine suggests a new term judgement of stacks. When augmented with this judgement, CBPV has an elegant categorical semantics based on adjunctions.We describe this categorical semantics incrementally. First, we introduce locally indexed categories and the opGrothendieck construction, and use these to give the basic structure for interpreting the 3 judgements: values, stacks and computations. Then we look at the universal property required to interpret each type constructor. We define a model to be a strong adjunction with countable coproducts, countable products and exponentials.We justify this definition in two ways. First, we see that it has a wide range of instances: we give examples for divergence, storage, erratic choice, continuations etc., in each case decomposing Moggi's strong monad into a strong adjunction.For the second justification, we start by giving equational laws for CBPV+stacks. This requires some additional pattern-matching constructs, but they do not affect the set of computations. We then show that the categories of theories and of models are equivalent.