Dependent subtyping, object paths, and classical control

Dependent subtyping and refinement entailment

Dependent products compare their codomains under the client domain:

The refinement ledger uses a distinct relation. Its annotated A-normal term syntax and evaluation contexts are It reduces only by $(\lambda x:R.e)v⟶e[v/x]$ and the compatible rule $e⟶e^{\prime }\Rightarrow E[e]⟶E[e^{\prime }]$. Its base and function subtyping clauses are

$\mathrm{Entails}(\mathrm{\Phi }(\mathrm{\Gamma })\wedge {\varphi }_1,{\varphi }_2)$

Base introduction, variables, and array introduction are

$\mathrm{\Gamma }(x)=R$

$\mathrm{\Gamma }{⊢}_{\mathsf{DRef}}x:R$

$\mathrm{\Gamma }{⊢}_{\mathsf{DRef}}\{\nu :\mathsf{Int}\mid \varphi \}\mathsf{type}$$\mathrm{Entails}(\mathrm{\Phi }(\mathrm{\Gamma }),\varphi [m/\nu ])$

$\mathrm{\Gamma }{⊢}_{\mathsf{DRef}}m:\{\nu :\mathsf{Int}\mid \varphi \}$

$\mathrm{\Gamma }{⊢}_{\mathsf{DRef}}\{\nu :\mathsf{Arr}\mid \varphi \}\mathsf{type}$$\mathrm{Entails}(\mathrm{\Phi }(\mathrm{\Gamma }),\varphi [⟨m_1,\dots ,m_k⟩/\nu ])$

$\mathrm{\Gamma }{⊢}_{\mathsf{DRef}}⟨m_1,\dots ,m_k⟩:\{\nu :\mathsf{Arr}\mid \varphi \}$

Refinement abstraction, application, and subsumption are

$\mathrm{\Gamma },x:R{⊢}_{\mathsf{DRef}}e:S$

$\mathrm{\Gamma }{⊢}_{\mathsf{DRef}}\lambda x:R.e:{\mathrm{\Pi }}_{x:R}S$

$\mathrm{\Gamma }{⊢}_{\mathsf{DRef}}f:{\mathrm{\Pi }}_{x:R}S$$\mathrm{\Gamma }{⊢}_{\mathsf{DRef}}v:R$

$\mathrm{\Gamma }{⊢}_{\mathsf{DRef}}fv:S[v/x]$

$\mathrm{\Gamma }{⊢}_{\mathsf{DRef}}e:R$

$\mathrm{\Gamma }{⊢}_{\mathsf{DRef}}e:S$

For a requested difference constraint, $\mathrm{Entails}$ accepts either a replayed path of weight at most the requested bound or a replayed closed cycle whose recomputed weight is negative. A claimed weight without the corresponding contiguous edge sequence is not a certificate. A GCIC cast is a run-time term $\mathsf{cast}[B\Leftarrow A](t)$, not either subtyping judgment. A failed constructor or index test reduces to ${\mathsf{err}}_B$.

Variable-path DOT

Type selection, recursive self, and object members use

$\mathrm{\Gamma }⊢x:\{A:S..U\}$

$\mathrm{\Gamma }⊢x:\{A:S..U\}$

$\mathrm{\Gamma }⊢x:T$

$\mathrm{\Gamma }⊢x:\mu (x:T)$

$\mathrm{\Gamma }⊢x:\mu (z:T)$

$\mathrm{\Gamma }⊢x:T[x/z]$

$\mathrm{\Gamma }⊢x:\{a:T\}$

$\mathrm{\Gamma }⊢x.a:T$

An inert recursive object type has pairwise distinct fields and only tight members $\{A:T..T\}$. Tight selection replaces the two general rules by

$\mathrm{\Gamma }{⊢}_{!}x:\{A:T..T\}$

$\mathrm{\Gamma }{⊢}_{!}x:\{A:T..T\}$

Concrete type definitions are tight by construction:

$\mathrm{\Gamma }⊢T\mathsf{type}$

$\mathrm{\Gamma }⊢\{A=T\}:\{A:T..T\}$

Stable paths and pDOT

Stable paths are variables and immutable field paths:

$x:T\in \mathrm{\Gamma }$

$\mathrm{\Gamma }⊢x\mathsf{path}$

$\mathrm{\Gamma }⊢p:\{a:T\}$

$\mathrm{\Gamma }⊢p.a\mathsf{path}$

Singletons propagate only toward a typeable target prefix:

$\mathrm{\Gamma }⊢p:q.\mathsf{type}$$\mathrm{\Gamma }⊢q:T$

$\mathrm{\Gamma }⊢p:T$

$\mathrm{\Gamma }⊢p:q.\mathsf{type}$$\mathrm{\Gamma }⊢q.a\mathsf{path}$

$\mathrm{\Gamma }⊢p.a:q.a.\mathsf{type}$

One-occurrence replacement is formation-indexed. The path-prefix relation checks every complete changed prefix:

$\mathrm{\Gamma }⊢q\mathsf{path}$

$\mathrm{\Gamma }⊢\mathrm{RPath}(p,p,q,q)$

$\mathrm{\Gamma }⊢\mathrm{RPath}(r,p,q,r^{\prime })$$\mathrm{\Gamma }⊢r^{\prime }.a\mathsf{path}$

$\mathrm{\Gamma }⊢\mathrm{RPath}(r.a,p,q,r^{\prime }.a)$

The selected leaf is also formed after replacement:

$\mathrm{\Gamma }⊢\mathrm{RPath}(r,p,q,r^{\prime })$$\mathrm{\Gamma }⊢r^{\prime }.A\mathsf{type}$

$\mathrm{\Gamma }⊢\mathrm{Replace}(r.A,p,q,r^{\prime }.A)$

$\mathrm{\Gamma }⊢\mathrm{RPath}(r,p,q,r^{\prime })$$\mathrm{\Gamma }⊢r^{\prime }.\mathsf{type}\mathsf{type}$

$\mathrm{\Gamma }⊢\mathrm{Replace}(r.\mathsf{type},p,q,r^{\prime }.\mathsf{type})$

Structural replacement descends through exactly one field, member bound, or intersection component. For function domains it checks the unchanged codomain under the replaced domain; for function codomains and recursive self types it alpha-renames the binder away from the two paths and checks the target codomain or recursive type. One-occurrence replacement is then bidirectional at subtyping:

$\mathrm{\Gamma }⊢p:q.\mathsf{type}$$\mathrm{\Gamma }⊢q\mathsf{path}$$\mathrm{\Gamma }⊢\mathrm{Replace}(T,p,q,U)$

$\mathrm{\Gamma }⊢p:q.\mathsf{type}$$\mathrm{\Gamma }⊢p\mathsf{path}$$\mathrm{\Gamma }⊢\mathrm{Replace}(T,q,p,U)$

Nested initialization substitutes the installed path for inner self and requires a tight record:

$p.a;\mathrm{\Gamma }⊢d[p.a/y]:T[p.a/y]$$\mathrm{TightRecord}(T)$

$p;\mathrm{\Gamma }⊢\{a=\nu (y:T)d\}:\{a:\mu (y:T)\}$

The body premise can be derived only after every path in $d[p.a/y]$ and $T[p.a/y]$ passes the path-formation rules. The source rule has no third path premise. Path lookup follows immutable stored fields; it is separate from term reduction.

Proof-dependent classical control

Proofs, left contexts, and commands have the three regular judgments $\mathrm{\Gamma }⊢p:A\mid \mathrm{\Delta }$, $\mathrm{\Gamma }\mid e:A⊢\mathrm{\Delta }$, and $c:(\mathrm{\Gamma }⊢\mathrm{\Delta })$. Regular judgments carry no dependency list. Their control core is

$\mathrm{\Gamma }⊢p:A\mid \mathrm{\Delta }$$\mathrm{\Gamma }\mid e:A⊢\mathrm{\Delta }$

$⟨p\parallel e⟩:(\mathrm{\Gamma }⊢\mathrm{\Delta })$

$c:(\mathrm{\Gamma }⊢\alpha :A,\mathrm{\Delta })$

$\mathrm{\Gamma }⊢\mu \alpha .c:A\mid \mathrm{\Delta }$

$c:(\mathrm{\Gamma },a:A⊢\mathrm{\Delta })$

$\mathrm{\Gamma }\mid \tilde{\mu }a.c:A⊢\mathrm{\Delta }$

Dependent products use

$\mathrm{\Gamma },a:A⊢p:B\mid \mathrm{\Delta }$

$\mathrm{\Gamma }⊢\lambda a.p:\mathrm{\Pi }a:A.B\mid \mathrm{\Delta }$

$\mathrm{\Gamma }⊢q:A\mid \mathrm{\Delta }$$\mathrm{\Gamma }\mid e:B[q/a]⊢\mathrm{\Delta }$$q\notin \mathrm{NEF}⟹a\notin \mathsf{FV}(B)$

$\mathrm{\Gamma }\mid q\cdot e:\mathrm{\Pi }a:A.B⊢\mathrm{\Delta }$

Thus a proof outside NEF is permitted only when the codomain is independent of the proof variable. The complete mutually generated fragment used here is Here $\star$ is the single continuation local to the fragment; it is not the calculus continuation $\widehat{\mathsf{tp}}$. Thus $\mu \star .c_N$ is admitted only with a command and context generated by the two displayed clauses. An ordinary $\mu \alpha .c$ proof and an application spine are rejected, while variables, lambdas, positive pairs, reflexivity, and the displayed delimited $\mu \star$ form are admitted. The principal roots are $$⟨V\parallel \tilde{\mu }a.c⟩⟶c[V/a],⟨\mu \alpha .c\parallel e⟩⟶c[e/\alpha ].$$ The dependent mode alone carries a list $\sigma ::=ϵ\mid \sigma \{r\mid q\}$. Formula compatibility is Its judgments are $\mathrm{\Gamma }\mid e:A{⊢}_d\mathrm{\Delta },\widehat{\mathsf{tp}}:B;\sigma$ and $c:(\mathrm{\Gamma }{⊢}_d\mathrm{\Delta },\widehat{\mathsf{tp}}:B;\sigma )$. The bridge rules include

$c:(\mathrm{\Gamma }{⊢}_d\mathrm{\Delta },\widehat{\mathsf{tp}}:A;ϵ)$

$\mathrm{\Gamma }⊢\mu \widehat{\mathsf{tp}}.c:A\mid \mathrm{\Delta }$

$\mathrm{\Gamma }⊢p:A\mid \mathrm{\Delta }$$\mathrm{\Gamma }\mid e:A{⊢}_d\mathrm{\Delta },\widehat{\mathsf{tp}}:B;\sigma \{\cdot \mid p\}$

$⟨p\parallel e⟩:(\mathrm{\Gamma }{⊢}_d\mathrm{\Delta },\widehat{\mathsf{tp}}:B;\sigma )$

The proof premise of Cut-$d$ is regular. The dependent context uses the open list entry to reconcile its formula with the regular proof’s formula. The distinguished continuation $\widehat{\mathsf{tp}}$ freezes the enclosing context while that dependency is open.

Graded erasure: additional formation, equality, usage, and dynamics

Together with the graded-erasure card immediately above, the rules below record the noninherited part of the signature in definition 101.2, definition 101.3, definition 101.4, definition 101.5, definition 101.9. Appendix A does not repeat the binder, congruence, and constructor schemas displayed in those definitions; those point-of-use displays are the complete signature.

$⊢ϵ$

$x_0:A[\uparrow ]\in \mathrm{\Gamma }.A$

$x_i:A\in \mathrm{\Gamma }$

$x_{i+1}:A[\uparrow ]\in \mathrm{\Gamma }.B$

$\mathrm{\Gamma }⊢A:\mathsf{U}$

$\mathrm{\Gamma }⊢A$

$\mathrm{\Gamma }.A⊢B$

$\mathrm{\Gamma }⊢{\mathrm{\Pi }}_p^{q}AB$

$\mathrm{\Gamma }.A⊢B$

$\mathrm{\Gamma }⊢{\mathrm{\Sigma }}_k^{q}AB$

$⊢\mathrm{\Gamma }$

$\mathrm{\Gamma }⊢\mathsf{N}:\mathsf{U}$

$⊢\mathrm{\Gamma }$

$\mathrm{\Gamma }⊢\mathrm{\perp }:\mathsf{U}$

$\mathrm{\Gamma }⊢A:\mathsf{U}$$\mathrm{\Gamma }.A⊢B:\mathsf{U}$

$\mathrm{\Gamma }⊢{\mathrm{\Pi }}_p^{q}AB:\mathsf{U}$

$\mathrm{\Gamma }⊢A:\mathsf{U}$$\mathrm{\Gamma }.A⊢B:\mathsf{U}$

$\mathrm{\Gamma }⊢{\mathrm{\Sigma }}_k^{q}AB:\mathsf{U}$

$\mathrm{\Gamma }.{\mathrm{\Sigma }}_{\otimes }^{q^{\prime }}AB⊢C$$\mathrm{\Gamma }⊢t:{\mathrm{\Sigma }}_{\otimes }^{q^{\prime }}AB$$\mathrm{\Gamma }.A.B⊢u:C[{\uparrow }^2,(x_1,x_0{)}_{\otimes }]$

$\mathrm{\Gamma }⊢{\mathsf{prodrec}}_r^q(C;t;u):C[t]$

$\mathrm{\Gamma }⊢A$$\mathrm{\Gamma }⊢t:\mathrm{\perp }$

$\mathrm{\Gamma }⊢{\mathsf{emptyrec}}^p(A;t):A$

$\mathrm{\Gamma }⊢z:A[\mathsf{zero}]$$\mathrm{\Gamma }.\mathsf{N}.A⊢s:A[{\uparrow }^2,\mathsf{suc}{x}_1]$$\mathrm{\Gamma }⊢n:\mathsf{N}$

$\mathrm{\Gamma }⊢{\mathsf{natrec}}_{p,r}^q(A;z;s;n):A[n]$

$\mathrm{\Gamma }⊢A=B:\mathsf{U}$

$\mathrm{\Gamma }⊢A=B$

$\mathrm{\Gamma }⊢A$

$\mathrm{\Gamma }⊢A=A$

$\mathrm{\Gamma }⊢A=B$

$\mathrm{\Gamma }⊢B=A$

$\mathrm{\Gamma }⊢A=B$$\mathrm{\Gamma }⊢B=C$

$\mathrm{\Gamma }⊢A=C$

$\mathrm{\Gamma }⊢A=A^{\prime }$$\mathrm{\Gamma }.A⊢B=B^{\prime }$

$\mathrm{\Gamma }⊢{\mathrm{\Pi }}_p^{q}AB={\mathrm{\Pi }}_p^q{A}^{\prime }{B}^{\prime }$

$\mathrm{\Gamma }⊢A=A^{\prime }$$\mathrm{\Gamma }.A⊢B=B^{\prime }$

$\mathrm{\Gamma }⊢{\mathrm{\Sigma }}_k^{q}AB={\mathrm{\Sigma }}_k^q{A}^{\prime }{B}^{\prime }$

$\mathrm{\Gamma }⊢t:A$

$\mathrm{\Gamma }⊢t=t:A$

$\mathrm{\Gamma }⊢A$$\mathrm{\Gamma }⊢t=u:A$

$\mathrm{\Gamma }⊢u=t:A$

$\mathrm{\Gamma }⊢t=u:A$$\mathrm{\Gamma }⊢u=v:A$

$\mathrm{\Gamma }⊢t=v:A$

$\mathrm{\Gamma }⊢t=u:A$$\mathrm{\Gamma }⊢A=B$

$\mathrm{\Gamma }⊢t=u:B$

$\mathrm{\Gamma }⊢A=A^{\prime }:\mathsf{U}$$\mathrm{\Gamma }.A⊢B=B^{\prime }:\mathsf{U}$

$\mathrm{\Gamma }⊢{\mathrm{\Pi }}_p^{q}AB={\mathrm{\Pi }}_p^q{A}^{\prime }{B}^{\prime }:\mathsf{U}$

$\mathrm{\Gamma }⊢A=A^{\prime }:\mathsf{U}$$\mathrm{\Gamma }.A⊢B=B^{\prime }:\mathsf{U}$

$\mathrm{\Gamma }⊢{\mathrm{\Sigma }}_k^{q}AB={\mathrm{\Sigma }}_k^q{A}^{\prime }{B}^{\prime }:\mathsf{U}$

$\mathrm{\Gamma }⊢t=t^{\prime }:{\mathrm{\Pi }}_p^{q}AB$$\mathrm{\Gamma }⊢u=u^{\prime }:A$

$\mathrm{\Gamma }⊢t{}^{p}u=t^{\prime }{}^p{u}^{\prime }:B[u]$

$\mathrm{\Gamma }.A⊢B$$\mathrm{\Gamma }.A⊢t:B$$\mathrm{\Gamma }⊢u:A$

$\mathrm{\Gamma }⊢({\lambda }^{p}t){}^{p}u=t[u]:B[u]$

$\mathrm{\Gamma }.A⊢B$$\mathrm{\Gamma }⊢t:{\mathrm{\Pi }}_p^{q}AB$$\mathrm{\Gamma }⊢u:{\mathrm{\Pi }}_p^{q}AB$$\mathrm{\Gamma }.A⊢t[\uparrow ]{}^p{x}_0=u[\uparrow ]{}^p{x}_0:B$

$\mathrm{\Gamma }⊢t=u:{\mathrm{\Pi }}_p^{q}AB$

$\mathrm{\Gamma }.A⊢B$$\mathrm{\Gamma }⊢t:A$$\mathrm{\Gamma }⊢u:B[t]$

$\mathrm{\Gamma }.A⊢B$

$\mathrm{\Gamma }⊢\mathsf{fst}t=\mathsf{fst}u:A$

$\mathrm{\Gamma }.A⊢B$$\mathrm{\Gamma }⊢t:A$$\mathrm{\Gamma }⊢u:B[t]$

$\mathrm{\Gamma }.A⊢B$

$\mathrm{\Gamma }⊢\mathsf{snd}t=\mathsf{snd}u:B[\mathsf{fst}t]$

$\mathrm{\Gamma }.A⊢B$$\mathrm{\Gamma }⊢\mathsf{fst}t=\mathsf{fst}u:A$$\mathrm{\Gamma }⊢\mathsf{snd}t=\mathsf{snd}u:B[\mathsf{fst}t]$

$\mathrm{\Gamma }.A⊢B$$\mathrm{\Gamma }⊢t=t^{\prime }:A$$\mathrm{\Gamma }⊢u=u^{\prime }:B[t]$

$\mathrm{\Gamma }⊢(t,u{)}_k=(t^{\prime },u^{\prime }{)}_k:{\mathrm{\Sigma }}_k^{q}AB$

$\mathrm{\Gamma }.{\mathrm{\Sigma }}_{\otimes }^{q^{\prime }}AB⊢C$$\mathrm{\Gamma }⊢t:A$$\mathrm{\Gamma }⊢t^{\prime }:B[t]$$\mathrm{\Gamma }.A.B⊢u:C[{\uparrow }^2,(x_1,x_0{)}_{\otimes }]$

$\mathrm{\Gamma }⊢{\mathsf{prodrec}}_r^q(C;(t,t^{\prime }{)}_{\otimes };u)=u[t,t^{\prime }]:C[(t,t^{\prime }{)}_{\otimes }]$

$\mathrm{\Gamma }.{\mathrm{\Sigma }}_{\otimes }^{q^{\prime }}AB⊢C=C^{\prime }$$\mathrm{\Gamma }⊢t=t^{\prime }:{\mathrm{\Sigma }}_{\otimes }^{q^{\prime }}AB$$\mathrm{\Gamma }.A.B⊢u=u^{\prime }:C[{\uparrow }^2,(x_1,x_0{)}_{\otimes }]$

$\mathrm{\Gamma }⊢{\mathsf{prodrec}}_r^q(C;t;u)={\mathsf{prodrec}}_r^q(C^{\prime };t^{\prime };u^{\prime }):C[t]$

$\mathrm{\Gamma }⊢z:A[\mathsf{zero}]$$\mathrm{\Gamma }.\mathsf{N}.A⊢s:A[{\uparrow }^2,\mathsf{suc}{x}_1]$

$\mathrm{\Gamma }⊢{\mathsf{natrec}}_{p,r}^q(A;z;s;\mathsf{zero})=z:A[\mathsf{zero}]$

$\mathrm{\Gamma }⊢z:A[\mathsf{zero}]$$\mathrm{\Gamma }.\mathsf{N}.A⊢s:A[{\uparrow }^2,\mathsf{suc}{x}_1]$$\mathrm{\Gamma }⊢n:\mathsf{N}$

$\mathrm{\Gamma }⊢{\mathsf{natrec}}_{p,r}^q(A;z;s;\mathsf{suc}n)=s[n,{\mathsf{natrec}}_{p,r}^q(A;z;s;n)]:A[\mathsf{suc}n]$

$\mathrm{\Gamma }⊢t=u:\mathsf{N}$

$\mathrm{\Gamma }⊢\mathsf{suc}t=\mathsf{suc}u:\mathsf{N}$

$\mathrm{\Gamma }.\mathsf{N}⊢A=A^{\prime }$$\mathrm{\Gamma }⊢z=z^{\prime }:A[\mathsf{zero}]$$\mathrm{\Gamma }.\mathsf{N}.A⊢s=s^{\prime }:A[{\uparrow }^2,\mathsf{suc}{x}_1]$$\mathrm{\Gamma }⊢n=n^{\prime }:\mathsf{N}$

$\mathrm{\Gamma }⊢{\mathsf{natrec}}_{p,r}^q(A;z;s;n)={\mathsf{natrec}}_{p,r}^q(A^{\prime };z^{\prime };s^{\prime };n^{\prime }):A[n]$

$\mathrm{\Gamma }⊢A=B$$\mathrm{\Gamma }⊢t=u:\mathrm{\perp }$

$\mathrm{\Gamma }⊢{\mathsf{emptyrec}}^p(A;t)={\mathsf{emptyrec}}^p(B;u):A$

$0▸\mathsf{U}$

$0▸\mathsf{zero}$

$\gamma ▸t$$\delta ▸u$

$\gamma +\delta ▸(t,u{)}_{\otimes }$

$\gamma ▸t$$\delta ▸u$

$\gamma ▸t$

$\gamma ▸\mathsf{fst}t$

$\gamma ▸t$

$\gamma ▸\mathsf{snd}t$

$\gamma ▸t$

$\gamma ▸\mathsf{suc}t$

$\gamma ▸t$$\delta ,r,r▸u$$\eta ,q▸C$$\mathsf{Prodrec}(r)$

$r\gamma +\delta ▸{\mathsf{prodrec}}_r^q(C;t;u)$

$\gamma ▸t$$\delta ▸A$$\mathsf{Emptyrec}(p)$

$p\gamma ▸{\mathsf{emptyrec}}^p(A;t)$

$\gamma ▸t$$\delta \le \gamma$

$\delta ▸t$

$\mathrm{\Gamma }⊢t⟶u:A$$\mathrm{\Gamma }⊢A=B$

$\mathrm{\Gamma }⊢t⟶u:B$

$\mathrm{\Gamma }.A⊢B$$\mathrm{\Gamma }.A⊢t:B$$\mathrm{\Gamma }⊢u:A$

$\mathrm{\Gamma }⊢({\lambda }^{p}t){}^{p}u⟶t[u]:B[u]$

$\mathrm{\Gamma }.A⊢B$

$\mathrm{\Gamma }⊢\mathsf{fst}t⟶\mathsf{fst}{t}^{\prime }:A$

$\mathrm{\Gamma }.A⊢B$$\mathrm{\Gamma }⊢t:A$$\mathrm{\Gamma }⊢u:B[t]$

$\mathrm{\Gamma }.A⊢B$

$\mathrm{\Gamma }⊢\mathsf{snd}t⟶\mathsf{snd}{t}^{\prime }:B[\mathsf{fst}t]$

$\mathrm{\Gamma }.A⊢B$$\mathrm{\Gamma }⊢t:A$$\mathrm{\Gamma }⊢u:B[t]$

$\mathrm{\Gamma }⊢t⟶t^{\prime }:{\mathrm{\Sigma }}_{\otimes }^{q^{\prime }}AB$$\mathrm{\Gamma }.{\mathrm{\Sigma }}_{\otimes }^{q^{\prime }}AB⊢C$$\mathrm{\Gamma }.A.B⊢u:C[{\uparrow }^2,(x_1,x_0{)}_{\otimes }]$

$\mathrm{\Gamma }⊢{\mathsf{prodrec}}_r^q(C;t;u)⟶{\mathsf{prodrec}}_r^q(C;t^{\prime };u):C[t]$

$\mathrm{\Gamma }.{\mathrm{\Sigma }}_{\otimes }^{q^{\prime }}AB⊢C$$\mathrm{\Gamma }⊢t_1:A$$\mathrm{\Gamma }⊢t_2:B[t_1]$$\mathrm{\Gamma }.A.B⊢u:C[{\uparrow }^2,(x_1,x_0{)}_{\otimes }]$

$\mathrm{\Gamma }⊢{\mathsf{prodrec}}_r^q(C;(t_1,t_2{)}_{\otimes };u)⟶u[t_1,t_2]:C[(t_1,t_2{)}_{\otimes }]$

$\mathrm{\Gamma }⊢n⟶n^{\prime }:\mathsf{N}$$\mathrm{\Gamma }⊢z:A[\mathsf{zero}]$$\mathrm{\Gamma }.\mathsf{N}.A⊢s:A[{\uparrow }^2,\mathsf{suc}{x}_1]$

$\mathrm{\Gamma }⊢{\mathsf{natrec}}_{p,r}^q(A;z;s;n)⟶{\mathsf{natrec}}_{p,r}^q(A;z;s;n^{\prime }):A[n]$

$\mathrm{\Gamma }⊢z:A[\mathsf{zero}]$$\mathrm{\Gamma }.\mathsf{N}.A⊢s:A[{\uparrow }^2,\mathsf{suc}{x}_1]$

$\mathrm{\Gamma }⊢{\mathsf{natrec}}_{p,r}^q(A;z;s;\mathsf{zero})⟶z:A[\mathsf{zero}]$

$\mathrm{\Gamma }⊢z:A[\mathsf{zero}]$$\mathrm{\Gamma }.\mathsf{N}.A⊢s:A[{\uparrow }^2,\mathsf{suc}{x}_1]$$\mathrm{\Gamma }⊢n:\mathsf{N}$

$\mathrm{\Gamma }⊢{\mathsf{natrec}}_{p,r}^q(A;z;s;\mathsf{suc}n)⟶s[n,{\mathsf{natrec}}_{p,r}^q(A;z;s;n)]:A[\mathsf{suc}n]$

$\mathrm{\Gamma }⊢A$$\mathrm{\Gamma }⊢t⟶t^{\prime }:\mathrm{\perp }$

$\mathrm{\Gamma }⊢{\mathsf{emptyrec}}^p(A;t)⟶{\mathsf{emptyrec}}^p(A;t^{\prime }):A$

$(\lambda v)w⟶v[w]$

$v⟶v^{\prime }$

$vw⟶v^{\prime }w$

$v⟶v^{\prime }$

$\mathsf{fst}v⟶\mathsf{fst}{v}^{\prime }$

$\mathsf{fst}(v,w)⟶v$

$\mathsf{snd}(v,w)⟶w$

$v⟶v^{\prime }$

$\mathsf{snd}v⟶\mathsf{snd}{v}^{\prime }$

$v⟶v^{\prime }$

$\mathsf{prodrec}(v;w)⟶\mathsf{prodrec}(v^{\prime };w)$

$\mathsf{prodrec}((v,v^{\prime });w)⟶w[v,v^{\prime }]$

$\mathsf{natrec}(z;s;\mathsf{zero})⟶z$

$v⟶v^{\prime }$

$\mathsf{natrec}(z;s;v)⟶\mathsf{natrec}(z;s;v^{\prime })$

$\mathsf{natrec}(z;s;\mathsf{suc}v)⟶s[v,\mathsf{natrec}(z;s;v)]$

Dependent sessions: additional base-rule delta

The quantifier and functional-passing rules are printed in the dependent session card above. The propositions-as-sessions rules are inherited from subappendix A.61; the seven rules below are the additional base rules used by definition 102.1. Thus every omitted rule has one named earlier card rather than an implicit premise.

$\mathrm{\Psi };\mathrm{\Gamma };\cdot ⟹\mathbf{0}::z:\mathbf{1}$

$\mathrm{\Psi };\mathrm{\Gamma };\mathrm{\Delta }⟹P::z:C$

$\mathrm{\Psi };\mathrm{\Gamma };\mathrm{\Delta },x:\mathbf{1}⟹P::z:C$

$\mathrm{\Psi };\mathrm{\Gamma };\mathrm{\Delta },x:A⟹P::z:B$

$\mathrm{\Psi };\mathrm{\Gamma };\mathrm{\Delta }⟹z(x).P::z:A⊸B$

$\mathrm{\Psi };\mathrm{\Gamma };{\mathrm{\Delta }}_1⟹P::y:A$$\mathrm{\Psi };\mathrm{\Gamma };{\mathrm{\Delta }}_2,x:B⟹Q::z:C$

$\mathrm{\Psi };\mathrm{\Gamma };{\mathrm{\Delta }}_1,{\mathrm{\Delta }}_2,x:A⊸B⟹(\nu y)x⟨y⟩.(P\mid Q)::z:C$

$\mathrm{\Psi };\mathrm{\Gamma };\cdot ⟹P::y:A$

$\mathrm{\Psi };\mathrm{\Gamma };\cdot ⟹!z(y).P::z:!A$

$\mathrm{\Psi };\mathrm{\Gamma },u:A;\mathrm{\Delta }⟹P::z:C$

$\mathrm{\Psi };\mathrm{\Gamma };\mathrm{\Delta },x:!A⟹P[x/u]::z:C$

$\mathrm{\Psi };\mathrm{\Gamma };\cdot ⟹P::x:A$$\mathrm{\Psi };\mathrm{\Gamma },u:A;\mathrm{\Delta }⟹Q::z:C$

$\mathrm{\Psi };\mathrm{\Gamma };\mathrm{\Delta }⟹(\nu u)((!u(x).P)\mid Q)::z:C$

Dependent effects: additional operation and inclusion delta

The value/computation boundary and both bind rules are printed in the card above. The following rules supplement the point-of-use operation, stack, and machine signatures in definition 103.4, definition 103.8. Those definitions display the complete transition relation; this card does not duplicate every constructor-preserving machine frame.

$\mathrm{\Gamma },x:\mathsf{B}⊢A:\mathsf{U}$$\mathrm{\Gamma }⊢\star :A[\mathsf{true}/x]$$\mathrm{\Gamma }⊢\star :A[\mathsf{false}/x]$

$\mathrm{\Gamma },x:\mathsf{B}⊢\star :A$

$\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{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 };\underset{―}{C}{⊢}^{\mathsf{k}}\mathsf{nil}:\underset{―}{C}$

$\mathrm{\Gamma }{⊢}^{\mathsf{v}}V:A$$\mathrm{\Gamma };\underset{―}{B}[V/x]{⊢}^{\mathsf{k}}K:\underset{―}{C}$

$\mathrm{\Gamma };{\mathrm{\Pi }}_{x:A}\underset{―}{B}{⊢}^{\mathsf{k}}V::K:\underset{―}{C}$

$\mathrm{\Gamma }{⊢}^{\mathsf{c}}N:\underset{―}{B}[\mathsf{thunk}M/z]$

$\mathrm{\Gamma }{⊢}^{\mathsf{c}}N:\underset{―}{B}[\mathsf{thunk}(\mathsf{write}s.M)/z]$

$\mathrm{\Gamma }{⊢}^{\mathsf{c}}N:\underset{―}{B}[\mathsf{thunk}{M}_{s^{\prime }}/z]$

$\mathrm{\Gamma }{⊢}^{\mathsf{c}}N:\underset{―}{B}[\mathsf{thunk}({\mathsf{readto}}_s(M_s))/z]$

$\mathrm{\Gamma }{⊢}^{\mathsf{c}}N:\underset{―}{B}[\mathsf{thunk}M/z]$

$\mathrm{\Gamma }{⊢}^{\mathsf{c}}N:\underset{―}{B}[\mathsf{thunk}(\mathsf{print}m.M)/z]$

$\mathrm{\Gamma }{⊢}^{\mathsf{c}}N:\underset{―}{B}[\mathsf{thunk}{M}_{i^{\prime }}/z]$

$\mathrm{\Gamma }{⊢}^{\mathsf{c}}N:\underset{―}{B}[\mathsf{thunk}({\mathsf{choose}}_i(M_i))/z]$

Weakest preconditions: execution rules

The transformer equations and WP-Return, WP-Bind, and WP-Sub are printed in the preceding card. These are the two additional execution rules of definition 104.6.

$\mathrm{\Gamma }⊢e:\mathsf{Pure}Aw$$\mathrm{\Gamma }⊢\mathrm{\exists }p.w(p)$

$\mathrm{\Gamma }⊢\mathsf{run}e:\mathsf{Tot}A$

$\mathsf{run}(\mathsf{Pure}\mathsf{.}\mathsf{return}v)⟶v$

Dependent subtyping: additional algorithmic rule delta

The declarative product, refinement, and cast rules are printed in the card above. The following formation and bidirectional rules form the algorithmic delta of definition 106.1, definition 106.4; the complete rule families remain displayed at those definitions.

$\mathrm{\Gamma }⊢A:\mathcal{U}$$\mathrm{\Gamma },x:A⊢B:\mathcal{U}$

$\mathrm{\Gamma }⊢{\mathrm{\Pi }}_{x:A}B:\mathcal{U}$

$\mathrm{\Gamma },x:A⊢M:B$

$\mathrm{\Gamma }⊢\lambda x:A.M:{\mathrm{\Pi }}_{x:A}B$

$\mathrm{\Gamma }⊢F:{\mathrm{\Pi }}_{x:A}B$$\mathrm{\Gamma }⊢N:A$

$\mathrm{\Gamma }⊢FN:B[N/x]$

$\mathrm{fv}(\varphi )\subseteq \mathrm{dom}(\mathrm{\Gamma })\cup \{\nu \}$$\mathrm{\Gamma }⊢\mathsf{vertices}(\varphi )\mathsf{well}\text{-}\mathsf{sorted}$

$\mathrm{\Gamma }{⊢}_{\mathsf{DRef}}\{\nu :B\mid \varphi \}\mathsf{type}$

$\mathrm{\Gamma }{⊢}_{\mathsf{DRef}}R\mathsf{type}$$\mathrm{\Gamma },x:R{⊢}_{\mathsf{DRef}}S\mathsf{type}$

$\mathrm{\Gamma }{⊢}_{\mathsf{DRef}}{\mathrm{\Pi }}_{x:R}S\mathsf{type}$

$\mathrm{\Gamma }{⊢}_{\mathsf{DRef}}m\Rightarrow [m{]}_{\mathsf{Int}}$

$\mathrm{\Gamma }{⊢}_{\mathsf{DRef}}R\mathsf{type}$$\mathrm{\Gamma },x:R{⊢}_{\mathsf{DRef}}e\Rightarrow S$

$\mathrm{\Gamma }{⊢}_{\mathsf{DRef}}\lambda x:R.e\Rightarrow {\mathrm{\Pi }}_{x:R}S$

$\mathrm{\Gamma }{⊢}_{\mathsf{DRef}}e\Rightarrow {\mathrm{\Pi }}_{x:R}S$$\mathrm{\Gamma }{⊢}_{\mathsf{DRef}}v\Leftarrow R$

$\mathrm{\Gamma }{⊢}_{\mathsf{DRef}}ev\Rightarrow S[v/x]$

$\mathrm{\Gamma }{⊢}_{\mathsf{DRef}}e\Rightarrow R$

$\mathrm{\Gamma }{⊢}_{\mathsf{DRef}}e\Leftarrow S$

Dependent object types: additional structural rule delta

The selection, recursive-self, field, and tight-member rules are printed in the object-type card above. The following structural and definition rules supplement the complete point-of-use family in definition 107.2; this card does not duplicate its application, let, and evaluation-context schemas.

$\mathrm{\Gamma },x:T⊢d:T$

$\mathrm{\Gamma }⊢\nu (x:T)d:\mu (x:T)$

$\mathrm{\Gamma }⊢t:T$

$\mathrm{\Gamma }⊢\{a=t\}:\{a:T\}$

$\mathrm{\Gamma }⊢d_1:T_1$$\mathrm{\Gamma }⊢d_2:T_2$$\mathrm{dom}(d_1)\cap \mathrm{dom}(d_2)=\varnothing$

$\mathrm{\Gamma }⊢d_1\wedge d_2:T_1\wedge T_2$

Fully path-dependent types: additional replacement and lookup delta

The stable-path, singleton, replacement-leaf, and nested-initialization rules are printed in the pDOT card above. The following rules complete the named replacement descent and lookup deltas; all unchanged DOT rules are inherited from definition 107.2.

$\mathrm{\Gamma }⊢q\mathsf{path}$

$p;\mathrm{\Gamma }⊢\{a=q\}:\{a:q.\mathsf{type}\}$

$\mathrm{\Gamma }⊢\mathrm{Replace}(S,p,q,S^{\prime })$

$\mathrm{\Gamma }⊢\mathrm{Replace}(\{a:S\},p,q,\{a:S^{\prime }\})$

$\mathrm{\Gamma }⊢\mathrm{Replace}(S,p,q,S^{\prime })$

$\mathrm{\Gamma }⊢\mathrm{Replace}(\{A:S..U\},p,q,\{A:S^{\prime }..U\})$

$\mathrm{\Gamma }⊢\mathrm{Replace}(U,p,q,U^{\prime })$

$\mathrm{\Gamma }⊢\mathrm{Replace}(\{A:S..U\},p,q,\{A:S..U^{\prime }\})$

$\mathrm{\Gamma }⊢\mathrm{Replace}(S,p,q,S^{\prime })$

$\mathrm{\Gamma }⊢\mathrm{Replace}(S\wedge U,p,q,S^{\prime }\wedge U)$

$\mathrm{\Gamma }⊢\mathrm{Replace}(U,p,q,U^{\prime })$

$\mathrm{\Gamma }⊢\mathrm{Replace}(S\wedge U,p,q,S\wedge U^{\prime })$

$\mathrm{\Gamma }⊢\mathrm{Replace}(S,p,q,S^{\prime })$$\mathrm{\Gamma },x:S^{\prime }⊢U\mathsf{type}$

$\mathrm{\Gamma }⊢\mathrm{Replace}(\mathrm{\forall }(x:S)U,p,q,\mathrm{\forall }(x:S^{\prime })U)$

$\mathrm{\Gamma },x:S⊢\mathrm{Replace}(U,p,q,U^{\prime })$$x\notin \mathrm{fv}(p)\cup \mathrm{fv}(q)$

$\mathrm{\Gamma }⊢\mathrm{Replace}(\mathrm{\forall }(x:S)U,p,q,\mathrm{\forall }(x:S)U^{\prime })$

$\mathrm{\Gamma },x:\mu (x:T)⊢\mathrm{Replace}(T,p,q,T^{\prime })$$\mathrm{\Gamma }⊢\mu (x:T^{\prime })\mathsf{type}$$x\notin \mathrm{fv}(p)\cup \mathrm{fv}(q)$

$\mathrm{\Gamma }⊢\mathrm{Replace}(\mu (x:T),p,q,\mu (x:T^{\prime }))$

$\gamma (x)=v$

${\mathrm{Lookup}}_{\gamma }(x)=v$

${\mathrm{Lookup}}_{\gamma }(p)=\nu (z:T)(d_1\wedge \{a=s\}\wedge d_2)$

${\mathrm{Lookup}}_{\gamma }(p.a)=s[p/z]$

${\mathrm{Lookup}}_{\gamma }(p)=q$

${\mathrm{Lookup}}_{\gamma }(p.a)=q.a$

Proof-dependent classical control: additional dependent rule delta

The cut, control, dependent-product, NEF, and dependency-list rules are printed in the classical-control card above. The following rules form the distinctive delta of definition 109.1, definition 109.4; the ordinary positive and equality schemas remain at those point-of-use definitions.

$\mathrm{\Gamma }⊢t:\mathbb{N}$$\mathrm{\Gamma }⊢p:A[t/x]\mid \mathrm{\Delta }$

$\mathrm{\Gamma }⊢(t,p):\mathrm{\exists }x:\mathbb{N}.A\mid \mathrm{\Delta }$

$\mathrm{\Gamma }⊢p:\mathrm{\exists }x:\mathbb{N}.A\mid \mathrm{\Delta }$$p\in \mathcal{D}$

$\mathrm{\Gamma }⊢\mathrm{wit}(p):\mathbb{N}$

$\mathrm{\Gamma }⊢p:\mathrm{\exists }x:\mathbb{N}.A\mid \mathrm{\Delta }$$p\in \mathcal{D}$

$\mathrm{\Gamma }⊢\mathrm{prf}(p):A[\mathrm{wit}(p)/x]\mid \mathrm{\Delta }$

$B\in A_{\sigma }$

$\mathrm{\Gamma }\mid \widehat{\mathsf{tp}}:A{⊢}_d\mathrm{\Delta },\widehat{\mathsf{tp}}:B;\sigma \{\cdot \mid p\}$

$c:(\mathrm{\Gamma },a:A{⊢}_d\mathrm{\Delta },\widehat{\mathsf{tp}}:B;\sigma \{a\mid p\})$

$\mathrm{\Gamma }\mid \tilde{\mu }a.c:A{⊢}_d\mathrm{\Delta },\widehat{\mathsf{tp}}:B;\sigma \{\cdot \mid p\}$

$\mathrm{\Gamma }\mid {\mathrm{abort}}_{\alpha }:\mathrm{\perp }⊢\alpha :P,\mathrm{\Delta }$