ch:existential-types: ch:existential-types

Let $$M(c):=\mathrm{\forall }a::\mathsf{Ty}.\mathrm{\forall }b::\mathsf{Ty}.(a\to b)\to ca\to cb.$$ The kinding calculation in the context $c::\mathsf{Ty}\to \mathsf{Ty},a::\mathsf{Ty},b::\mathsf{Ty}$ gives $ca,cb::\mathsf{Ty}$ by K-App; K-Arr forms the three arrows, and two uses of K-All give $$c::\mathsf{Ty}\to \mathsf{Ty}⊢M(c)::\mathsf{Ty}.$$ Thus the existential body has precisely the kind required by T-Pack. The complete final rule is $$\frac{\begin{array}{c}\cdot ⊢\mathsf{P}::\mathsf{Ty}\to \mathsf{Ty}\\ c::\mathsf{Ty}\to \mathsf{Ty}⊢M(c)::\mathsf{Ty}\\ \cdot ;\cdot ⊢\mathsf{dmap}:M(\mathsf{P})\end{array}}{\cdot ;\cdot ⊢\mathsf{pack}[\mathsf{P},\mathsf{dmap}]\mathsf{as}\mathrm{\exists }c::\mathsf{Ty}\to \mathsf{Ty}.M(c):\mathsf{Mapper}}\mathrm{T}-\mathrm{Pack}.$$ The third premise is the previously derived typing $\mathsf{dmap}:\mathsf{Map}\mathsf{P}$, since $M(\mathsf{P})=\mathsf{Map}\mathsf{P}$ after unfolding the abbreviation.

If the witness is replaced by $\mathbb{N}$, the first premise would have to be $$\cdot ⊢\mathbb{N}::\mathsf{Ty}\to \mathsf{Ty}.$$ Kinding instead uniquely gives $\cdot ⊢\mathbb{N}::\mathsf{Ty}$. The first premise therefore fails before a payload is considered: $\mathbb{N}$ is a type, whereas this package hides a unary type constructor that can be applied to $a$ and $b$.

Define $$\mathsf{reseal}:=\lambda c:\mathsf{Counter}.\mathsf{unpack}[X,z]=c\mathsf{in}\mathsf{pack}[X,z]\mathsf{as}\mathsf{Counter}.$$ In the unpacking body, $$X::\mathsf{Ty};z:X\times ((X\to X)\times (X\to \mathbb{N})).$$ Rule T-Pack uses witness $X$ and the variable premise for $z$, producing the outer type $\mathsf{Counter}$. That result type is formed in the empty kind context: $X$ occurs only beneath the existential binder of $\mathsf{Counter}$. Hence T-Unpack discharges the local $X$, and T-Lam gives $\mathsf{reseal}:\mathsf{Counter}\to \mathsf{Counter}$.

Inversion of the unpacking judgment supplies a kind $\kappa$, a body constructor $A$, and the three premises $$\begin{array}{c}\mathrm{\Delta };\mathrm{\Gamma },y:D⊢p:\mathrm{\exists }u::\kappa .A,\\ \mathrm{\Delta },u::\kappa ;\mathrm{\Gamma },y:D,x:A⊢e:B,\\ \mathrm{\Delta }⊢B::\mathsf{Ty}.\end{array}$$ The binders have been chosen fresh for $d$. Term substitution in the scrutinee gives the first required transformed premise $$\begin{array}{}\text{(}1\text{)}& \mathrm{\Delta };\mathrm{\Gamma }⊢p[d/y]:\mathrm{\exists }u::\kappa .A.\end{array}$$ To substitute in the body, first use constructor-context weakening on the given derivation of $d$: $$\begin{array}{}\text{(}2\text{)}& \mathrm{\Delta },u::\kappa ;\mathrm{\Gamma }⊢d:D.\end{array}$$ This is the exact use of weakening under the hidden constructor. Applying term substitution to the body derivation, with $x:A$ in its trailing context, gives the second transformed premise $$\begin{array}{}\text{(}3\text{)}& \mathrm{\Delta },u::\kappa ;\mathrm{\Gamma },x:A⊢e[d/y]:B.\end{array}$$ Equivalently, one may weaken (2) through $x:A$ inside the variable case of that substitution induction. Neither $A$ nor $B$ changes because term substitution does not act on constructors.

The old no-escape premise still forms $B$ outside $u$. Reassembling (1), (3), and that premise gives $$\frac{\begin{array}{c}\mathrm{\Delta };\mathrm{\Gamma }⊢p[d/y]:\mathrm{\exists }u::\kappa .A\\ \mathrm{\Delta },u::\kappa ;\mathrm{\Gamma },x:A⊢e[d/y]:B\\ \mathrm{\Delta }⊢B::\mathsf{Ty}\end{array}}{\mathrm{\Delta };\mathrm{\Gamma }⊢\mathsf{unpack}[u,x]=p[d/y]\mathsf{in}e[d/y]:B}\mathrm{T}-\mathrm{Unpack}.$$ Capture-avoiding substitution identifies the subject in the conclusion with $(\mathsf{unpack}[u,x]=p\mathsf{in}e)[d/y]$.

Put $$q_N^{+2}:=(\mathsf{0},(s_N^{+2},r_N)),C_N^{+2}:=\mathsf{pack}[\mathbb{N},q_N^{+2}]\mathsf{as}\mathsf{Counter}.$$ Here $s_N^{+2}=\lambda n:\mathbb{N}.\mathsf{suc}(\mathsf{suc}(n))$, so the ordinary product and arrow rules type the payload at $\mathbb{N}\times ((\mathbb{N}\to \mathbb{N})\times (\mathbb{N}\to \mathbb{N}))$; T-Pack gives $C_N^{+2}:\mathsf{Counter}$.

Write $q=q_N^{+2}$, $s=s_N^{+2}$, and $r=r_N$. Expanding every projection, the complete call-by-value contraction sequence is The first step is the outer term beta contraction, the second opens the package, the next projection steps expose $r$, the two copies of $s$, and $\mathsf{0}$, the next two term-beta steps advance by two each, and the final term-beta step applies the identity observer. The result is the normal numeral four. The same typed client applied to $C_N$ has the normal result two; constructor injectivity makes the two numeral normal forms distinct. Thus the common existential type enforces opacity but does not equate these two implementations.

Constructor reduction gives $$\mathsf{Comp}\mathsf{P}\mathsf{P}{=}_{\beta }\lambda a::\mathsf{Ty}.\mathsf{P}(\mathsf{P}a).$$ Apply the abstraction/action clause to $Q=(A_0,A_1,R)$. It first yields $$[[\mathsf{P}(\mathsf{P}a){]]}_{a\mapsto Q}.$$ The outer application clause applies the action of $\mathsf{P}$ to the relational object denoted by $\mathsf{P}a$. By a second application clause, followed by the product clause, $$[[\mathsf{P}a{]]}_{a\mapsto Q}=[[\mathsf{P}{]]}_{\varnothing }(A_0,A_1,R)=R\times R.$$ The endpoints of that intermediate object are $A_0\times A_0$ and $A_1\times A_1$. Applying the outer $\mathsf{P}$ action and unfolding its product body once more gives This relation has endpoint types $$(A_0\times A_0)\times (A_0\times A_0),(A_1\times A_1)\times (A_1\times A_1),$$ exactly the two constructor endpoints of $\mathsf{Comp}\mathsf{P}\mathsf{P}$ applied to $A_0$ and $A_1$. For the nonconstant action, $$[[\mathsf{D}{]]}_{\varnothing }(A_0,A_1,R)=[[a\to a{]]}_{a\mapsto (A_0,A_1,R)}=R\Rightarrow R.$$ Changing $R$ while keeping $A_0,A_1$ fixed changes which function pairs the arrow lifting relates. Thus an arrow-kind relational object must carry an action on the relation argument, not only a pair of endpoint constructors.

The initial states satisfy $$i_P^{+}=(\mathsf{0},\mathsf{suc}(\mathsf{0})),$$ so $[i_N]R^{+}[i_P^{+}]$. If $[n]R^{+}[p]$, then $p{=}_{\beta }(n,\mathsf{suc}(n))$, whence $$s_P^{+}p{=}_{\beta }(\mathsf{suc}(n),\mathsf{suc}(\mathsf{suc}(n))).$$ This is exactly the witness for $[s_{N}n]R^{+}[s_P^{+}p]$. The observer calculation is $$r_P^{+}p{=}_{\beta }n{=}_{\beta }{r}_{N}n.$$ Thus the three payload components are related at $$R^{+}\times ((R^{+}\Rightarrow R^{+})\times (R^{+}\Rightarrow {\mathsf{Eq}}_{\mathbb{N}})).$$ Existential lifting relates $C_N$ and $C_P^{+}$. The single use of self-parametricity relates a closed $k:\mathsf{Counter}\to \mathbb{N}$ to itself at $[[\mathsf{Counter}]]\Rightarrow {\mathsf{Eq}}_{\mathbb{N}}$; applying it to the packages gives $k{C}_N{=}_{\beta }k{C}_P^{+}$.

The unknown-remainder display requires a row kind $\mathsf{Row}$, a row extension constructor $\{\ell :A\mid \xi \}$, and a lacks judgment $\xi \mathrm{\backslash }\ell$; none belongs to the fixed-record extension.

Rules Rec-E and T-Lam give $$\mathsf{portOf}:\{\mathsf{port}:\mathbb{N}\}\to \mathbb{N},$$ while Rec-I gives $$\mathsf{server}:\{\mathsf{port}:\mathbb{N},\mathsf{secure}:{\mathsf{Bool}}_F\}.$$ At their application, T-App demands the smaller record type for the argument. The two sorted record types are distinct normal constructors, so T-Conv cannot supply it. Adding Width and Sub derives and then Now T-App gives $\mathsf{portOf}\mathsf{server}:\mathbb{N}$ from the displayed domain and argument judgments. Width and Sub add no row kind, extension constructor, or lacks predicate, so the first display remains unformed.

Let $$A(X):=X\times ((X\to X)\times (X\to \mathbb{N})).$$ The Church encoding of $C_N$ is $$\mathsf{c}{C}_N:=\mathrm{\Lambda }R::\mathsf{Ty}.\lambda k:\mathrm{\forall }X::\mathsf{Ty}.A(X)\to R.k[\mathbb{N}]q_N.$$ The witness premise $\mathbb{N}::\mathsf{Ty}$ and the payload typing $q_N:A(\mathbb{N})$ show $$\mathsf{c}{C}_N:{\mathsf{Some}}_{\mathsf{Ty}}(X.A(X)).$$

Use the continuation $$K:=\mathrm{\Lambda }X::\mathsf{Ty}.\lambda z:A(X).r_z(s_z(s_z{i}_z)).$$ Under $X::\mathsf{Ty};z:A(X)$, the projections synthesize $i_z:X$, $s_z:X\to X$, and $r_z:X\to \mathbb{N}$. The two step applications have type $X$ and the observation has type $\mathbb{N}$. Hence $$K:\mathrm{\forall }X::\mathsf{Ty}.A(X)\to \mathbb{N}.$$ Opening the package with this continuation reproduces the four administrative contractions without abbreviation: The remaining projection and counter contractions are the native calculation and end in $\mathsf{suc}(\mathsf{suc}(\mathsf{0}))$.

At result type $\mathbb{N}$, the continuation arrow in the package instance is $$(\underset{―}{\mathrm{\forall }X::\mathsf{Ty}.A(X)\to \mathbb{N}})\to \mathbb{N}.$$ When $A(X)$ and $\mathbb{N}$ contain no nested universal quantifiers, the underlined continuation has rank one. Placing that polymorphic type to the left of the enclosing arrow raises the enclosing arrow to rank two. The kind of $X$ is only $\mathsf{Ty}$; the rank increase is caused by arrow position, not by a higher kind.

In the context $b:{\mathsf{Bool}}_F,m:\mathsf{Counter},n:\mathsf{Counter}$, the body tree is $$\frac{\begin{array}{c}{\displaystyle \frac{\begin{array}{c}{\displaystyle \frac{\begin{array}{c}{\displaystyle \frac{b:{\mathsf{Bool}}_F\in \mathrm{\Gamma }}{\mathrm{\Gamma }⊢b:{\mathsf{Bool}}_F}}\mathrm{T}-\mathrm{Var}\\ \cdot ⊢\mathsf{Counter}::\mathsf{Ty}\end{array}}{\mathrm{\Gamma }⊢b[\mathsf{Counter}]:\mathsf{Counter}\to \mathsf{Counter}\to \mathsf{Counter}}}\mathrm{T}-\mathrm{TApp}\\ {\displaystyle \frac{m:\mathsf{Counter}\in \mathrm{\Gamma }}{\mathrm{\Gamma }⊢m:\mathsf{Counter}}}\mathrm{T}-\mathrm{Var}\end{array}}{\mathrm{\Gamma }⊢b[\mathsf{Counter}]m:\mathsf{Counter}\to \mathsf{Counter}}}\mathrm{T}-\mathrm{App}\\ {\displaystyle \frac{n:\mathsf{Counter}\in \mathrm{\Gamma }}{\mathrm{\Gamma }⊢n:\mathsf{Counter}}}\mathrm{T}-\mathrm{Var}\end{array}}{\mathrm{\Gamma }⊢b[\mathsf{Counter}]mn:\mathsf{Counter}}\mathrm{T}-\mathrm{App}.$$ Three applications of T-Lam, discharging $n,m,b$ in that order, therefore derive $$\mathsf{chooseCounter}:{\mathsf{Bool}}_F\to \mathsf{Counter}\to \mathsf{Counter}\to \mathsf{Counter}.$$

For the false branch, the three Boolean contractions are visible after the three outer lambda contractions: Consequently the client opens $C_P$. With the states from the chapter, its two counter steps and observation are

The selected expression has the existential type $\mathsf{Counter}$. Typing it at the representation type $\mathbb{N}$ would reveal that the true branch used witness $\mathbb{N}$ and would be false for the pair-state branch, whose witness is $P=\mathbb{N}\times \mathbb{N}$. No rule projects an existential witness into the surrounding type, and T-Unpack deliberately prevents that witness from escaping. Assigning $\mathbb{N}$ would therefore violate the package’s opacity invariant.