存在类型

在多态类型论中, 存在类型是全称类型的对偶, 也可以类比为依值类型论中$\Sigma$ 类型的对应物、谓词逻辑中存在量词的对应物, 记作$$\exists x.\alpha$$其中 $\alpha$ 是可以使用 $x$ 这个类型变量的类型.

换言之, 要给出一存在类型的实例, 只需要给出任意值并配上它的类型即可.

1类型规则

形成规则依定义可以直接看出:$$\frac{\Sigma ,x⊢\alpha }{\Sigma ⊢\exists x.\alpha }$$构造规则需要指出 $x$ , 并给出 $\alpha$ 在替换 $x$ 后的实例:$$\frac{\Sigma ⊢\rho \Sigma ;\Gamma ⊢u:\alpha [x:=\rho ]}{\Sigma ;\Gamma ⊢⟨\rho ,u⟩:\exists x.\alpha }$$消去规则类似极性为正的积类型的消去规则,$$\frac{\Sigma ;\Gamma ⊢u:\exists x.\alpha \Sigma ,x;\Gamma ,y:x⊢e:\rho }{\Sigma ;\Gamma ⊢{\mathsf{uncurry}}_{\rho }(u,x.y.e):\rho }$$计算规则执行必要的代换:$${\mathsf{uncurry}}_{{\rho }^{\prime }}(⟨\rho ,u⟩,x.y.e)=e[x:=\rho ,y:=u]$$

$\lambda$ 编码

在 F 系统中, 可以使用全称类型编码存在类型:

$$\begin{array}{lll}& \exists x.\alpha & ::=\forall u.(\forall x.\alpha \to u)\to u\\ & ⟨\rho ,e⟩& ::=\Lambda u.\lambda c.c[\rho ](e)\\ & {\mathsf{uncurry}}_{\rho }(u,x.y.e)& ::=u[\rho ](\Lambda x.\lambda y.e)\end{array}$$

2性质

不同于$\Sigma$ 类型, 存在类型的极性是正的, 并且不是负的.

3例子

假如 $\alpha ⊢\mathrm{List}(\alpha )$ 表示 “类型为 $\alpha$ 的值组成的序列 (又叫列表)”, 那么:

•	$u:\exists x.\mathrm{List}(x)$ 中, 元素的类型均相同, 具体是什么只能等到确定 $u$ 的具体值时才能知道.

•	$u:\mathrm{List}(\exists x.x)$ 中, 每个元素都打包了它们自己的类型, 因此可以各不相同.

4相关概念

•	全称类型和多态类型论,

•	$\Sigma$ 类型和存在量词是存在类型的异时空同位体.

术语翻译

存在类型 • 英文 existential type