ch:ml-modules: ch:ml-modules

Write the order package as $$O:=\mathsf{pack}[t,\mathsf{le}]:\mathrm{\exists }t:\mathsf{Ty}.t\to t\to \mathbf{2}.$$ If a set implementation is represented by $\mathsf{pack}[u,⟨\mathsf{empty},\mathsf{insert}⟩]$, the desired insert field has type $t\to u\to u$. That occurrence of $t$ is legal only inside $$\mathsf{unpack}[t,o]=O\mathsf{in}\mathsf{pack}[u,⟨\mathsf{empty},\mathsf{insert}⟩].$$ Returning this package would put the locally fresh $t$ in the result type, contradicting existential elimination’s no-escape premise. Giving the set an independent element witness loses the required equation. Replacing both witnesses by $\mathbb{N}$ restores the equation by revealing the representation, so it no longer implements the abstract interface.

Let $$\mathsf{leBool}:=\lambda b_1:\mathbf{2}.\lambda b_2:\mathbf{2}.\mathrm{\neg }{b}_1\vee b_2,p_B:=⟨\mathbf{2};\mathsf{leBool}⟩.$$ Rule Basic derives $$p_B:\mathsf{B}(s::\mathsf{Sing}(\mathbf{2});s\to s\to \mathbf{2})=\mathsf{ORDERED}[\mathbf{2}].$$ Transparent matching retains the singleton $s::\mathsf{Sing}(\mathbf{2})$, so a client may pass $\mathsf{true}$ to the comparison field. Opaque sealing instead derives $$p_B\upharpoonright \mathsf{ORDERED}:\mathsf{B}(s::\mathsf{Ty};s\to s\to \mathbf{2}).$$ The exported $s$ is abstract, and no judgment $s\equiv \mathbf{2}::\mathsf{Ty}$ is available. The same client application is therefore rejected.

The first component supplies the singleton equation $$X.s\equiv \mathbb{N}::\mathsf{Ty}.$$ The second component of $\mathsf{ORDSET}$ consequently specializes to $\mathsf{SET}[\mathbb{N}]$. Matching $p_B:\mathsf{SET}[\mathbf{2}]$ against it also requires $$X.s\equiv \mathbf{2}::\mathsf{Ty}.$$ The two equations would imply $\mathbb{N}\equiv \mathbf{2}::\mathsf{Ty}$, which constructor equivalence cannot derive. Thus Sigma-Match fails at its second premise; the ordinary dynamic operations of the two components are irrelevant.

Bind two separately sealed applications $S_i=\mathsf{SetFn}(p_O)$. Both applications are specialized at $p_O:\mathsf{ORDERED}[\mathbb{N}]$, so both interface element parameters are $\mathbb{N}$. Opaque sealing nevertheless allocates distinct representation identities: no judgment $S_1.s\equiv S_2.s$ is derivable even though both bodies use lists. A hierarchy sharing exactly the element type is $$\mathsf{Sigma}(X:\mathsf{ORDERED}[\mathbb{N}]).\mathsf{Sigma}(S_1:\mathsf{SET}[X.s]).\mathsf{SET}[X.s].$$ The two set components mention the same path $X.s$, but each basic set signature binds its own abstract representation constructor.

At the manifest argument, Pi-Match compares the domain contravariantly and then specializes the result to $\mathsf{SET}[\mathbb{N}]$; Sub applies the match. The source calculation is Substituting that value in the annotated let gives The target application binds the translated argument once and opens it before translating the body: The translated let opens this package. Its dynamic projection is $$\mathsf{unpack}[r,x]=\mathsf{pack}[\mathsf{List}\mathbb{N};q]\mathsf{in}x\stackrel{\mathrm{\exists }-\beta }{⟶}q,$$ after which the same product projections select $\mathsf{nil}$ and ${\mathsf{member}}_{p_O}$. If the annotated result type mentioned $S.s$, the witness $r$ opened for $S$ would occur free in that result type. The existential-elimination no-escape premise would then fail, which is why the supported translation requires the displayed closed result.

Take $$K(z,\mathsf{step},\mathsf{read}):=\mathsf{read}(\mathsf{step}(\mathsf{step}(\mathsf{step}z))).$$ For $C_N$, the successive states are $0,1,2,3$, so the result is $3$. For $C_P$, they are $$⟨0,\star ⟩,⟨1,\star ⟩,⟨2,\star ⟩,⟨3,\star ⟩,$$ and the observer again returns $3$. If abstract equality were exported, the logical relation would additionally have to satisfy $$R(n,p)\wedge R(n^{\prime },p^{\prime })⟹{\mathsf{eq}}_N(n,n^{\prime })={\mathsf{eq}}_P(p,p^{\prime }).$$ Without this operation clause the fundamental-relation induction has no case for the new constant.

The basic clause gives $$\mathsf{psig}({\mathsf{NatOrder}}_0)=\mathsf{B}(s::\mathsf{Sing}(\mathbb{N});\mathbb{N}\to \mathbb{N}\to \mathbf{2}).$$ If $p_S=⟨\mathsf{List}\mathbb{N};v_S⟩$, the hierarchy clause and singleton propagation give $$\mathsf{Sigma}{(}_{:}\mathsf{psig}({\mathsf{NatOrder}}_0)).\mathsf{B}(r::\mathsf{Sing}(\mathsf{List}\mathbb{N});\mathsf{pty}(v_S)).$$ An opaque seal is excluded from the grammar of projectible paths because it forgets static identity. The generative application $\mathsf{SetFn}({\mathsf{NatOrder}}_0)$ is also nonprojectible. Neither has a clause in definition 12.12; inspecting either body would manufacture precisely the identity that the boundary hides or generates. If another signature is proposed as least for either projectible example, leastness yields matches in both directions between it and the displayed $\mathsf{psig}$; the selected calculus supplies no antisymmetry rule that would turn those two matches into judgmental equality.

Within the selected $\alpha$-small relation fibers, the functorial action is pointwise, so the two witnesses become $$w_{\mathsf{round}}(r_j)=w_{\mathsf{pack}}(w_{\mathsf{unpack}}(r_j))(j\in \{1,2\}).$$ The output witnesses need not be equal: proof relevance records the chosen input witness and the two maps applied to it. Under $\mathsf{bst}$, the dynamic round-trip functions are identified; the output still has the input static type components $X_0,X_1$ and the tracked family $\tilde{X}$ between them. If relation fibers are truncated to propositions, both $r_1$ and $r_2$ become the same mere fact of relatedness, and the distinction between the two displayed outputs is erased.

The counter theorem’s proposition is $R(n,⟨m,\star ⟩)$. It is defined externally inside a simply typed logical relation. That calculus has no internal $\mathsf{bst}$, no static-extent signature, no family of witness sets, and no model of phase-separated parametricity. Therefore its proof has the same broad shape as representation independence, but does not instantiate the hypotheses of the imported ModTT theorem.

In Crary’s comparison calculus, two ordinary avoiding answers may retain the four visible fields while choosing respectively $$D:\mathsf{int}u\to v\text{and}D:\mathsf{bool}u\to v.$$ The first types $Dx$ but not $Dy$; the second types $Dy$ but not $Dx$. Each therefore exposes a fact unavailable from the other, so neither subsigns the other.

The least answer in the extended signature language is $$\mathrm{\exists }t.\mathsf{sig}\{\mathsf{type}{}^{\prime }au=t;\mathsf{datatype}v=D\mathsf{of}t;x:\mathsf{int}u;y:\mathsf{bool}u\}.$$ The leading $\mathrm{\exists }t$ binds the generated name throughout the four-field signature and prevents it from escaping. This answer belongs to Crary’s existential-signature extension, not to definition 12.1.

Let $\mathsf{MAP}[a]$ bind a private representation and operations on keys of type $a$. Use the hierarchy $$\mathsf{Sigma}(O:\mathsf{ORDERED}).\mathsf{Sigma}(S:\mathsf{SET}[O.s]).\mathsf{MAP}[O.s].$$ A natural-number implementation matches with $O.s\equiv \mathbb{N}$, a set representation $\mathsf{List}\mathbb{N}$, and an independent map representation such as $\mathsf{List}(\mathbb{N}\times \mathsf{String})$. The two representation paths are unrelated. Replacing the map by $\mathsf{MAP}[\mathbf{2}]$ requires both $O.s\equiv \mathbb{N}$ and $O.s\equiv \mathbf{2}$, so matching fails at $\mathbb{N}\not\equiv \mathbf{2}::\mathsf{Ty}$.

After matching both counter components to a closed result, use the hierarchy signature $$\mathsf{Sigma}{(}_{:}\mathsf{COUNTER}).\mathsf{COUNTER}.$$ Its target is $\mathsf{Pack}(\mathsf{COUNTER})\times \mathsf{Pack}(\mathsf{COUNTER})$, and the hierarchy translates to $⟨P_1,P_2⟩$. The second dynamic projection reduces by where $P_2=\mathsf{pack}[t_2,v_2]$. If the source second component was written using the first path, matching must first replace that path by its manifest constructor. Otherwise $P_2$’s type contains the witness opened for $P_1$, so returning the pair violates no-escape and lies outside theorem 12.7.

With the temporary App-P and Seal-P rules, an applicative result can be recognized only from stable syntax. The corresponding principal clause is $$\mathsf{psig}(F(A))={\sigma }_2[A/X]$$ when $$\mathsf{psig}(F)=\mathsf{Pi}(X:{\sigma }_1).{\sigma }_2,\mathsf{psig}(A){⪯}_{\mathsf{s}}{\sigma }_1,$$ and equality of two such result paths requires equality of both the functor paths and the argument values. That information is absent from the four structural clauses of definition 12.12.

For the extended phrase $\mathsf{if}b\mathsf{then}{M}_1\mathsf{else}{M}_2$, the runtime Boolean $b$ is not a projectible functor path or a module value. Neither App-P nor Seal-P derives projectibility for the conditional, even when both branches have the same signature. Thus it has no stable applicative identity without an additional, unsound inspection of runtime control flow.