5
$\begingroup$

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.

$\endgroup$
  • 2
    $\begingroup$ The stacks make it an abstract machine, like the Krivine abstract machine. When you define the term calculus, you have a top-level reduction but it's often not enough to define an operational semantics. For example in the lambda calculus, you need to use weak head reduction the goes under some contexts. You can think of abstract machines as the top-level reduction plus rules that explicitly "move" in the term: the left part of the configuration is the subterm you're looking at, and the stack represents the context you are under. $\endgroup$ – xavierm02 Oct 6 at 8:52
  • $\begingroup$ So it is some sort of trick to express intermediate states in operational semantics, but not needed, if for example, I was interested just in a denotational semantics? $\endgroup$ – Qhead Oct 6 at 9:10
  • $\begingroup$ It's more than a trick. It's useful for realizability. Type systems for configurations are closer to sequent calculi which have some meta-theoretic advantages over natural deduction. It makes expressing control operators easier, and probably a lot more. But I guess you could argue that all of this is related to operational semantics. $\endgroup$ – xavierm02 Oct 8 at 13:24
4
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ Interesting. But why it was not present in the original presentation of CBPV? It's because it's not needed if you're not interested in this more operational view of computations? $\endgroup$ – Qhead Oct 6 at 17:16
  • $\begingroup$ I suppose it was not there because (a) it was "just" Paul Levy's PhD thesis and there are only so many things one can squeeze out of a PhD student, and (b) it takes time for people to figure things out. $\endgroup$ – Andrej Bauer Oct 7 at 13:02
  • $\begingroup$ (c) The stacks are a very French thing, Paul is English. $\endgroup$ – Andrej Bauer Oct 7 at 13:03
  • $\begingroup$ Thanks. About (c), it's funny then that he was in France when he wrote his paper on adjunction models for CBPV with stacks (according to his affiliation). $\endgroup$ – Qhead Oct 7 at 20:12
3
$\begingroup$

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).

$\endgroup$
  • $\begingroup$ About $\eta$ for $F A$, what about for $\Gamma \vdash^{c} M : F A$, you have $M \equiv M~\mathsf{to}~x.\mathsf{return}~x$? $\endgroup$ – Qhead Oct 9 at 21:31
  • $\begingroup$ No that's not equivalent, the one I gave gives you "commuting conversions". For instance a function application should be able to be pushed into a bind: $y ` (M \textrm{ to } x. \textrm{force } x)$ should be equivalent to $M \textrm{ to } x. y ` (\textrm{force} x)$ $\endgroup$ – Max New Oct 10 at 0:08

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.