ch:dependent-effects: dependent effects

Without $C[t]\equiv \mathsf{false}$, substitution still yields $⊢\star :C[t]{=}_{\mathsf{B}}\mathsf{true}$. The next proof line can no longer convert that judgment to $⊢\star :\mathsf{false}{=}_{\mathsf{B}}\mathsf{true}$. A diverging Boolean term supplies no judgmental equation with $\mathsf{false}$: divergence is the absence of a terminating computation, whereas conversion requires a finite equality derivation. Thus it does not restore the missing observability premise.

Let $M=\mathsf{return}2:F\mathsf{Nat}$, let $z:UF\mathsf{Nat}$, and put $\underset{―}{B}(z)=F(\mathsf{ResultVec}(z))$. Before the beta step the rule conclusion is $$\mathrm{\Gamma }{⊢}^{\mathsf{c}}M\mathsf{to}x\mathsf{in}\mathsf{return}(\mathsf{replicate}x\mathsf{true}):F(\mathsf{ResultVec}(\mathsf{thunk}M)).$$ The continuation premise is formed under $x:\mathsf{Nat}$ and has classifier $F(\mathsf{ResultVec}(\mathsf{tr}x))$. Beta reduction substitutes two and gives $$\mathsf{return}(\mathsf{replicate}2\mathsf{true}):F(\mathsf{ResultVec}(\mathsf{tr}2))\equiv F(\mathsf{Vec}\mathsf{B}2).$$ Replacing $\mathsf{thunk}M$ by $M$ is ill sorted because $\mathsf{ResultVec}$ accepts a value of type $UF\mathsf{Nat}$, while $M$ is a computation of type $F\mathsf{Nat}$.

Let ${\mathsf{Id}}_{\mathsf{B}}(b,c)$ have constructor ${\mathsf{refl}}_b:{\mathsf{Id}}_{\mathsf{B}}(b,b)$ and eliminator $J$. Dependent Boolean elimination on $x$ constructs $$x:\mathsf{B}⊢q(x):{\mathsf{Id}}_{\mathsf{B}}(C[x],\mathsf{true}),$$ because both branch classifiers reduce to ${\mathsf{Id}}_{\mathsf{B}}(\mathsf{true},\mathsf{true})$. Substitute the effectful term $t$, then use $C[t]\equiv \mathsf{false}$ to convert $q(t)$ to an identity $e:{\mathsf{Id}}_{\mathsf{B}}(\mathsf{false},\mathsf{true})$. Take the family $D(\mathsf{false})=\mathrm{\perp }$ and $D(\mathsf{true})=\mathbf{1}$. Identity elimination transports $\mathsf{unit}:D(\mathsf{true})$ along the symmetry of $e$, producing an inhabitant of $D(\mathsf{false})=\mathrm{\perp }$. The only conversion using observability is the conversion of $q(t)$’s left endpoint from $C[t]$ to $\mathsf{false}$.

Use the classifier from the chapter, $$\underset{―}{B}(z):=F(\mathsf{ResultVec}(z)),\mathsf{ResultVec}(\mathsf{tr}n)\equiv \mathsf{Vec}(\mathsf{B},n).$$ It stays stuck on the thunk of an effect operation but computes after a selected branch returns a numeral.

The computation ${\mathsf{error}}_{F\mathsf{Nat}}e$ is thunkable for every well-formed family. There is no transition ${\mathsf{error}}_{F\mathsf{Nat}}e⟶M^{\prime }$, so the required implication $${\mathsf{error}}_{F\mathsf{Nat}}e⟶M^{\prime }⟹\underset{―}{B}[\mathsf{thunk}({\mathsf{error}}_{F\mathsf{Nat}}e)/z]\equiv \underset{―}{B}[\mathsf{thunk}{M}^{\prime }/z]$$ has no instances. This is the vacuous positive case.

The other three machine operations are negative. Set $$W:=\mathsf{write}1.(\mathsf{return}0).$$ The step from store zero to store one has successor $\mathsf{return}0$. Its two classifiers have normal forms $$F(\mathsf{ResultVec}(\mathsf{thunk}W))\text{and}F(\mathsf{Vec}(\mathsf{B},0)),$$ so they are not judgmentally equal. For $R:={\mathsf{readto}}_s(\mathsf{return}s)$, stores zero and one select successors whose classifiers are respectively $F(\mathsf{Vec}(\mathsf{B},0))$ and $F(\mathsf{Vec}(\mathsf{B},1))$, while the source classifier remains the stuck form $F(\mathsf{ResultVec}(\mathsf{thunk}R))$. Finally, for $$C:={\mathsf{choose}}_i(\mathsf{return}0,\mathsf{return}1),$$ the two branches again yield the distinct vector classifiers at lengths zero and one; neither is judgmentally equal to the stuck source classifier. Thus $\mathsf{write}$, $\mathsf{readto}$, and $\mathsf{choose}$ are not thunkable for this family.

A fixed-environment reader is not an operation of definition 103.8, so thunkability has no reader transition to classify. With $e:E$ in the value context, reading is represented directly by $\mathsf{return}e$, and a classifier may mention $e$; no machine step observes or changes an environment.

The first claim of theorem 103.10 therefore admits $\mathsf{error}$, whose terminal configuration cannot violate preservation, and the fixed-environment reader, because it contributes no effect rule. The state operations $\mathsf{write}$ and $\mathsf{readto}$ require Incl-Write and Incl-Read; erratic choice requires Incl-Choose. The reader lies on the admitted side because it is a value parameter, not because a read transition satisfies a thunkability equation.