Dependent Effects and Call-by-Push-Value

Prerequisites. Direct starred prerequisites: none. No later core chapter depends on this route.

Let $\mathsf{read}:F\mathsf{Nat}$ be the state-reading computation of chapter 22. An ordinary monadic bind can form $$\mathsf{read}\mathsf{to}x\mathsf{in}\mathsf{return}x:F\mathsf{Nat}.$$ It cannot assign the result the family $F(\mathsf{Vec}\mathsf{Bool}x)$, because $x$ is not in scope in the type of the whole computation. Substituting the effectful term $\mathsf{read}$ into that family is worse: another read may produce another number. The defect is not missing notation. Dependency needs a stable value, whereas the operation has not yet produced one.

Three incompatible unrestricted principles

Proof of Theorem 103.3 — Fire Triangle

Proof. Write $X\leftrightarrow Y$ for the pair of functions $(X\to Y)\times (Y\to X)$, and define Leibniz equality at type $A$ by $$a{=}_{A}b:=\mathrm{\Pi }P:A\to \mathsf{U}.Pa\leftrightarrow Pb.$$ Let $t$ and $C[-]$ witness observability. Apply dependent Boolean elimination to the family $C[x]{=}_{\mathsf{B}}\mathsf{true}$. Its two branches are inhabited because both $C[\mathsf{true}]$ and $C[\mathsf{false}]$ are judgmentally true. Thus $x:\mathsf{B}⊢\star :C[x]{=}_{\mathsf{B}}\mathsf{true}$. Substitution at $t$ gives $⊢\star :C[t]{=}_{\mathsf{B}}\mathsf{true}$. Conversion along $C[t]\equiv \mathsf{false}$ gives $⊢\star :\mathsf{false}{=}_{\mathsf{B}}\mathsf{true}$.

It remains to turn that equality into an inhabitant of $\mathrm{\perp }$. The second clause of definition 103.2 builds the family $x:\mathsf{B}⊢P:\mathsf{U}$ determined by $$P[\mathsf{false}/x]\equiv \mathrm{\perp },P[\mathsf{true}/x]\equiv \mathbf{1},$$ and this is the only step that needs case analysis at the universe. Instantiating the Leibniz equality at $P$ gives $\star :\mathrm{\perp }\leftrightarrow \mathbf{1}$; applying its second component to $\mathsf{unit}:\mathbf{1}$ produces an inhabitant of $\mathrm{\perp }$. ◻

In call by value, beta substitution is restricted to values, so the first vertex is weakened. In call by name, arbitrary substitution remains, but a dependent eliminator must force the scrutinee in its classifier as well as its term; unrestricted elimination is weakened. These are exact exits from the theorem, not evaluation-order slogans.

Values and computations

Call-by-push-value prevents an effectful computation from occupying a value variable. Chapter 22 fixes the nondependent calculus; this chapter states one delta against that signature and then proves at the enlarged one.

The delta has three parts. First, the type formers $\mathrm{\Sigma }$ and $\mathrm{\Pi }$ become dependent, so a value type may mention a value variable: Second, the seven operation forms are carried over unchanged from chapter 22. Their complete typing delta is

$\mathrm{\Gamma }{⊢}^{\mathsf{c}}{\mathsf{diverge}}_{\underset{―}{B}}:\underset{―}{B}$

$\mathrm{\Gamma },z:U\underset{―}{B}{⊢}^{\mathsf{c}}M:\underset{―}{B}$

$\mathrm{\Gamma }{⊢}^{\mathsf{c}}{\mu }_z^{\underset{―}{B}}M:\underset{―}{B}$

$\mathrm{\Gamma }{⊢}^{\mathsf{c}}{\mathsf{error}}_{\underset{―}{B}}e:\underset{―}{B}$

$\mathrm{\Gamma }{⊢}^{\mathsf{c}}M:\underset{―}{B}$

$\mathrm{\Gamma }{⊢}^{\mathsf{c}}\mathsf{write}s.M:\underset{―}{B}$

$\mathrm{\Gamma }{⊢}^{\mathsf{c}}M:\underset{―}{B}$

$\mathrm{\Gamma }{⊢}^{\mathsf{c}}\mathsf{print}m.M:\underset{―}{B}$

$\{\mathrm{\Gamma }{⊢}^{\mathsf{c}}{M}_i:\underset{―}{B}{\}}_{1\le i\le n}$

$\mathrm{\Gamma }{⊢}^{\mathsf{c}}{\mathsf{choose}}_i(M_i):\underset{―}{B}$

$\{\mathrm{\Gamma }{⊢}^{\mathsf{c}}{M}_s:\underset{―}{B}{\}}_{s\in S}$

$\mathrm{\Gamma }{⊢}^{\mathsf{c}}{\mathsf{readto}}_s(M_s):\underset{―}{B}$

Here $s\in S$ ranges over a finite pointed state set, $m\in \mathcal{M}$ over a printing monoid, and $e\in E$ over errors. The annotations on divergence, recursion, and error record the computation type that their premise does not otherwise determine. Recursion unfolding is included in judgmental equality: $${\mu }_z^{\underset{―}{B}}M\equiv M[\mathsf{thunk}({\mu }_z^{\underset{―}{B}}M)/z].$$ The computation $\mathsf{read}$ of the opening is ${\mathsf{readto}}_s(\mathsf{return}s)$. Third, the sequencing rule itself changes, and that change is the subject of the chapter.

The judgments are $\mathrm{\Gamma }{⊢}^{\mathsf{v}}V:A$, $\mathrm{\Gamma }{⊢}^{\mathsf{c}}M:\underset{―}{B}$, and separate formation judgments for value and computation types. Contexts contain only value variables.

The expression $$\mathsf{return}3\mathsf{to}x\mathsf{in}\mathsf{return}(\mathsf{replicate}x\mathsf{true})$$ computes to a length-three vector. Rule Bind${}^{-}$ can type its term but cannot expose that length in the classifier of the whole computation. This is the concrete obstruction that forces the plus calculus.

For the vector computation, fix a value-type family $$\mathsf{ResultVec}:UF\mathsf{Nat}\to \mathsf{U}$$ with defining equation $$\mathsf{ResultVec}(\mathsf{tr}n)\equiv \mathsf{Vec}\mathsf{B}n.$$ Then form $$\underset{―}{B}(z):=F(\mathsf{ResultVec}(z)).$$ The family is a value-level classifier; it does not force $z$ as a computation. The result type stores $\mathsf{thunk}M$, so repeated type inspection does not rerun $M$.

Work one effectful program at that classifier. Let $S=\{0,1,2\}$ be the state set, let $$M:={\mathsf{readto}}_s(\mathsf{return}s):F\mathsf{Nat}$$ read the cell, and let $N:=\mathsf{return}(\mathsf{replicate}x\mathsf{true})$. Rule Bind${}^{+}$ types $M\mathsf{to}x\mathsf{in}N$ at $\underset{―}{B}[\mathsf{thunk}M/z]=F(\mathsf{ResultVec}(\mathsf{thunk}M))$. The postcondition genuinely depends on the returned value: in state $s$ the program returns a vector of length $s$, and the classifier names the computation that produced it rather than any one of those lengths. Nothing here forces $M$: the classifier inspects $\mathsf{thunk}M$, so type checking the program does not read the cell. What the classifier cannot do is reduce to $\mathsf{Vec}\mathsf{B}2$ in state $2$, because $\mathsf{ResultVec}$ computes only on $\mathsf{tr}n$.

Recovering it means running the machine, and that is where this program leaves the equality-preserving fragment. The transition from the state read $M$ to its selected branch $M_s$ is not a judgmental equality, so a classifier that distinguishes their thunks changes across the step. Rule Bind${}^{+}$ still types the source program. The base preservation claim cannot cover its read step; the extended claim below uses an explicit computation-type inclusion to retype the selected branch at the source read classifier. Replacing the cell by a fixed environment removes the problem and the effect together: with $M_e:=\mathsf{return}e$ under a parameter $e:E$, the classifier may name $e$ itself, no transition of the machine fires, and the first claim applies unchanged.

Sort the seven operations, and note at once that the sort does not follow intuition about which effects feel harmless. $\mathsf{error}$ is thunkable vacuously: it has no successor, so the quantification over steps is empty. Divergence is thunkable because its only successor is itself. Recursion is thunkable when its unfolding equation is included in judgmental equality. Each of $\mathsf{write}$, $\mathsf{print}$, $\mathsf{choose}$, and $\mathsf{readto}$ fails thunkability for any family that distinguishes its source thunk from the thunk of the selected successor.

The last of those deserves its own sentence, because reading looks passive. It is not. ${\mathsf{readto}}_s(M_s)$ does not compute a value from its own subterms; it selects the branch $M_s$ indexed by the state the machine happens to be in, and that state is not part of the term. Two runs of the same closed computation therefore take different transitions, so no equation of the calculus can identify ${\mathsf{readto}}_s(M_s)$ with the branch it selects. Reading is the read half of global state, and it is excluded from the first theorem below exactly as writing is.

A reader—a computation parameterized by an environment that is never written—is a different object, and it is not an effect of this calculus at all. Fix a value type $E$ of environments and use a value parameter: ${\mathrm{\Pi }}_{e:E}FA$ is an ordinary dependent computation type built from Bind${}^{-}$ and Bind${}^{+}$, its classifier may mention $e$ directly rather than a thunk, and no transition of definition 103.8 fires for it. The distinction is exactly the one Bind${}^{+}$ was introduced to make: a value already produced may be named in a type, a computation that has not run may not.

Substitution and reduction

Proof of Lemma 103.7 — Value substitution

Proof. Prove the four claims simultaneously by induction on their derivations. A variable derivation for $x$ becomes the given derivation of $V$; every other variable is unchanged. Under $\mathrm{\Sigma }$, $\mathrm{\Pi }$, and lambda binders, choose $y\notin \mathrm{FV}(V)\cup \mathrm{dom}(\mathrm{\Gamma })$ and apply the induction hypothesis to the alpha-renamed body.

For Bind${}^{+}$, write its two bound names as $x_0$, the value variable of $\mathsf{to}{x}_0\mathsf{in}$, and $z$, the thunk variable of the classifier; alpha-rename both outside $\mathrm{FV}(V)\cup \{x\}$. Substitute in the family formation premise, the computation premise, and the continuation premise. The two substitutions then commute, because no bound name of the rule occurs in $V$ and $x$ is neither $x_0$ nor $z$. Thus $$\underset{―}{B}[\mathsf{thunk}M/z][V/x]=\underset{―}{B}[V/x][\mathsf{thunk}(M[V/x])/z],$$ which is the conclusion classifier of the rebuilt rule. Return, thunk, force, ordinary bind, products, and their equations rebuild their induction hypotheses directly. Conversion substitutes into both sides of the equality derivation. These are all rule families of the displayed fragment. ◻

Subject reduction is stated for a machine rather than a term relation, because a dependent classifier is disturbed by what the surrounding stack does, not only by what the head computation does.

Proof of Lemma 103.9 — Equality-preserved classifiers

Proof. Congruence first gives $\mathsf{thunk}M\equiv \mathsf{thunk}{M}^{\prime }$. Substitution respects judgmental equality, which gives the displayed classifier equality. The force/thunk and recursion transitions are directed uses of their judgmental equations, and divergence has identical source and target, proving the three uniform claims.

No converse is asserted for an arbitrary family: a constant family cannot observe any transition. For a sensitive family, failure of the classifier equality is its defining property. A write or print step discards its outer operation, while a choice or read step selects one branch; none of these four root transitions is a judgmental equation of the selected signature. The inclusion rules in theorem 103.10 handle exactly these steps without pretending that all families distinguish them. ◻

Proof of Theorem 103.10 — Subject reduction

Proof. Fix a transition from a configuration of result type $\underset{―}{C}$, and induct on the root transition. The induction invariant retains a middle computation type $\underset{―}{B}$: before and after the transition, the head has type $\underset{―}{B}$ and the stack consumes $\underset{―}{B}$, up to the conversion rule in the first claim and up to one of the four displayed inclusions in the second claim.

For application push, inversion gives $\mathrm{\Gamma }{⊢}^{\mathsf{c}}M:{\mathrm{\Pi }}_{x:A}\underset{―}{B}$, $\mathrm{\Gamma }{⊢}^{\mathsf{v}}V:A$, and a stack consuming $\underset{―}{B}[V/x]$. Rule Arg therefore types $V::K$ as a stack consuming ${\mathrm{\Pi }}_{x:A}\underset{―}{B}$. Lambda pop uses value substitution on the premise $\mathrm{\Gamma },x:A{⊢}^{\mathsf{c}}M:\underset{―}{B}$, yielding $\mathrm{\Gamma }{⊢}^{\mathsf{c}}M[V/x]:\underset{―}{B}[V/x]$; the tail stack already consumes that type. Force/thunk contraction is typed by inversion of Force and Thunk. Divergence is a self-loop at its annotation, and recursion unfolding is typed by substituting $\mathsf{thunk}({\mu }_z^{\underset{―}{B}}M):U\underset{―}{B}$ for $z$ in the premise of Rec. An error configuration has no successor.

For sequencing push, inversion of Bind${}^{-}$ or Bind${}^{+}$ gives the head typing and the frame premise. Rule To rebuilds the stack in the minus case. In the plus case, retain the classifier family $\mathrm{\Gamma },z:UFA,{\mathrm{\Gamma }}^{\prime }⊢\underset{―}{B}(z)\mathsf{ctype}$ as part of the frame invariant. When the head reaches $\mathsf{return}V$, value substitution gives $$\mathrm{\Gamma },{\mathrm{\Gamma }}^{\prime }[\mathsf{tr}V/z]{⊢}^{\mathsf{c}}N[V/x]:\underset{―}{B}[\mathsf{tr}V/z].$$ Every intervening transition in the first claim is a directed judgmental equation: beta, force/thunk, recursion unfolding, or the divergence self-loop. Consequently $M\equiv \mathsf{return}V$, and lemma 103.9 gives $$\underset{―}{B}[\mathsf{thunk}M/z]\equiv \underset{―}{B}[\mathsf{tr}V/z].$$ Conversion therefore makes the residual head and tail stack meet at the original middle type. This proves the two sequencing roots, including the only case in which the middle type can mention the computation being run.

It remains to check the four observable roots admitted only by the second claim. Inverting Write and Print types the successor $M$ at $\underset{―}{B}[\mathsf{thunk}M/z]$; Incl-Write or Incl-Print converts that judgment to the classifier containing the discarded outer operation. Inverting Read or Choose types every branch, in particular the selected branch $M_{s^{\prime }}$ or $M_{i^{\prime }}$, and Incl-Read or Incl-Choose converts the selected classifier to the source classifier. The output and state components do not occur in typing, so their update leaves the derivation unchanged. These four roots and the pure roots listed in definition 103.8 exhaust the machine. Hence the first claim holds without the four roots, and the second holds after adding their inclusions. ◻

The exclusions are substantive. Each of the four excluded operations replaces the term by a successor that judgmental equality need not identify with it. A family sensitive in the sense of lemma 103.9 therefore has different classifiers before and after the step. A write and a print discard an outer operation; a choice and a read select a branch on information the term does not contain. The inclusion rules of the second claim repair this by giving up uniqueness of typing rather than by proving the two types equal. Thunkability, in the sense of definition 103.6, is the corresponding property of one computation and one family; it is not a theorem that all state computations are harmless.

Translations and two bounded repairs

The call-by-value translation sends a source type $A$ to a value type $A^{\mathsf{v}}$ and a term to a computation $M^{\mathsf{v}}:F{A}^{\mathsf{v}}$. A source variable remains a value, so substitution is restricted to values. The call-by-name translation sends a source type to a computation type and places assumptions under $U$; arbitrary substitution is available, while dependent elimination requires the storage/thunkability equation. Neither translation validates all three vertices of theorem 103.3.

Classical control produces another concrete failure, and it is worth printing because the repair is the same move as Bind${}^{+}$ made at a different level. Under the ordinary double-negation translation a computation of type $A$ becomes $(A^{+}\to \mathrm{\perp })\to \mathrm{\perp }$. The type of the second component of a dependent pair must then mention $\mathsf{fst}e$, a value that exists only inside a continuation and can never be returned, since the continuation’s answer type is $\mathrm{\perp }$.

A polymorphic-answer CPS translation changes the answer type from $\mathrm{\perp }$ to a variable. Its computation translation is $$A^{÷}:=\mathrm{\Pi }\alpha :\ast .(A^{+}\to \alpha )\to \alpha ,$$ so that the underlying value can be extracted by running the computation at the identity continuation: $e^{÷}{A}^{+}\mathsf{id}:A^{+}$. Two target rules make that extraction usable inside a type. The first records the value of a computation while checking a continuation,

$\mathrm{\Gamma }⊢e:\mathrm{\Pi }\alpha :\ast .(A\to \alpha )\to \alpha$$\mathrm{\Gamma }⊢B:\ast$$\mathrm{\Gamma },x=eA\mathsf{id}⊢e^{\prime }:B$

$\mathrm{\Gamma }⊢e@B(\lambda x:A.e^{\prime }):B$

and the second is the equation that justifies it, $$\mathrm{\Gamma }⊢(e_1@B(\lambda x:A.e_2))\equiv (\lambda x:A.e_2)(e_{1}A\mathsf{id}).$$ Evaluation order is explicit in T-Cont: the continuation body $e^{\prime }$ is checked under the hypothesis that $x$ already equals the value that $e$ returns, so the pair’s second component may mention it. Compare Bind${}^{+}$, which checks $N$ under a classifier mentioning $\mathsf{tr}x$ for the value $x$ that $M$ will return. Both rules buy dependency by naming the not-yet-produced value in the classifier; the source language differs, and so does what is proved. Its call-by-name and call-by-value translations preserve typing for the exact CoC-with-$\mathrm{\Pi }/\mathrm{\Sigma }$ signatures of those translations. This fact does not prove that arbitrary control operators satisfy Bind${}^{+}$.

A fibred calculus repairs the same obstruction with a different rule. It adds a computational Sigma type: from $\mathrm{\Gamma },x:A⊢\underset{―}{C}$ it forms $\mathrm{\Gamma }⊢{\mathrm{\Sigma }}_{x:A}\underset{―}{C}$, a computation type whose inhabitants package a value index with a computation in the corresponding fiber. Its introduction and elimination are $$⟨V,M{⟩}_{(x:A).\underset{―}{C}},M\mathsf{to}⟨x:A,z:\underset{―}{C}⟩\mathsf{in}K,$$ and the eliminator is typed in a third judgment $\mathrm{\Gamma }\mid z:\underset{―}{C}⊢K:\underset{―}{D}$ of homomorphism terms, in which the computation variable $z$ occurs linearly. That linearity is what fixes evaluation order: a computation bound to $z$ always runs before the rest of $K$, so eliminating $⟨V,M⟩$ runs $M$ first.

The two repairs differ in where the not-yet-produced value is named. Bind${}^{+}$ keeps one judgment and moves the dependency into the classifier through a thunk; the fibred calculus adds a judgment and moves the dependency into a linear computation variable. On the vector example the package contains $n:\mathsf{Nat}$ and a computation returning $\mathsf{Vec}\mathsf{B}n$, and no thunk appears. The rule delta has a different semantic model and donates no substitution or preservation theorem to definition 103.5.

Suggested first pass.

None of these problems is a prerequisite for a later chapter. Begin with exercise 103.3, then complete exercise 103.5.

Exercise 103.3¶

★★☆ Reconstruct the Fire Triangle proof using an identity type instead of Leibniz equality. State the eliminator used to distinguish true from false and identify the conversion that uses observability.

Referenced from 4 locations

• Dependent Effects and Call-by-Push-Value
• ch:dependent-effects: dependent effects

Exercise 103.4¶

★★★ Classify $\mathsf{error}$, $\mathsf{write}$, $\mathsf{readto}$, $\mathsf{choose}$, and a fixed-environment reader against thunkability. For each positive classification write the equation required by definition 103.6; for each negative one give a family $\underset{―}{B}(z)$ and two states, or two branches, at which the two classifiers differ. Then say which of the five are admitted by the first claim of theorem 103.10 and which need an inclusion rule, and explain why the reader is on the admitted side for a reason that has nothing to do with thunkability.

Referenced from 3 locations

• Dependent Effects and Call-by-Push-Value
• ch:dependent-effects: dependent effects

Exercise 103.5¶

★★★ Practical project.dcbpv-dependent-sequencing-checker Implement in Kappa a finite checker and evaluator for values, computations, return, thunk, force, a state read, and dependent sequencing over natural-indexed vectors. Maintain the invariant that classifiers mention only value variables or thunks admitted by Bind${}^{+}$, so that sequencing a state read yields a classifier that names the thunk rather than any one state. The named acceptance cases are $$\begin{array}{c}\mathtt{\text{return-vector-2}}\mapsto \mathtt{\text{accepted: Vec 2}},\\ \mathtt{\text{raw-effect-in-type}}\\ \mapsto \mathtt{\text{rejected: computation in value position}},\\ \mathtt{\text{force-neutral}}\mapsto \mathtt{\text{neutral computation}},\\ \mathtt{\text{readto-classifier}}\mapsto \mathtt{\text{accepted: thunked}}.\end{array}$$ A mutation that permits a raw computation in a classifier must fail the second oracle, and one that collapses a state read to a single state must fail the fourth. The checker illustrates subject reduction on a finite fragment; it does not prove the Fire Triangle or semantic soundness.

Referenced from 5 locations

• Dependent Effects and Call-by-Push-Value
• Erasure, dependent protocols, effects, specifications, and partiality: executable records
• ch:dependent-effects: dependent sequencing