存在类型 | Codeboy's Blog

形式陈述

存在类型 $\exists\alpha.T$ 的值包含一个见证类型 $A$ 和一个接口值，其具体类型为 $T[A/\alpha]$ 。引入形式 pack 的类型规则可写为

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

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

\frac{ \Gamma\vdash e_1:\exists\alpha.T \qquad \Gamma,\alpha\ \mathsf{type},x:T\vdash e_2:U \qquad \alpha\notin\operatorname{FV}(\Gamma,U) }{ \Gamma\vdash \mathsf{unpack}\,[\alpha,x]=e_1\ \mathsf{in}\ e_2:U }.

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

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

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

在 impredicative System F 中，存在类型可作 Church 编码。选取不自由出现于 $T$ 的新鲜答案类型变量 $\beta$ ，编码目标为

\forall\beta.(\forall\alpha.T\to\beta)\to\beta.

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

直觉

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

全称类型要求程序能接受客户端选择的任意类型，存在类型则允许实现者选择一个类型后将其隐藏。两者都利用参数化限制程序依赖的类型信息，但控制选择权的一方相反。

例子与边界

集合模块的接口可写成

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

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

两个包分别打开时得到两个新鲜抽象类型，因而不能把第一个包产生的 $Rep_1$ 值交给第二个包期待的 $Rep_2$ 操作，即使生产者碰巧都使用数组。这与和类型不同：和类型公开有限的分支选择并允许模式匹配，存在类型刻意隐藏见证身份，客户端没有按见证类型分支的规则。

封装类型名也不自动证明两个实现行为等价。若树实现的 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。