ch:control-operators: ch:control-operators

Let $F_L=\mathsf{throw}[]\mathsf{to}\mathsf{cont}(K_0)$. The complete first invocation is The last step uses $K_0=\bullet ;{\mathsf{add}}_1[]$. Replacing $L$ by $L^{\prime }$ changes only the first four states: $$L^{\prime }▹\mathsf{throw}5\mathsf{to}\mathsf{cont}(K_0){⟶}^{\ast }{K}_0◃5⟶\bullet ◃6.$$ In both runs the final throw transition pattern-matches the same value $\mathsf{cont}(K_0)$, discards the current stack, and produces $K_0◃5$. Its right-hand side contains $K_0$, not a modified or consumed stack. That transition is the operational evidence that the continuation is persistent rather than one-shot.

Fix the ambient answer $R$, suppose $K:B\Rightarrow R$, and invert T-Throw to obtain ${⊢}_R{e}_1:A$, ${⊢}_R{e}_2:\mathsf{Cont}A$, and the arbitrary local result $B$. For the push step, $$\frac{K:B\Rightarrow R\mathsf{throw}[]\mathsf{to}{e}_2:A\Rightarrow B}{K;\mathsf{throw}[]\mathsf{to}{e}_2:A\Rightarrow R},$$ so the reduct evaluating $e_1:A$ is a state of result $R$.

For the first return, suppose ${⊢}_{R}v:A$. The old top frame accepts $A$ and produces $B$. The new top frame has $$\mathsf{throw}v\mathsf{to}[]:\mathsf{Cont}A\Rightarrow B$$ by the value premise $v:A$; hence $K;\mathsf{throw}v\mathsf{to}[]$ accepts the type of $e_2$ and still returns $R$.

For the final return, state typing gives $$K;\mathsf{throw}v\mathsf{to}[]:\mathsf{Cont}A\Rightarrow R,{⊢}_{R}w:\mathsf{Cont}A.$$ Canonical continuations is used exactly here: $w=\mathsf{cont}(K^{\prime })$ with $K^{\prime }:A\Rightarrow R$. Since $v:A$, the reduct $K^{\prime }◃v$ has result type $R$. The discarded stack $K$ was allowed to produce the unrelated local type $B$; the ambient subscript forces the restored stack $K^{\prime }$ to have the same final answer $R$.

Write $V=A^{\mathsf{v}}$. In the letcc clause the translated captured variable has type $c:V\to \mathbf{0}$. If $e^{\mathsf{c}}:(V\to \mathbf{0})\to \mathbf{0}$, then $$\lambda k:V\to \mathbf{0}.(e^{\mathsf{c}}[k/c])k:(V\to \mathbf{0})\to \mathbf{0}=A^{\mathsf{c}}.$$ For throw, if $e_1:A$, $e_2:\mathsf{Cont}A$, and the arbitrary source result is $B$, then $$a:V,c:V\to \mathbf{0},ca:\mathbf{0},\lambda c.ca:(V\to \mathbf{0})\to \mathbf{0}.$$ Thus $e_2^{\mathsf{c}}(\lambda c.ca):\mathbf{0}$, $\lambda a.e_2^{\mathsf{c}}(\lambda c.ca):V\to \mathbf{0}$, and $$\lambda k:B^{\mathsf{v}}\to \mathbf{0}.e_1^{\mathsf{c}}(\lambda a.e_2^{\mathsf{c}}(\lambda c.ca)):B^{\mathsf{c}}.$$ The binder $k$ is unused, matching the discarded throw site.

Here are all four machine roots; in particular this includes the three throw transitions. Capture has the marked beta step $$(\mathsf{letcc}c\mathsf{in}e{)}^{\mathsf{c}}{K}_h^{\mathsf{k}}{⟶}_{\beta }^{+}{e}^{\mathsf{c}}[K_h^{\mathsf{k}}/c]K_h^{\mathsf{k}}.$$ The initial throw push is $$(\mathsf{throw}{e}_1\mathsf{to}{e}_2{)}^{\mathsf{c}}{K}_h^{\mathsf{k}}{⟶}_{\beta }^{+}{e}_1^{\mathsf{c}}(\lambda a.e_2^{\mathsf{c}}(\lambda c.ca)).$$ Returning $v$ to the first throw frame contracts the displayed $a$: $$(\lambda a.e_2^{\mathsf{c}}(\lambda c.ca))v^{\mathsf{v}}{⟶}_{\beta }^{+}{e}_2^{\mathsf{c}}(\lambda c.c{v}^{\mathsf{v}}).$$ Finally, returning $\mathsf{cont}(K^{\prime })$ contracts $c$: $$(\lambda c.c{v}^{\mathsf{v}})K_h^{\prime }{}^{\mathsf{k}}{⟶}_{\beta }^{+}{K}_h^{\prime }{}^{\mathsf{k}}{v}^{\mathsf{v}}.$$ Each source root therefore contributes at least one target beta step.

Put $V=A^{\mathsf{v}}$ and $S=V+(V\to \mathbf{0})$. Expanding the two letcc clauses, both injections, and throw, then contracting administrative beta redexes, gives $${\mathsf{lem}}_A^{\mathsf{c}}{⟶}_{\beta }^{\ast }\lambda h:S\to \mathbf{0}.h(\mathsf{inr}(\lambda a:V.h(\mathsf{inl}a))).$$ Indeed $\lambda a.h(\mathsf{inl}a):V\to \mathbf{0}$, so the right injection has type $S$; its application to $h$ has type $\mathbf{0}$, and abstraction gives $(S\to \mathbf{0})\to \mathbf{0}$, the required type.

The outer occurrence $h(\mathsf{inr}(\lambda a.h(\mathsf{inl}a)))$ is the first call of the supplied continuation, with apparent evidence for the right summand. If a client invokes that evidence at $a:V$, the inner occurrence $h(\mathsf{inl}a)$ calls the same continuation again with evidence for the left summand. The repeated occurrence of $h$, rather than an equation between the two injections, is the CPS image of the change of mind.

With ${\mathrm{\Delta }}_0=(\gamma ::\mathsf{T})$, $\tau =\gamma$, and $\rho =\iota$, the first effect clause of theorem 35.30 is $$\alpha ::\mathsf{T}.\mathrm{\forall }\gamma ::\mathsf{T}.((\alpha \stackrel{\iota }{\to }\gamma )\stackrel{\iota }{\to }\gamma )\Rightarrow \alpha .$$ For an operation result $\alpha$, the parameter is one function which, for every chosen $\gamma$, consumes a captured continuation $\alpha \to \gamma$ and produces an answer $\gamma$. Therefore $\mathrm{\forall }\gamma$ must bind both the continuation codomain and the answer codomain. The ill-scoped alternative $(\mathrm{\forall }\gamma .\alpha \to \gamma )\to \gamma$ leaves the final $\gamma$ free; moving the quantifier only into the continuation type also allows its instantiation to disagree with the surrounding answer. Neither is the image of the well-kinded source effect.

The four rows are: In the first row the handler resumption is $\lambda z.\mathsf{handle}E[z]D$; in the second the translated operation passes $\lambda x.kxh$, so the reset/return code is retained. The second root contracts $\lambda w.Q[w]$ beneath $\lambda z$, which is precisely why only that direction needs arbitrary-context ${⟶}_i$.

In the shallow rows the captured resumption is $\lambda z.E[z]$, with no handler, reset, or return clause. Its type may expose the same leading effect, so both target effects are defined by $\mu \alpha$. Both displayed shallow root calculations contract only in evaluation position and hence use ordinary ${⟶}^{+}$.

Under $k:\mathrm{\neg }(\mathrm{\exists }x:\mathsf{Nat}.x=1)$, the leaves and pair are $$1:\mathsf{Nat},\mathsf{refl}:1=1,(1,\mathsf{refl}):\mathrm{\exists }x:\mathsf{Nat}.x=1.$$ Rule Dep-Throw-P assigns ${\mathsf{throw}}_k(1,\mathsf{refl})$ the arbitrary local result type $0=1$. Hence $$(0,{\mathsf{throw}}_k(1,\mathsf{refl})):\mathrm{\exists }x:\mathsf{Nat}.x=1,$$ and Dep-Callcc-P gives $p_0:\mathrm{\exists }x:\mathsf{Nat}.x=1$.

All three reductions, including the transformed throw, are The first step is commuting projection, the second is pair projection under number-level $\mathsf{callcc}$, and the third is vacuity. Projection gives $\mathsf{prf}{p}_0:\mathsf{wit}{p}_0=1$. Conversion along the displayed reduction gives $\mathsf{refl}:\mathsf{wit}{p}_0=0$. Taking $B(x)\equiv x=0$, Dep-Subst derives $$\mathsf{subst}(\mathsf{prf}{p}_0)\mathsf{refl}:B(1),B(1)\equiv (1=0).$$ The absent ${\lambda }_{\mathsf{K}}$ rule is the call-by-name commuting rule which moves $\mathsf{wit}([])$ through a captured continuation (together with its compatibility closure beneath number-level $\mathsf{callcc}$). The CBV stack machine has no dependent projection root of this form.

For a fresh $u$, $\lambda z.z:u\to u$. Since the surrounding context is empty, ML-Let closes this type to $i:\mathrm{\forall }u.u\to u$. Instantiating the first occurrence at $\mathsf{int}$ gives $i1:\mathsf{int}$; instantiating the second at $\mathsf{bool}$ gives $i\mathsf{true}:\mathsf{bool}$. The sequencing abbreviation discards the first result, so the displayed term has type $\mathsf{bool}$. Its right-hand side is a lambda, hence it satisfies values-only let.

For the unrestricted continuation-plugging calculation, assume that $x$ has a monotype $\tau$. Closing the type of the bound expression $x$ relative to the context $x:\tau$ quantifies no variable: every variable free in $\tau$ is already free in the context. Thus $f$ also has monotype $\tau$. Typing $f1$ forces its domain to be $\mathsf{int}$, whereas typing $f\mathsf{true}$ forces the same domain to be $\mathsf{bool}$. No monotype satisfies both constraints. With $x:\mathrm{\forall }u.u\to u$, the let can instantiate its right-hand side at a fresh $u\to u$, close that type again, and let the two occurrences of $f$ instantiate $u$ separately. Thus $K_0[x]$ is typable. The plugged expression is not a term of the values-only fragment, because its let right-hand side is a variable rather than a value; it is used only to test the unrestricted evaluator’s continuation invariant. This is precisely the gap between the monomorphic premise needed to reify the continuation and the polymorphic premise available to unrestricted let-generalization.

In $P$, the rejected node is the outer let whose right-hand side is $E=\mathsf{callcc}(\lambda k.\lambda x.\mathsf{throw}k(\lambda y.x))$: $E$ is an application, not a syntactic value. Changing the body to $f1;f1$ makes the saved continuation monomorphically typable at $\mathsf{int}\to \mathsf{int}$, but it does not change that syntactic node. The selected values-only repair rejects it nonetheless; the theorem does not perform a finer safety analysis of individual nonvalues.

Let $K_3=\bullet ;{\mathsf{add}}_3[]$. Since ${\mathsf{add}}_3[]:\mathsf{Nat}\Rightarrow \mathsf{Nat}$, $K_3:\mathsf{Nat}\Rightarrow \mathsf{Nat}$. The top frame has $[]7:(\mathsf{Nat}\to \mathsf{Nat})\Rightarrow \mathsf{Nat}$, so $$K=K_3;[]7:(\mathsf{Nat}\to \mathsf{Nat})\Rightarrow \mathsf{Nat}.$$ Writing ${\mathsf{add}}_3^{\mathsf{v}}=\lambda n.\lambda k.k(3+n)$, the stack translation is Here $a:\mathsf{Nat}$, $f:\mathsf{Nat}\to (\mathsf{Nat}\to \mathbf{0})\to \mathbf{0}$, and $(K_3{)}_h^{\mathsf{k}}:\mathsf{Nat}\to \mathbf{0}$, so every application is typed.

For $i=\lambda x.x$, the source run is $$K◃i⟶K_3;i[]▹7⟶K_3;i[]◃7⟶K_3▹7⟶K_3◃7⟶\bullet ◃10.$$ On the target side the exact typed spine is The first reductions pass $7$ to $i^{\mathsf{v}}$, then pass its result to $(K_3{)}_h^{\mathsf{k}}$, and finally compute $3+7$.

The two branches of $C$ return $A$: the left branch returns $x:A$, and T-Throw gives the right branch arbitrary result $A$ from $a:A$ and $q:\mathsf{Cont}A$. Thus $C:(A+\mathsf{Cont}A)\Rightarrow A$, and $K;C:(A+\mathsf{Cont}A)\Rightarrow R$.

Put $J=K;C$ and $J^{\prime }=J;\mathsf{inl}[]$. Splicing the two traces gives one run: The case-frame translation is $$J_h^{\mathsf{k}}=\lambda s.\mathsf{case}s\mathsf{of}\{\mathsf{inl}x\mapsto x^{\mathsf{c}}{K}_h^{\mathsf{k}};\mathsf{inr}q\mapsto (\mathsf{throw}a\mathsf{to}q{)}^{\mathsf{c}}{K}_h^{\mathsf{k}}\},$$ and the restored injection frame is $J_h^{\prime }{}^{\mathsf{k}}=\lambda b.J_h^{\mathsf{k}}(\mathsf{inl}b)$. The CPS normal form from the preceding solution first supplies $\mathsf{inr}(J_h^{\prime }{}^{\mathsf{k}})$ to $J_h^{\mathsf{k}}$; the right branch applies $J_h^{\prime }{}^{\mathsf{k}}$ to $a^{\mathsf{v}}$, after which the injection continuation calls $J_h^{\mathsf{k}}$ again with $\mathsf{inl}{a}^{\mathsf{v}}$. The left branch then calls $K_h^{\mathsf{k}}{a}^{\mathsf{v}}$, the translation of the endpoint.

Let $$D=\{f,r.fr;x.\mathsf{DH}(e_r)\},v_c=\lambda z.\mathsf{handle}\mathsf{DH}(E)[z]D.$$ Then the entire root calculation is The first contraction is legal only because $E$ is $0$-free. Translation preserves freeness, so the deep handler sees the translated operation before any nearer delimiter. The last equality uses translation of plugging and value substitution; it is not an extra reduction.

Choose a target value $u$ and define $T(s)=u$ for every source state. For each source step $s\to s^{\prime }$, one has $T(s)=u=T(s^{\prime })$, hence $T(s){\to }^{\ast }T(s^{\prime })$ by the empty target reduction. Nevertheless an infinite source run $s_0\to s_1\to \cdots$ translates to the constant sequence $u,u,\dots$, not to an infinite target reduction. Target strong normalization says nothing about repetitions joined by zero steps.

In theorem 35.13, positivity is used when the per-source-step reductions are concatenated: $$T(s_0){\to }^{+}T(s_1){\to }^{+}T(s_2){\to }^{+}\cdots .$$ Because every segment contains at least one target step, infinitely many source steps yield infinitely many target steps, contradicting target strong normalization. Replacing ${\to }^{+}$ by ${\to }^{\ast }$ invalidates exactly that inference.

Under the value-restricted grammar, $p_0$ is not a proof value: its outer constructor is $\mathsf{callcc}$. Consequently both $$\mathsf{wit}{p}_0\text{and}\mathsf{prf}{p}_0$$ are ill formed. The first was needed to commute projection through control and to convert it to $0$; the second was needed for the certificate $\mathsf{wit}{p}_0=1$. Hence the two premises of Dep-Subst cannot be assembled and this inconsistency derivation is blocked.

This syntactic observation is not a soundness theorem. A complete dependent control calculus must still define every evaluation context and conversion, prove substitution and preservation for all of them, and show that no other eliminator observes a nonvalue computation in a dependent type. The value restriction removes this counterexample; it does not supply those missing metatheoretic arguments.