What's the point of stack judgement in CBPV?

Question

Call-by-push-value (CBPV) introduces two main families of types, values and computations, and their corresponding judgements. However, in some extensions/variants/adaptation of CBPV, there is a third judgement: stacks. What is the purpose of this judgement? Why it was not present in the original CBPV? What do we gain when we introduce them?

The kind of extensions I am talking about are for example Levy's CBPV with stacks, or Egger et al.'s Enriched Effect Calculus, or the calculus in Ahman et al.'s Dependent Types and Fibred Computational Effects.

Answer 1

The point of stacks is that they are in a sense the dual concept to computations.

A computation does not run in a vacuum. It is always "surrounded" by some sort of an environment, or evaluation context, telling us what the current "state of progress" is, or is recording "where we are, and where we're going". Often this sort of information has stack-like behavior, so we can call it simply a stack.

The duality between computations and stacks can be made quite precise and is useful in formalizing and discovering various mathematical aspects of computation. I am not sure where you're expecting a more technical answer, but that's the gist of it.

Answer 2

Since Andrej has somewhat covered the operational side, I'll take the more semantic/category theoretic perspective of why we care about stacks, that is especially relevant in EEC.

The general philosophy of categorical logic is that all types should be defined by a universal property. In CBPV without stacks, you cannot give a universal property to the $F$ type. I believe this was not discovered initially because Levy was originally working based on concrete denotational models rather than general categorical logic.

To see what I mean, let's consider the universal property of the thunk type constructor $U$, which is that the sets of computations $\Gamma \vdash M : B$ are naturally isomorphic to the sets of values $\Gamma \vdash V : UB$. This is essentially what is encoded by the intro/elim and $\beta\eta$ equations for $U$. Now what's the universal property of the $F$ type constructor? It turns out that it says that sets of computations $\Gamma,x:A \vdash M : B$ are naturally isomorphic to the sets of stacks $\Gamma | F A \vdash S : B$. In particular, I don't know how you can state the $\eta$ principle for $F$ without using stacks, which says that for any stack $\Gamma|F A \vdash S : B$ that $$S \equiv \bullet \textrm{ to } x. S[\textrm{return } x]$$ which might also be written as saying for any such $S$ and $\Gamma \vdash M : F A$ that $$S[M] \equiv M \textrm{ to } x. S[\textrm{return } x]$$ I know from experience, that you need this rule frequently when proving program equivalences where computations use the $F$ type.

When looking at the models, you get that rather than describing an effect by a strong monad $T$, you describe it by a strong adjunction $F \dashv U$. What are the two categories involved? The category of values and the category of stacks.

Stacks become even more important when you move to the setting of enriched effect calculus. There they are written as terms $\Gamma | \Delta \vdash t : B$ which are typed with a non-empty stoup $\Delta$. In EEC, we need the stacks to describe the universal properties of types like the tensor product $!A \otimes B$ (which generalizes $F A$), the linear function space $B \multimap B'$ (which generalizes $U B'$) and the computation sum types $0, \oplus$. The stuff by Ahman extends EEC and includes these connectives as well.

Finally, a bit of semantic intuition for what a stack is. We can think of values as "total" functions between value types, and we can think of stacks as "linear" functions between computation types. This can be formalized in the idea of "thunkable" terms, which are computations that "act like" values and "linear" terms which are computations that "act like" stacks. This idea was introduced by Guillaume Munch-Maccagnoni (1) and is shown in CBPV syntax in section 6 of (2).