Existential Types, Abstract Data, and Representation Independence

Universal polymorphism lets the client choose a type. Abstract data requires the implementation to choose and hide one while exporting operations that share it.

Here an implementation is a package value: a chosen representation constructor together with operations on it. An abstract interface is the existential type visible outside that package, and a client is a closed term whose input type mentions the interface but not its hidden constructor. Opaque sealing means that typing gives the client no syntax for naming that constructor outside an unpacking.

Existential packages hide a constructor

Kinds let an interface mention a representation constructor with its proper arity. They do not hide that constructor. For example, if a counter is published with state type $\mathbb{N}$, a client may apply $\mathsf{suc}$ directly to its initial state. Such a client depends on the representation, even if the library intended the state to be manipulated only through its step and read operations.

The desired interface has the shape $$X\times ((X\to X)\times (X\to \mathbb{N})),$$ but the name $X$ should be local to one implementation and to one use of that implementation. An existential type binds precisely such a name. Its introduction rule seals a witness constructor together with data at the corresponding instance of the interface. Its elimination rule opens the package under a fresh constructor name, but forbids that name from occurring in the result type.

The core has constructors $\mathsf{0}$ and $\mathsf{suc}(e)$ for $\mathbb{N}$, but no natural-number eliminator or recursor. Thus a client can return an observed number, apply $\mathsf{suc}$ to it, or pass it to another interface operation. No typing rule derives a branch or recursive call by inspecting that number. Representation independence quantifies over exactly these well-typed clients.

The no-escape premise is required by preservation, not merely by interface etiquette. If the body were allowed to return type $u$, then opening $\mathsf{pack}[\mathbb{N},\mathsf{0}]\mathsf{as}\mathrm{\exists }u::\mathsf{Ty}.u$ with body $x$ would assign the whole unpacking the locally scoped type $u$. The computation step produces $\mathsf{0}:\mathbb{N}$, but the alleged result type $u$ is free after the binder disappears. The reduct could not even be stated at the source judgment’s type. Forming $B$ in the outer $\mathrm{\Delta }$ prevents exactly this escape.

Rule T-Pack permits a witness of any kind, not only $\mathsf{Ty}$. Recall the operators $\mathsf{Map}$ and $\mathsf{P}$ and the term $\mathsf{dmap}$ from example 7.7. Define $$\mathsf{Mapper}:=\mathrm{\exists }c::\mathsf{Ty}\to \mathsf{Ty}.\mathsf{Map}c.$$ The derivations already constructed give $$\cdot ⊢\mathsf{P}::\mathsf{Ty}\to \mathsf{Ty},\cdot ;\cdot ⊢\mathsf{dmap}:\mathsf{Map}\mathsf{P}.$$ Therefore one use of T-Pack derives the genuinely higher-kinded package $$\cdot ;\cdot ⊢\mathsf{pack}[\mathsf{P},\mathsf{dmap}]\mathsf{as}\mathsf{Mapper}:\mathsf{Mapper}.$$ The witness is the unary constructor $\mathsf{P}$, not a term and not a type of kind $\mathsf{Ty}$.

A base-kind witness exhibits the no-escape premise in the smallest useful program.

Here are two implementations. The first stores only the visible count: and $$C_N:=\mathsf{pack}[\mathbb{N},q_N]\mathsf{as}\mathsf{Counter}.$$ The second stores a count together with a shadow count that advances in lockstep: Every term abbreviation on the right is a term of the core calculus; $P$ is a constructor of kind $\mathsf{Ty}$. This plain $P$ names the pair-state type; it is distinct from the earlier operator $\mathsf{P}$, which maps a type to its diagonal product. For the first payload, the rules for naturals, arrows, and products give $$\cdot ;\cdot ⊢q_N:\mathbb{N}\times ((\mathbb{N}\to \mathbb{N})\times (\mathbb{N}\to \mathbb{N})).$$ This is exactly the existential body with $\mathbb{N}$ substituted for $X$. Hence T-Pack gives $\cdot ;\cdot ⊢C_N:\mathsf{Counter}$. For the pair-state payload, $$\cdot ;\cdot ⊢q_P:P\times ((P\to P)\times (P\to \mathbb{N})),\cdot ;\cdot ⊢C_P:\mathsf{Counter}.$$

An unpacking client may use all three operations without knowing the state type. For a payload variable $z$, write $$i_z:={\mathsf{pr}}_{1}z,s_z:={\mathsf{pr}}_1({\mathsf{pr}}_{2}z),r_z:={\mathsf{pr}}_2({\mathsf{pr}}_{2}z).$$ These are abbreviations, not new term forms. Define The nested expression is easier to check by naming its projections. Under $$X::\mathsf{Ty};z:X\times ((X\to X)\times (X\to \mathbb{N}))$$ the projection and application rules derive, in order, The final type $\mathbb{N}$ is formed before $X$ is introduced. Thus T-Unpack types the unpacking at $\mathbb{N}$, and T-Lam gives $$\cdot ;\cdot ⊢{\mathsf{tick}}_2:\mathsf{Counter}\to \mathbb{N}.$$

Two tempting clients fail for two different, precise reasons. In the body of the unpacking, $\mathsf{suc}({\mathsf{pr}}_{1}z)$ is ill typed: the projection has type $X$, whereas T-Suc requires $\mathbb{N}$. The variable $X$ does not convert to $\mathbb{N}$, by distinctness of constructor heads. On the other hand, $$\lambda c:\mathsf{Counter}.\mathsf{unpack}[X,z]=c\mathsf{in}{\mathsf{pr}}_{1}z$$ has a body of type $X$, but cannot use T-Unpack: its proposed result type is not formed in the outer, empty kind context. The first error tries to use a representation-specific operation; the second tries to return the representation itself.

Substitution through packages

The computation rule for unpacking will perform a constructor substitution and then a term substitution. We therefore record their action on the two new forms before defining evaluation. After renaming binders to satisfy the displayed freshness conditions, where $v\ne u$ and $v\notin \mathrm{fv}(C)$. Term substitution changes no constructor annotation and satisfies where $x\ne y$, $x\notin \mathrm{fv}(d)$, and the constructor binder $u$ has first been chosen fresh for every constructor occurring free in $d$. These are equations of capture-avoiding substitution, not reduction rules.

Proof of Lemma 7.33 — Structural lemmas for package terms

Proof. Term-context weakening, constructor-context weakening, and term substitution are inductions on the typing derivation; constructor substitution is an induction on the same derivation together with kinding substitution. The package-free cases are the four interfaces of lemma 11.34. For a T-Conv premise, weakening uses lemma 11.33. Constructor substitution instead uses lemma 7.27; kinding substitution alone would not transport its equality premise. We give both new package-rule cases, because each contains a constructor binder.

The constructor-substitution induction uses the split context $${\mathrm{\Delta }}_0,u::\kappa ,{\mathrm{\Delta }}_1.$$ It carries this split unchanged through every premise. This is essential beneath T-TLam, K-All, and the two package binders: a new declaration is appended to ${\mathrm{\Delta }}_1$, rather than exchanged across $u$. If that declaration mentions $u$, exchanging it to the left of $u$ would make its annotation ill formed because $u$ would no longer occur in the prefix where the annotation is checked. For T-Pack, rename the package binder $v$ away from $u$ and $C$. Suppressing the common split, its premises have the form $$\begin{array}{c}{\mathrm{\Delta }}_0,u::\kappa ,{\mathrm{\Delta }}_1⊢D::{\kappa }^{\prime },\\ {\mathrm{\Delta }}_0,u::\kappa ,{\mathrm{\Delta }}_1,v::{\kappa }^{\prime }⊢A::\mathsf{Ty},\\ {\mathrm{\Delta }}_0,u::\kappa ,{\mathrm{\Delta }}_1;\mathrm{\Gamma }⊢e:A[D/v].\end{array}$$ Kinding substitution and the induction hypothesis give the corresponding premises for $D[C/u]$, $A[C/u]$, and $e[C/u]$. The substitution-composition law lemma 7.17(1) gives the payload-type equation $$(A[D/v])[C/u]=A[C/u][D[C/u]/v].$$ Rule T-Pack now reconstructs the substituted package.

For constructor substitution in T-Unpack, rename its hidden binder $v$ away from $u$ and $C$. Apply the induction hypothesis to the scrutinee. In the body premise use the split-context induction hypothesis with ${\mathrm{\Delta }}_1,v::{\kappa }^{\prime }$ as the suffix. Freshness makes substitution pass through $v$, giving $${\mathrm{\Delta }}_0,{\mathrm{\Delta }}_1,v::{\kappa }^{\prime };\mathrm{\Gamma }[C/u],x:A[C/u]⊢e_2[C/u]:B[C/u].$$ Kinding substitution forms $B[C/u]$ in ${\mathrm{\Delta }}_0,{\mathrm{\Delta }}_1$, so T-Unpack reconstructs the conclusion.

For term substitution, T-Pack applies the induction hypothesis only to the payload. In T-Unpack, rename its term binder $x$ away from $y$ and $d$. Apply the induction hypothesis to the scrutinee and to the body. For the latter, first apply constructor-context weakening to the derivation of $d$, then term-context weakening through the declaration $x:A$; use the body induction hypothesis with that declaration in the trailing context. Reapply T-Unpack. Both weakening inductions repeat these two reconstructions without a replacement step. Thus all four inductions cover the new grammar. ◻

Call-by-value opening and safety

A package hides a constructor; it should not hide an unfinished computation. Call-by-value evaluation therefore evaluates the payload before regarding the package as a value. It also evaluates the scrutinee of an unpacking before opening it.

Proof of Lemma 12.5 — Determinism of package evaluation

Proof. First, no value takes a call-by-value step. This is an induction on the value grammar: no root rule has a value as its source, and the evaluation contexts do not descend beneath a value former. Induct on the term. The left-to-right evaluation-context grammar selects at most one immediate subterm: it advances past a position only after that position is a value. Once all required subterms are values, their outer constructor selects at most one of the four root rules. Those roots have disjoint outer forms, and each has one right-hand side. The induction hypothesis gives a unique step in the selected proper subterm. ◻

Call-by-value reduction answers how a program is run. Representation independence needs a larger equality: two terms are beta-convertible even when the decisive contraction lies beneath a binder or in a branch that call-by-value evaluation does not enter.

The operational relations have the following distinct domains and closures: The role macros ${⟶}_{\beta }$ and ${⟶}_{\beta }$ deliberately share the same printed beta arrow. Their operand sorts and the $e$-beta and $A$-beta tags distinguish directed reductions at the term and constructor levels. The relation ${=}_{\beta }$ is reserved for term conversion, while $\equiv$ compares formed constructors.

Proof of Proposition 7.36 — Subject reduction for compatible term beta

Proof. Peel the final chain of T-Conv uses from the typing of the whole expression. Induct on the compatible step at the remaining syntax-directed result type, then restore the conversion chain. The root cases use inversion through any conversions on their operator premises.

For term beta, suppose the application rule expects an operator of type $D\to A$. Strip conversions from the typing of $\lambda x:C.e_0$. Its introduction rule gives $\mathrm{\Delta };\mathrm{\Gamma },x:C⊢e_0:B$, while the stripped conversion gives $C\to B\equiv D\to A$. Arrow-head injectivity yields $C\equiv D$ and $B\equiv A$. Convert the operand from $D$ to $C$, apply term substitution, and finally convert the result from $B$ to $A$.

For type beta, suppose type application expects an operator of type $\mathrm{\forall }u::\kappa .A$. Stripping conversions from the typing of $\mathrm{\Lambda }v::{\kappa }^{\prime }.e_0$, followed by alpha-renaming, gives $\mathrm{\Delta },u::\kappa ;\mathrm{\Gamma }⊢e_0:B$ and $\mathrm{\forall }u::\kappa .B\equiv \mathrm{\forall }u::\kappa .A$. Universal-head injectivity gives $B\equiv A$ in the extended constructor context. Constructor substitution types $e_0[C/u]$ at $B[C/u]$; equality substitution and T-Conv change that result to $A[C/u]$.

For projection beta, suppose the projection rule expects $D_1\times D_2$. Strip conversions from the typing of the displayed pair. Product-head injectivity gives $C_i\equiv D_i$ for $i\in \{1,2\}$. The selected pair premise has type $C_i$, and one use of T-Conv gives the required $D_i$.

For the unpacking root, invert T-Unpack. Write its scrutinee type as $\mathrm{\exists }u::\kappa .A_1$ and its body premise as $$\mathrm{\Delta },u::\kappa ;\mathrm{\Gamma },x:A_1⊢e_0:B,\mathrm{\Delta }⊢B::\mathsf{Ty}.$$ Peeling final conversions from the package typing and using existential-head injectivity gives, after alpha-renaming, $$\mathrm{\Delta }⊢C::\kappa ,\mathrm{\Delta };\mathrm{\Gamma }⊢d:A_0[C/u],\mathrm{\Delta },u::\kappa ⊢A_0\equiv A_1::\mathsf{Ty}.$$ Equality substitution and T-Conv type $d$ at $A_1[C/u]$. Constructor substitution types $e_0[C/u]$ at $B$ in $\mathrm{\Gamma },x:A_1[C/u]$; because $u$ is absent from the well-formed outer $\mathrm{\Gamma }$ and $B$, their substitutions by $C$ are literally $\mathrm{\Gamma }$ and $B$. Term substitution now types $e_0[C/u][d/x]$ at $B$, as required.

For a step in a proper subterm, apply the induction hypothesis to its typing premise and rebuild the same typing rule. Beneath $\lambda$, $\mathrm{\Lambda }$, or the body of an unpacking, the induction hypothesis is applied in the corresponding extended context. These cases cover every term constructor. ◻

The quotient by ${=}_{\beta }$ is taken separately at each fixed type. The proposition ensures that every forward reduction used in a conversion calculation remains at that type.

The existential type displayed in the first premise of T-Unpack need not use the same bound-variable name or the same spelling of its body as the type synthesized for the scrutinee. Typing shows that the two existential types are convertible; the preservation proof above used injectivity of the existential head to reconcile their bodies.

Proof of Lemma 7.37 — Canonical package values

Proof. Peel off all final uses of T-Conv, composing their equalities. The last remaining rule is determined by the value form. Its syntax-directed result type has outer head $\to$, $\mathrm{\forall }$, $\times$, $\mathbb{N}$, or $\mathrm{\exists }$, respectively. Distinct heads do not convert (corollary 7.26), so only the form with the requested head can occur.

In the existential case the remaining rule is T-Pack, whose premises give $\mathrm{\Delta }⊢C::\kappa$ and the required payload typing. Its result type $\mathrm{\exists }a::{\kappa }^{\prime }.A_0$ converts to $\mathrm{\exists }u::\kappa .A$. Existential-head injectivity gives ${\kappa }^{\prime }=\kappa$ and, after opening both binders with one fresh $u$, $A_0\equiv A$. Alpha-renaming the annotation produces the required package. For the four other heads, replace T-Pack respectively by T-Lam, T-TLam, T-Pair, and T-Zero/T-Suc; head disjointness rules out every other value form, and head injectivity gives the component equalities described in the statement. ◻

Proof of Theorem 7.38 — Preservation

Proof. Every call-by-value step is a compatible term-beta step by definition 7.35. Apply proposition 7.36. Notice that this argument also covers a reduction in an evaluation context: compatible closure already contains every call-by-value context. ◻

Proof of Theorem 7.39 — Progress

Proof. Induct on the typing derivation. A variable case is impossible, and a final T-Conv uses the induction hypothesis of its premise. Term and type abstractions are values. For an application, first apply the induction hypothesis to the operator and then to the operand. If both are values, the arrow clause of canonical forms gives an operator $\lambda x:B.s$, so term beta applies. For type application, a universal-typed value has form $\mathrm{\Lambda }u::\kappa .s$, so type beta applies. For a pair, evaluate its components from left to right; it is a value when both are values. For a projection, evaluate its argument; a value of product type is a pair, so projection beta applies. The zero term is a value, and a successor evaluates its argument or is a value.

For a package, apply the induction hypothesis to its payload. A payload step occurs in the package context; if the payload is a value, the package is a value by the value grammar. For $\mathsf{unpack}[u,x]=e_1\mathsf{in}{e}_2$, apply the induction hypothesis to $e_1$. A step occurs in the unpacking context. If $e_1$ is a value, lemma 7.37 proves that it has the form $\mathsf{pack}[C,d]\mathsf{as}\mathrm{\exists }u::\kappa .A$ with value payload $d$, so the unpacking contraction applies. These cases exhaust the typing rules. ◻

Proof of Corollary 7.40 — Safety

Proof. Repeated preservation types $e^{\prime }$ at $A$; progress gives the alternative. ◻

An open unpacking can be blocked, as an eliminator should be. In the context $y:\mathsf{Counter}$ the term $$\mathsf{unpack}[X,z]=y\mathsf{in}({\mathsf{pr}}_2({\mathsf{pr}}_{2}z))({\mathsf{pr}}_{1}z)$$ is well typed at $\mathbb{N}$ but takes no step: its scrutinee is the variable $y$, not a package value. This does not contradict progress, whose term context is empty.

Running the two counters

The client reduction realizes its typing derivation as follows. After the outer term beta step, opening $C_N$ substitutes $\mathbb{N}$ for $X$ and $q_N$ for $z$. The three projection abbreviations satisfy $$i_{q_N}⟶i_N,s_{q_N}{⟶}^{\ast }{s}_N,r_{q_N}{⟶}^{\ast }{r}_N.$$ For example, $s_{q_N}={\mathsf{pr}}_1({\mathsf{pr}}_2{q}_N)$ first reduces its inner projection to $(s_N,r_N)$ and then reduces to $s_N$. The client calculation is therefore

For the pair implementation, put One step operation performs the following complete calculation: The same three contractions with $p_1$ in place of $p_0$ yield $s_P{p}_1{⟶}^{\ast }{p}_2$. Consequently, Thus this particular client obtains the same observation from the two packages, although their state values have different types.

This agreement is a calculation, not a representation-independence theorem. Existential typing enforces opacity; by itself it does not assert that any two packages of the same existential type behave alike. To see the difference, replace $s_N$ by $$s_N^{+2}:=\lambda n:\mathbb{N}.\mathsf{suc}(\mathsf{suc}(n))$$ and seal the resulting payload at $\mathsf{Counter}$. It has the same existential type as $C_N$, but the calculation above now ends at $\mathsf{suc}(\mathsf{suc}(\mathsf{suc}(\mathsf{suc}(\mathsf{0}))))$. A relation between witnesses and operations is the additional premise needed to prove representation independence.

Relations at higher kinds

The relation environment of chapter 6 assigns to a type variable $X$ two closed types and a relation between their closed terms. That assignment is insufficient for $c::\mathsf{Ty}\to \mathsf{Ty}$. The expression $cA$ is a type, so its interpretation must be a relation; but the relation may depend on the relation chosen for $A$. Thus $c$ must carry an action: it sends related arguments to a relation between the two results. This is the one new idea. The clauses for constructor abstraction and application will merely form and apply such actions.

Constructor-beta endpoints require the following indexing convention.

For relations $R:A_0\leftrightarrow A_1$ and $S:B_0\leftrightarrow B_1$, recall arrow lifting and define product lifting by In the first line the implication is required for every $[a]R[b]$. Both definitions are independent of representatives because beta conversion is compatible with application and projection. Put $${\mathsf{Eq}}_{\mathbb{N}}:=\{([m],[m])\mid [m]\in \mathsf{Tm}(\mathbb{N})\}.$$

Proof of Lemma 12.14 — Constructor-convertible relation endpoints

Proof. Induct on $\kappa$. At $\mathsf{Ty}$, $\mathsf{Tm}(A_i)=\mathsf{Tm}(A_i^{\prime })$ by T-Conv, so the two power sets are literally equal. At ${\kappa }_0\to {\kappa }_1$, the same operations occur on both sides: for each pair $C_0,C_1$ and input relation $R$, constructor congruence proves $A_i{C}_i\equiv A_i^{\prime }{C}_i$, and the induction hypothesis at ${\kappa }_1$ gives equality of the required output collections. ◻

The following notation distinguishes beta-classes, type application, and substitution: Thus the outer brackets in $[e[{\rho }_i][{\gamma }_i]]$ form one beta-class after the two substitutions.

These collections are meta-level sets for the same reason as in definition 6.1: closed constructors and terms are countable syntax, the base clause uses a power set, and the arrow clause is a set of operations between already constructed sets at proper subkinds.

The naive arrow-kind attempt assigns only a bare set of pairs of closed constructor beta-classes at endpoints $F_0$ and $F_1$, without an operation describing how that set acts on a related argument. At an application it then asks for $$[[cA{]]}_{\rho }\text{from only}\rho (c)=(F_0,F_1,R),$$ but $R$ contains no relation between $F_0{C}_0$ and $F_1{C}_1$—in particular none at the concrete instance $\mathsf{Map}\mathsf{P}$. The repair is an action $\mathrm{\Phi }$ that maps each related input triple to a well-indexed output relation. No functor law is imposed: the abstraction theorem needs only that every related input is sent to a well-indexed output relation. In particular, we do not require $\mathrm{\Phi }$ to preserve identity relations or composition of relations; “functor” here refers to that categorical preservation condition. Parameterized ML modules use the same word for a different construction, and neither use concerns modules over a ring.

As in chapter 6, $ϵ$ denotes the unique relation environment over the empty constructor context; it is not an empty relation.

The relational interpretation of a constructor $A$ will be written $[[A{]]}_{\rho }$. If $\mathrm{\Delta }⊢A::\kappa$, it must belong to $${\mathrm{Rel}}_{\kappa }(A[{\rho }_0],A[{\rho }_1]).$$ The following definition gives all its clauses. In the binder clauses, the bound variable is first renamed away from the finite ranges of the endpoint substitutions.

The existential clause is asymmetric with the universal clause for a reason. A polymorphic term must work for every relational object. A package hides one pair of witnesses, so related packages need exhibit one relation between those witnesses. Requiring every relation would reject ordinary abstract data types; requiring no witness relation would leave the payloads unconnected.

Three lemmas are needed before the term induction. The first prevents silent index changes; the second is the constructor-level analogue of the type-substitution lemma from chapter 6; the third handles rule T-Conv.

Proof of Lemma 7.45 — Endpoints and irrelevant constructor variables

Proof. Prove both claims simultaneously by induction on the kinding derivation. The variable, $\mathbb{N}$, arrow, and product cases follow directly from their defining clauses. For $\lambda u::{\kappa }_0.A_0$, take an arbitrary relational object $Q$ of kind ${\kappa }_0$. The induction hypothesis under $\rho [u\mapsto Q]$ indexes the body relation by $$A_0[{\rho }_0,u\mapsto Q_0]\text{and}{A}_0[{\rho }_1,u\mapsto Q_1].$$ These are beta-convertible to the applications of the two endpoint abstractions to $Q_0,Q_1$, so the action has the required arrow-kind index. Agreement away from the free variables of the abstraction remains agreement after extending both environments by the same $Q$.

For $A_1{A}_2$, the induction hypothesis for $A_1$ gives an action and the one for $A_2$ gives an admissible relational argument. Applying the former to the latter gives exactly the required endpoint applications.

For $\mathrm{\forall }u::{\kappa }_0.A_0$, type application at $Q_i$ has endpoint type $A_0[{\rho }_i,u\mapsto Q_i]$; the body induction hypothesis therefore types every relation required by the universal clause.

For $\mathrm{\exists }u::{\kappa }_0.A_0$, suppose $[p]$ and $[q]$ satisfy the existential clause, witnessed by $Q=(C_0,C_1,R)$, payloads $a_0,a_1$, and annotations $\mathrm{\exists }{v}_i::{\kappa }_0.D_i$. The body induction hypothesis says that $[a_0][[A_0{]]}_{\rho [u\mapsto Q]}[a_1]$ is indexed by $$A_0[{\rho }_0,u\mapsto C_0]\text{and}{A}_0[{\rho }_1,u\mapsto C_1].$$ Hence T-Pack, using the endpoint body $A_0[{\rho }_i]$, types the two literal packages at $\mathrm{\exists }u::{\kappa }_0.A_0[{\rho }_i]$. The annotation equalities in the definition, existential-head injectivity from corollary 7.26, and T-Conv give the same endpoint typing for the displayed $D_i$ annotations. The domain restriction in the defining clause already places $[p]$ and $[q]$ in the two corresponding $\mathsf{Tm}$ endpoints; the two term-beta equalities choose the displayed package representatives of those classes. Thus all five conditions of the defining clause contribute: two expose the packages, two align their annotations, and the last relates well-typed payloads.

In both binder cases, irrelevance follows by extending the two environments with the same arbitrary $Q$ and applying the body hypothesis. These cases exhaust the constructor grammar. ◻

Proof of Lemma 7.46 — Relational constructor substitution

Proof. Induct on the kinding derivation of $A$. At the variable $u$, both sides are $[[B{]]}_{\rho }$; another variable and $\mathbb{N}$ are unchanged. For arrows and products, apply the induction hypothesis at both components and form the corresponding relational lifting.

For application $A_1{A}_2$, the left side applies the interpreted action of $A_1[B/u]$ to the interpreted relational object of $A_2[B/u]$. The two induction hypotheses replace these by the interpretation of $A_1$ and the relational object of $A_2$ under $\rho [u\mapsto Q_B]$, which is the right-hand application clause.

For a binder, first rename its variable $v$ so that $v\ne u$ and $v\notin \mathrm{fv}(B)$. In the constructor-abstraction case, apply both sides to an arbitrary relational object $Q$ for $v$. The body induction hypothesis applies under $\rho [v\mapsto Q]$. Irrelevance and $v\notin \mathrm{fv}(B)$ give equality of relational objects $$(B[{\rho }_0,v\mapsto Q_0],B[{\rho }_1,v\mapsto Q_1],[[B{]]}_{\rho [v\mapsto Q]})=Q_B.$$ The two environment extensions commute, so the resulting body relations are equal. This proves equality of the actions. For a universal, fix an arbitrary $Q$; the body induction hypothesis equates the two relations applied to $p[Q_0]$ and $q[Q_1]$, so the universally quantified membership conditions coincide. For an existential, keep its witnessing $Q$, payloads, and written annotations fixed; the body induction hypothesis equates the two payload conditions. Its endpoint calculation $$(A_0[B/u])[{\rho }_i]=A_0[{\rho }_i,u\mapsto B[{\rho }_i]](i=0,1)$$ is the simultaneous/single substitution-composition equation. It makes the left clause’s annotation condition $\mathrm{\exists }v.D_i\equiv \mathrm{\exists }w.A_0[B/u][{\rho }_i]$ identical to the right clause’s condition $\mathrm{\exists }v.D_i\equiv \mathrm{\exists }w.A_0[{\rho }_i,u\mapsto B[{\rho }_i]]$ after freshening $v,w$. The payload condition is the body equality just proved. ◻

Proof of Lemma 7.47 — Invariance under constructor equality

Proof. At arrow kind, equality of actions is ordinary function extensionality in the fixed ZF metatheory. Write $\mathrm{\Phi }(Q)$ for $\mathrm{\Phi }(C_0,C_1,R)$ when $Q=(C_0,C_1,R)$. Then $$\mathrm{\Phi }=\mathrm{\Psi }⟺\mathrm{\Phi }(Q)=\mathrm{\Psi }(Q)\text{ for every relational object }Q.$$ First prove invariance under one constructor reduction. Induct on the constructor reduction (an $A$-beta step). At the root redex, by lemma 7.46. A congruence step uses the induction hypothesis in the corresponding compositional clause of definition 7.43; at arrow kind apply the displayed extensionality principle and the body induction hypothesis to each arbitrary relational object.

By the common-reduction characterization of constructor equality, theorem 7.25, $A$ and $B$ reduce to one constructor $C$. Repeated one-step invariance gives $[[A{]]}_{\rho }=[[C{]]}_{\rho }=[[B{]]}_{\rho }$. At an existential endpoint, keep the witness, payloads, and payload relation fixed. If a written endpoint annotation is $E_i$, its old and new side conditions are $$E_i\equiv A[{\rho }_i],E_i\equiv B[{\rho }_i].$$ Applying constructor-equality substitution successively to the closed images of ${\rho }_i$ gives $A[{\rho }_i]\equiv B[{\rho }_i]$. Transitivity converts the old condition to the new; symmetry and transitivity give the reverse implication. Thus the two existential membership conditions are equivalent. ◻

The abstraction theorem with packages

For existential elimination, the two endpoint substitutions and the closing term substitutions must be related. Let $\mathrm{\Delta }⊢\mathrm{\Gamma }\mathsf{ctx}$ and let $\rho :{\rho }_0\leftrightarrow {\rho }_1\mathsf{over}\mathrm{\Delta }$. Endpoint substitutions ${\gamma }_i$ close the term variables when $$\cdot ;\cdot ⊢{\gamma }_i(x):A[{\rho }_i]\text{for each }x:A\in \mathrm{\Gamma }.$$ They are related, written ${\gamma }_0[[\mathrm{\Gamma }{]]}_{\rho }{\gamma }_1$, when $$[{\gamma }_0(x)][[A{]]}_{\rho }[{\gamma }_1(x)]\text{for each }x:A\in \mathrm{\Gamma }.$$

Proof of Theorem 7.48 — Abstraction for F_ω with existentials

Proof. Induct on the typing derivation with the displayed relational judgment as the induction property. At a type binder, endpoint irrelevance preserves the relation on $\mathrm{\Gamma }$. At constructor application, relational constructor substitution rewrites the interpreted result type. At T-Conv, conversion invariance rewrites the endpoint relations. Capture-avoiding substitution commutes with the closing substitutions in every term-binder case.

Variable. The conclusion is the corresponding component of ${\gamma }_0[[\mathrm{\Gamma }{]]}_{\rho }{\gamma }_1$.

Arrow introduction. For a last premise $\mathrm{\Delta };\mathrm{\Gamma },x:B⊢e_0:C$, take arbitrary closed $a_0,a_1$ with $[a_0][[B{]]}_{\rho }[a_1]$. The substitutions ${\gamma }_i[x\mapsto a_i]$ are related at the extended context, so the induction hypothesis relates the two substituted bodies at $[[C{]]}_{\rho }$. At endpoint $i$, term beta gives $$(\lambda x:B[{\rho }_i].e_0[{\rho }_i][{\gamma }_i])a_i{=}_{\beta }{e}_0[{\rho }_i][{\gamma }_i[x\mapsto a_i]].$$ Thus the two applications satisfy the arrow-lifting clause.

Arrow elimination. The operator induction hypothesis lies in $[[B{]]}_{\rho }\Rightarrow [[C{]]}_{\rho }$, and the argument hypothesis lies in $[[B{]]}_{\rho }$. Apply the former to the latter.

Type abstraction (T-TLam). Suppose the premise is $\mathrm{\Delta },u::\kappa ;\mathrm{\Gamma }⊢e_0:B$, with $u$ fresh for $\mathrm{\Gamma }$. To establish the universal relation, take an arbitrary relational object $Q=(C_0,C_1,R)$ of kind $\kappa$ and extend $\rho$ by $u\mapsto Q$. Since $u$ is absent from every declaration in $\mathrm{\Gamma }$, endpoint irrelevance says that the original ${\gamma }_0,{\gamma }_1$ remain related. The induction hypothesis gives the body relation. The type-application beta law identifies its endpoints with $$((\mathrm{\Lambda }u::\kappa .e_0)[{\rho }_i][{\gamma }_i])[C_i].$$ As $Q$ was arbitrary, this is the universal clause.

Type application (T-TApp). Suppose the operator has type $\mathrm{\forall }u::\kappa .B$ and the argument constructor is $C$. Its interpretation forms the relational object $$Q_C=(C[{\rho }_0],C[{\rho }_1],[[C{]]}_{\rho }).$$ The operator induction hypothesis is universal over relational objects. Instantiating it at $Q_C$ gives the body relation $[[B{]]}_{\rho [u\mapsto Q_C]}$, which equals $[[B[C/u]{]]}_{\rho }$ by lemma 7.46.

Product introduction. The two induction hypotheses relate the components. The projection beta laws therefore put the two pairs in $[[A_1{]]}_{\rho }\times [[A_2{]]}_{\rho }$.

Product elimination. The premise induction hypothesis is a pair in the product lifting. Its $i$th conjunct is exactly the required relation between the $i$th projections.

Natural numbers. The two occurrences of $\mathsf{0}$ determine the same beta-class, hence are in ${\mathsf{Eq}}_{\mathbb{N}}$. In the successor case the induction hypothesis says the two arguments are beta-equal; compatible conversion makes their successors beta-equal as well.

Conversion. The premise induction hypothesis gives the relation interpreted at the premise type. By lemma 7.47, the conclusion type has the same interpreted relation after the endpoint conversions performed by T-Conv.

Existential introduction. Suppose the package witness is $C::\kappa$ and its payload premise has type $B[C/u]$. Form $Q_C$ as in the constructor-application case. The payload induction hypothesis lies in $$[[B[C/u]{]]}_{\rho }=[[B{]]}_{\rho [u\mapsto Q_C]},$$ where the equality is lemma 7.46. The two substituted package terms have witnesses $C[{\rho }_0]$ and $C[{\rho }_1]$, with payloads related by this equation. Hence they are related at $[[\mathrm{\exists }u::\kappa .B{]]}_{\rho }$.

Existential elimination. Write the last two premises as $$\mathrm{\Delta };\mathrm{\Gamma }⊢e_1:\mathrm{\exists }u::\kappa .B,\mathrm{\Delta },u::\kappa ;\mathrm{\Gamma },x:B⊢e_2:D,$$ where $u$ is absent from $\mathrm{\Gamma }$ and $D$. By the first induction hypothesis, the two closed instances of $e_1$ are related existential packages. Unfolding the existential clause gives a relational object $Q=(C_0,C_1,R)$ and payloads $a_0,a_1$ such that the endpoint instances of $e_1$ are beta-equal to the corresponding packages and $$[a_0][[B{]]}_{\rho [u\mapsto Q]}[a_1].$$ Endpoint irrelevance keeps the substitutions ${\gamma }_i$ related at $\mathrm{\Gamma }$ after extending $\rho$ by $Q$. Extending them further by $x\mapsto a_i$ therefore satisfies the hypotheses for the body induction hypothesis, which gives $$[e_2[{\rho }_0,u\mapsto C_0][{\gamma }_0,x\mapsto a_0]][[D{]]}_{\rho [u\mapsto Q]}[e_2[{\rho }_1,u\mapsto C_1][{\gamma }_1,x\mapsto a_1]].$$ Since $u$ is not free in $D$, irrelevance changes the middle relation to $[[D{]]}_{\rho }$. Finally, compatible conversion replaces each endpoint instance of $e_1$ by its package, and the package computation rule gives $$\mathsf{unpack}[u,x]=(\mathsf{pack}[C_i,a_i])\mathsf{in}{e}_2{=}_{\beta }{e}_2[C_i/u][a_i/x].$$ This is exactly the pair of terms in the theorem’s conclusion. ◻

Proof of Corollary 7.49 — Self-parametricity

Proof. Use theorem 7.48 with empty constructor and term environments. ◻

Proof of Corollary 12.23 — Related values are indistinguishable by natural clients

Proof. Self-parametricity gives $$[k]([[E{]]}_{ϵ}\Rightarrow {\mathsf{Eq}}_{\mathbb{N}})[k].$$ Apply this arrow relation to the assumed pair. Its result belongs to ${\mathsf{Eq}}_{\mathbb{N}}$, which is beta equality by definition. ◻

Representation independence for an existential counter

Representation independence means that clients cannot distinguish implementations related at their abstract interface. The Church-encoded counter of section 6.6 quantified the representation type in every client. The existential type $\mathsf{Counter}$ of definition 7.32 moves that quantifier to the implementation boundary. The preceding calculations compared its $\mathbb{N}$ implementation $C_N$ with its shadow-count implementation $C_P$ for one client. The logical relation proves that the two instances of every closed natural-number client are beta-convertible.

The state constructors are $\mathbb{N}$ and $P=\mathbb{N}\times \mathbb{N}$. Relate their closed terms by $$[n]R[p]⟺p{=}_{\beta }(n,n).$$ This is a relation in ${\mathrm{Rel}}_{\mathsf{Ty}}(\mathbb{N},P)$. It records the lockstep invariant used by the second implementation: both stored coordinates are the visible count.

Proof of Lemma 7.50 — The counter packages are related

Proof. Use the relational object $(\mathbb{N},P,R)$ as the hidden witness of the existential clause. We verify the three payload components.

First, $i_P{=}_{\beta }(i_N,i_N)$, so $[i_N]R[i_P]$. Next suppose $[n]R[p]$. Then $p{=}_{\beta }(n,n)$, and the projection and function beta laws give $$s_{P}p{=}_{\beta }(\mathsf{suc}(n),\mathsf{suc}(n)){=}_{\beta }(s_{N}n,s_{N}n).$$ Thus $[s_N](R\Rightarrow R)[s_P]$. The same hypothesis gives $$r_{P}p{=}_{\beta }n{=}_{\beta }{r}_{N}n,$$ so $[r_N](R\Rightarrow {\mathsf{Eq}}_{\mathbb{N}})[r_P]$. Two uses of product lifting now yield $$[q_N]R\times ((R\Rightarrow R)\times (R\Rightarrow {\mathsf{Eq}}_{\mathbb{N}}))[q_P].$$ This middle relation is $[[X\times ((X\to X)\times (X\to \mathbb{N})){]]}_{X\mapsto (\mathbb{N},P,R)}$. In the existential clause, the two term-beta conditions are reflexive on the displayed packages, and the two annotation conditions are literal equalities because both packages are written with annotation $\mathsf{Counter}$. The payload relation proved above is its fifth condition. The existential clause therefore relates $C_N$ and $C_P$. ◻

Proof of Theorem 7.51 — Existential counter representation independence

Proof. Apply corollary 12.23 to lemma 7.50. ◻

No identity-extension theorem is hidden in this proof. Such a theorem would identify the relation assigned to a closed type with equality at that type; section 6.4 showed why beta equality does not validate that principle in general. Equality of the observations follows only because the result constructor is the primitive $\mathbb{N}$ and its relational clause was defined to be ${\mathsf{Eq}}_{\mathbb{N}}$. Replacing $\mathbb{N}$ by an arbitrary closed type $O$ would yield related results at $[[O{]]}_{ϵ}$; it would not by itself yield beta equality. The calculations for ${\mathsf{tick}}_2$ above are the visible instance of the theorem. The theorem now establishes their conclusion for every well-typed closed natural-number client.

The result is stated in beta equality, not silently in evaluation equivalence. This chapter has not established term-level normalization and confluence for the full $F_{\omega }$ package calculus. If those standard metatheorems are supplied, any call-by-value evaluations $k{C}_N{⟶}^{\ast }\bar{m}$ and $k{C}_P{⟶}^{\ast }\bar{n}$ are compatible beta reductions to normal forms; confluence and the theorem force $m=n$. Without that additional metatheory, the proved observation is exactly the displayed beta equality.

Sources.

The package rules, escape condition, and representation independence pattern follow the development of abstract types in [Har16]. Relation environments and the abstraction argument originate with Reynolds; the relation interpretation and abstraction theorem occur on pp. 515–517, and the representation semantics and theorem on pp. 518–519 of [Rey83]. The arrow-kind action, constructor substitution, and conversion proofs above are the extension needed for this chapter’s $F_{\omega }$ signature. Those steps were proved locally rather than attributed to the System F statement in the cited paper.

Optional route.

A higher-rank client hidden inside existential elimination $\star$

The native unpacking rule binds an abstract constructor directly. There is another way to expose the same client boundary: ask a package to accept a polymorphic continuation. This does not replace the native calculus under call-by-value evaluation, but it shows exactly where a higher-rank argument enters the package encoding.

Suppose $\mathrm{\Delta },u::\kappa ⊢A::\mathsf{Ty}$. With $R$ fresh, define the Church package type $${\mathsf{Some}}_{\kappa }(u.A):=\mathrm{\forall }R::\mathsf{Ty}.(\mathrm{\forall }u::\kappa .A\to R)\to R.$$ If $\mathrm{\Delta }⊢C::\kappa$ and $\mathrm{\Delta };\mathrm{\Gamma }⊢v:A[C/u]$, define $$\mathsf{cpack}[C,v]:=\mathrm{\Lambda }R::\mathsf{Ty}.\lambda k:\mathrm{\forall }u::\kappa .A\to R.k[C]v.$$ Rule T-TApp gives $k[C]:A[C/u]\to R$; its domain is well formed by constructor substitution. Together with $\mathrm{\Delta };\mathrm{\Gamma }⊢v:A[C/u]$, rule T-App gives $k[C]v:R$. Repeated uses of T-TLam and T-Lam derive $$\mathrm{\Delta };\mathrm{\Gamma }⊢\mathsf{cpack}[C,v]:{\mathsf{Some}}_{\kappa }(u.A).$$

Here rank counts how deeply a universal quantifier occurs to the left of arrows. A prenex type has all of its quantifiers at the front and has rank one; placing such a polymorphic type in an arrow domain raises the rank to two. A monomorphic type in this paragraph contains no universal quantifier.

Now suppose $$\begin{array}{c}\mathrm{\Delta }⊢\mathrm{\Gamma }\mathsf{ctx},\mathrm{\Delta };\mathrm{\Gamma }⊢p:{\mathsf{Some}}_{\kappa }(u.A),\\ \mathrm{\Delta },u::\kappa ;\mathrm{\Gamma },x:A⊢e:B,\mathrm{\Delta }⊢B::\mathsf{Ty}.\end{array}$$ Formation of $\mathrm{\Gamma }$ before $u$ makes the constructor binder fresh for the surrounding term context; formation of $B$ before $u$ is the escape condition. These are the two corresponding side conditions of native unpacking. The continuation $$\mathrm{\Lambda }u::\kappa .\lambda x:A.e:\mathrm{\forall }u::\kappa .A\to B$$ may be passed to a Church package $p$ by $${\mathsf{copen}}_B(p;u,x.e):=p[B](\mathrm{\Lambda }u::\kappa .\lambda x:A.e).$$ Here a polymorphic term appears in the domain of the package’s continuation arrow. When $A$ and $B$ contain no nested universal types, the continuation $\mathrm{\forall }u::\kappa .A\to B$ has rank one, while the enclosing arrow $(\mathrm{\forall }u::\kappa .A\to B)\to B$ has rank two. If $A$ or $B$ already has higher-rank structure, the rank may be larger. Higher kinds and higher rank are independent notions: $\kappa$ may be $\mathsf{Ty}$; the rank rise comes from placing the polymorphic continuation to the left of an arrow.

For a value payload, the entire administrative calculation is visible: Constructor and term annotations have only been suppressed on the middle three lines. The result is the native unpacking contraction.

This calculation does not prove a general call-by-value encoding theorem. A native package evaluates its payload before becoming a value; a Church package begins with $\mathrm{\Lambda }R$ and can hide an unfinished payload beneath that value. Thus we have proved typing and the value-payload calculation, not operational equivalence for arbitrary effects or divergence. Church checking remains syntax directed because every binder is annotated. The undecidability of Curry-style System F inference from theorem 5.23 is unaffected.

Sources.

The existential-as-universal definition and its beta calculation appear in [GLT89]. Harper gives the same client encoding and states the lazy-dynamics qualification in [Har16]. The value restriction in the calculation above is therefore part of the theorem, not an implementation footnote.

First-class packages

A package is an ordinary term, so an eliminator may select between package values at run time. Using the Church booleans of definition 5.15, with their quantified variable kinded by $\mathsf{Ty}$, define All three lambda annotations are the types displayed on the first line. The universal elimination for $b$, followed by two applications, proves the typing judgment.

The true branch is a complete first-class-package calculation: Replacing ${\mathsf{true}}_F$ by ${\mathsf{false}}_F$ chooses $C_P$ and reaches the same displayed numeral by the earlier shadow-count calculation. The choice occurs before unpacking; both branches have the common existential type $\mathsf{Counter}$.

First class does not make the hidden constructor projectible. From an arbitrary $m:\mathsf{Counter}$ there is no type expression $m.X$ in the core grammar. One must unpack $m$, receiving a fresh lexical name $X$ whose scope is the unpacking body. The core also has no syntax relating the hidden constructors of two packages or naming a component of one package in the type of another. Module systems with static names and sharing judgments add those capabilities; lexical packages alone establish none of them.

Source.

The passage between a second-class module and a first-class existential package is given in [Har16]. That comparison does not identify packages with the full ML module hierarchy, and neither do we.

Two record failures, two different missing judgments

Products can encode an ordered tuple, but label-based records expose a different problem. To make the failure exact, temporarily add a static fixed-record fragment with record types and two term forms: The finite label set has no duplicates. Its formation and typing rules are $$\frac{\mathrm{\Delta }⊢A_i::\mathsf{Ty}(i\in I)}{\mathrm{\Delta }⊢\{{\ell }_i:A_i{\}}_{i\in I}::\mathsf{Ty}}\mathrm{Rec}-\mathrm{F}\frac{\mathrm{\Delta };\mathrm{\Gamma }⊢e_i:A_i(i\in I)}{\mathrm{\Delta };\mathrm{\Gamma }⊢\{{\ell }_i=e_i{\}}_{i\in I}:\{{\ell }_i:A_i{\}}_{i\in I}}\mathrm{Rec}-\mathrm{I}$$ and $$\frac{\mathrm{\Delta };\mathrm{\Gamma }⊢e:\{{\ell }_i:A_i{\}}_{i\in I}j\in I}{\mathrm{\Delta };\mathrm{\Gamma }⊢e.{\ell }_j:A_j}\mathrm{Rec}-\mathrm{E}.$$ Its only new equality rule is componentwise equality after sorting labels: $$\frac{\mathrm{\Delta }⊢A_i\equiv B_i::\mathsf{Ty}(i\in I)}{\mathrm{\Delta }⊢\{{\ell }_i:A_i{\}}_{i\in I}\equiv \{{\ell }_i:B_i{\}}_{i\in I}::\mathsf{Ty}}\mathrm{Q}-\mathrm{Rec}.$$ We use this fragment only for static typing counterexamples; no record-value or operational theorem is claimed here. In particular, there is still no subtyping judgment.

The first failure asks for an unknown remainder. The intended type of record extension would have the following shape in a hypothetical higher-kinded extension with a row kind: $$\mathrm{\forall }\xi ::\mathsf{Row}.(\xi \mathrm{\backslash }\mathsf{secure})\Rightarrow \mathsf{Rec}(\xi )\to \mathsf{Rec}(\{\mathsf{secure}:{\mathsf{Bool}}_F\mid \xi \}).$$ Here $\Rightarrow$ is the qualified-type constraint arrow of chapter 4, not the relation lifting used in the preceding logical relation. This is not merely unprovable in $F_{\omega }$ plus fixed records: it is not a formed type. The kind grammar contains no $\mathsf{Row}$, the constructor grammar contains no row extension, and the judgments contain no lacks predicate. Quantifying over $c::\mathsf{Ty}\to \mathsf{Ty}$ does not create field selection or extension operations. The calculus of chapter 4 has a second syntactic sort of rows, row extension, and lacks predicates. Internalizing those ingredients here would add a kind $\mathsf{Row}$ and require the constructor metatheory to be rerun for it.

The second failure needs no unknown tail. As already previewed for the row calculus in subsection 7.8.3, define $$\mathsf{portOf}:\{\mathsf{port}:\mathbb{N}\}\to \mathbb{N},\mathsf{portOf}:=\lambda r:\{\mathsf{port}:\mathbb{N}\}.r.\mathsf{port},$$ and the closed larger record $$\mathsf{server}:=\{\mathsf{port}=\mathsf{0},\mathsf{secure}={\mathsf{true}}_F\}:\{\mathsf{port}:\mathbb{N},\mathsf{secure}:{\mathsf{Bool}}_F\}.$$ The application $\mathsf{portOf}\mathsf{server}$ fails. Its argument has the larger fixed record type, while T-App requires the exact domain $\{\mathsf{port}:\mathbb{N}\}$. The two sorted record constructors are distinct normal forms, so T-Conv cannot remove the extra field. A width relation would say that the larger record type is usable where the smaller one is expected; in general, proposes that $A$ is usable where $B$ is expected. Adding that width judgment and a subsumption rule would derive the application: width gives the displayed subtype premise, and subsumption changes the argument’s fixed record type to $\{\mathsf{port}:\mathbb{N}\}$. Neither nor subsumption belongs to the $F_{\omega }$ fragment of definition 7.31; constructor equality cannot derive the width premise. The missing term rule would take premises $\mathrm{\Gamma }⊢e:A$ and to $\mathrm{\Gamma }⊢e:B$.

The remedies are independent. Width subtyping forgets fields but does not name and preserve an unknown tail through extension. Row polymorphism names that tail but, without a subsumption rule, does not allow every fixed larger record wherever a smaller fixed record is expected.

Existential packages hide a constructor behind typed operations. Package preservation and progress establish the operational boundary; the higher-kinded logical relation proves representation independence for the two counter implementations. First-class selection is an ordinary consequence of native packages. Constructor equality still cannot forget a fixed record field; a subtype judgment and subsumption lie outside this calculus.