<p>The point of stacks is that they are in a sense the <em>dual</em> concept to <em>computations</em>.</p>

<p>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 <em>stack</em>.</p>

<p>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.</p>

CC BY-SA 4.0
2019-10-06T17:16:02.920Z
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?
Qhead
CC BY-SA 4.0
2019-10-07T13:02:26.440Z
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.
Andrej Bauer
CC BY-SA 4.0
2019-10-07T13:03:01.110Z
(c) The stacks are a very French thing, Paul is English.
Andrej Bauer
CC BY-SA 4.0
2019-10-07T20:12:30.360Z
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).
Qhead
CC BY-SA 4.0
2019-10-06T15:52:22.250Z
2019-10-06T15:52:22.250Z
Andrej Bauer
<p>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.</p>

<p>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 <span class="math-container">$F$</span> type. I believe this was not
discovered initially because Levy was originally working based on
concrete denotational models rather than general categorical logic.</p>

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

<p>When looking at the models, you get that rather than describing an
effect by a strong monad <span class="math-container">$T$</span>, you describe it by a strong adjunction
<span class="math-container">$F \dashv U$</span>. What are the two categories involved? The category of
values and the category of stacks.</p>

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

<p>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 (<a href="https://guillaume.munch.name/files/duploids.pdf" rel="nofollow noreferrer">1</a>) and is shown in CBPV syntax in section 6 of (<a href="https://www.cs.bham.ac.uk/~pbl/papers/contextiso.pdf" rel="nofollow noreferrer">2</a>).</p>

CC BY-SA 4.0
2019-10-09T21:31:33.063Z
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$?
Qhead
CC BY-SA 4.0
2019-10-10T00:08:26.150Z
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)$
Max New
CC BY-SA 4.0
2019-10-09T18:22:06.813Z
2019-10-09T18:22:06.813Z
Max New
<p>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?</p>

<p>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.</p>

CC BY-SA 4.0
2019-10-06T08:52:58.490Z
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.
xavierm02
CC BY-SA 4.0
2019-10-06T09:10:48.987Z
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?
Qhead
CC BY-SA 4.0
2019-10-08T13:24:13.143Z
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.
xavierm02
<type-theory><type-systems><typed-lambda-calculus><monad>
What's the point of stack judgement in CBPV?
Qhead
# What's the point of stack judgement in CBPV?

(Asked by: username_0 on 2019-10-05)

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.

**Tags:** type-theory, type-systems, typed-lambda-calculus, monad

> **Comments:**
> **username_1**: 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.  
> **username_0**: 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?  
> **username_1**: 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.  

---

## 2 answers

### Answer by username_2 on 2019-10-06. Score: 4 | Accepted answer

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.

> **Comments:**
> **username_0**: 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?  
> **username_2**: 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.  
> **username_2**: (c) The stacks are a very French thing, Paul is English.  
> **username_0**: 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).  

---

### Answer by username_3 on 2019-10-09. Score: 3

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](https://guillaume.munch.name/files/duploids.pdf)) and is shown in CBPV syntax in section 6 of ([2](https://www.cs.bham.ac.uk/~pbl/papers/contextiso.pdf)).

> **Comments:**
> **username_0**: 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$?  
> **username_3**: 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)$  

---

