存在类型

形式陈述 ​

存在类型 $\mathrm{\exists }\alpha .T$ 的值包含一个见证类型 $A$ 和一个接口值，其具体类型为 $T[A/\alpha ]$。引入形式 pack 的类型规则公理库类型判断Typing judgment在上下文中断言项具有某类型的形式判断。可写为

$$\frac{\mathrm{\Gamma }⊢v:T[A/\alpha ]}{\mathrm{\Gamma }⊢\mathsf{pack}[A,v]\mathsf{as}\mathrm{\exists }\alpha .T:\mathrm{\exists }\alpha .T}.$$

接口 $T$ 对外保留，见证 $A$ 被封装。消去形式 unpack 的规则为

$$\frac{\mathrm{\Gamma }⊢e_1:\mathrm{\exists }\alpha .T\mathrm{\Gamma },\alpha \mathsf{type},x:T⊢e_2:U\alpha \notin \mathrm{FV}(\mathrm{\Gamma },U)}{\mathrm{\Gamma }⊢\mathsf{unpack}[\alpha ,x]=e_1\mathsf{in}{e}_2:U}.$$

打开包时，$\alpha$ 是作用域内新鲜的抽象类型名，$x$ 只能按接口 $T$ 使用。侧条件 $\alpha \notin \mathrm{FV}(U)$ 禁止结果类型泄露隐藏见证；它不是排版细节，而是封装成立的关键。运行时，已知包可按

$$\mathsf{unpack}[\alpha ,x]=(\mathsf{pack}[A,v])\mathsf{in}e⟶e[A/\alpha ][v/x]$$

消去；实现若擦除类型，运行步骤只需传递值，但静态新鲜性仍必须先由类型系统保证。声明式规则说明哪些程序合法，类型检查算法则负责管理新鲜类型变量、作用域和替换，二者不应与这条运行归约混为同一种机制。

在 impredicative System F公理库System FSystem F · Polymorphic lambda calculus具有显式类型抽象与类型应用的二阶多态 λ 演算。 中，存在类型可作 Church 编码

$$\mathrm{\exists }\alpha .T\cong \mathrm{\forall }\beta .(\mathrm{\forall }\alpha .T\to \beta )\to \beta .$$

这个编码把使用包的客户端作为续接传入，说明存在量化与全称量化的对偶直觉；它依赖相应的多态能力，不能反过来当作所有语言原生 pack/unpack 的定义或运行规则。

直觉 ​

存在包对客户端说：“确实有某个表示类型能实现这份接口，但你不需要、也不允许知道它是谁。”包的生产者选择见证并提供操作，消费者只能让这些操作接收或返回同一个抽象类型。隐藏的不是一个运行时随机选择，而是类型身份；每次打开包都以新鲜名字代表那项未知身份。

全称类型要求程序能接受客户端选择的任意类型，存在类型则允许实现者选择一个类型后将其隐藏。两者都利用参数化公理库参数多态Parametric polymorphism程序对类型参数统一工作而不依赖其具体表示的多态。限制程序依赖的类型信息，但控制选择权的一方相反。

例子与边界 ​

集合模块的接口可写成

$$\mathrm{\exists }Rep.\{\mathsf{empty}:Rep,\mathsf{insert}:Int\to Rep\to Rep,\mathsf{member}:Int\to Rep\to Bool\}.$$

一个实现可取排序数组为 $Rep$，另一个可取平衡树。客户端打开任一包后，能从该包的 empty 开始，经 insert 构造表示，再交给同一包的 member；它不能索引数组、旋转树或检查表示标签，因为接口没有暴露这些操作。

两个包分别打开时得到两个新鲜抽象类型，因而不能把第一个包产生的 $Re{p}_1$ 值交给第二个包期待的 $Re{p}_2$ 操作，即使生产者碰巧都使用数组。这与和类型公理库和类型Sum type · Variant type其值从若干带标签分支中选择一个的类型。不同：和类型公开有限的分支选择并允许模式匹配，存在类型刻意隐藏见证身份，客户端没有按见证类型分支的规则。

封装类型名也不自动证明两个实现行为等价。若树实现的 member 总返回 false，它仍可能满足表面的函数类型。表示独立还需要抽象不变量或逻辑关系证明各导出操作保持预期行为；存在类型只提供隐藏机制。

推论与应用 ​

存在类型为模块、插件与抽象对象提供类型论模型：实现可以更换内部表示，只要重新打包后仍满足同一接口。它也解释了为什么某些状态必须连同操作一起封装；若单独泄露一个隐藏表示值，客户端既无法构造同类型的新值，也无法安全选择别的包来处理它。

存在包的作用域纪律支持信息隐藏，但接口设计仍决定可观察能力。若接口暴露指针身份、遍历顺序、异常或计时信息，这些都成为客户端可用的观察，不能再仅凭类型隐藏声称实现不可区分。

参考资料

• John C. Mitchell and Gordon D. Plotkin, “Abstract Types Have Existential Type,” ACM TOPLAS 10(3), 1988。
• Benjamin C. Pierce, Types and Programming Languages, MIT Press, 2002，Ch. 24, existential types。
• Robert Harper, Practical Foundations for Programming Languages, 2nd ed., Cambridge University Press, 2016，abstract types and modularity。