Existential type (存在类型)提供了一种在类型系统上抽象的方式，其中 existential type 这个名称源于 existential quantification (存在量词，数学符号∃)。可以这样理解：某种形式的类型存在，但是在上下文中不知道它的具体类型。比如我们定义一种类型 type T = ∃x {a: x; f: (x => Int);}，它可以表示这种类型有一个类型为 x 的成员变量a，一个类型为 x => Int 的成员函数 f，而类型 x 是任意的。

这篇文章我们来探讨一下 existential type 在 Java、Scala 和 Haskell 中的运用。

Existential type in Java

Existential Type 在 Java 如此烂的类型系统中发挥着重要的作用。Java 泛型中的 Wildcards(占位符)其实就是一种existential type，比如 java.util.List<?>。

由于JVM在编译时会对type parameters进行类型擦除，让它们回归为raw types，因此很多人认为existential type就相当于raw types，比如List =:= List<?>，这是不正确的。它们两种类型最大的区别就是existential type是type safe的，而raw types则不是。在将一个具化的泛型扒掉所有的type parameters的时候，后者是不安全的。我们测试一下：

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24

import java.util.Arrays;
import java.util.List;
import java.util.ArrayList;
public class Existential {
	public static List<String> list = new ArrayList<>(Arrays.asList("Java", "sucks"));
	public static void t1() {
		List a = list;
		a.forEach(System.out::println);
	}
	public static void t2() {
		List<?> b = list;
		b.forEach(System.out::println);
	}
	public static void main(String[] args) {
		t1();
		t2();
	}
}

编译一下，编译器会提示t1方法不安全，而t2则无警告：

1
2
3
4
5
6
7

λ javac ./Existential.java -Xlint:unchecked
./Existential.java:11: 警告: [unchecked] 对作为原始类型Iterable的成员的forEach(Consumer<? super T>)的调用未经过检查
                a.forEach(System.out::println);
                         ^
  其中, T是类型变量:
    T扩展已在接口 Iterable中声明的Object
1 个警告

因此我们要避免使用原始类型。(貌似越写越偏了。。那就顺便总结一下Java的Bounded Wildcards吧:)

Java通过 Bounded Wildcards（限定通配符）来实现有限的可变性(variance)，比如

• List<? extends Object>（协变, covariance）
• List<? super User>（逆变, contravariance）
• List<?>（不可变, invariance）

注意我们无法给限定通配符的List添加任何对象，因为它的类型参数无法确定（这即是existential的含义）。我们可以在方法参数中使用Bounded Wildcards来达到协变和逆变的效果，使用时遵循 PECS原则 (Producer Extends, Consumer Super)。

注：这里的variance其实是一种 use-site variance，后边有时间探究一下它与 declaration-site variance 的区别。

Existential type in Scala

Scala同样兼容Java的这种use-site variance，语法有两种。一种和Java类似，一种是完整表示方法（forSome关键字）。举个例子：

Existential type in Haskell

在GHC中使用Existential Types需要开启扩展(-XExistentialQuantification)。Haskell中的Existential Type通过forall关键字来实现。但是，forall代表全称量词∀，这似乎和existential type的含义是对立的，是不是很神奇呢？我们将在稍后解释。这里我们先来看一下我们最熟悉的map函数：

1

map :: (a -> b) -> [a] -> [b]

我们还可以通过全称量化的方法构造map：

1

map :: forall a b. (a -> b) -> [a] -> [b]

这两个map的定义是等价的。其实在Haskell中，很多类型的定义都是隐式地使用了forall。

再比如下边的例子定义了可以show的existential type：

1
2
3
4
5
6
7
8
9
10
11
12
13
14

{-# LANGUAGE ExistentialQuantification #-}
data ShowObj = forall a. Show a => S a
instance Show ShowObj where
	show (S a) = show a
li :: [ShowObj]
li  = [S 1, S "Java", S "sucks", S True, S ()]
f :: [ShowObj] -> IO ()
f xs = mapM_ print xs
main = f li

下面我们来探究一下existential和forall的真正含义。我们可以将类型看作是某些值的集合，比如Bool类型对应集合{True, False, ⊥}，Integer对应数的集合。注意bottom(⊥)属于每一个类型。

forall代表这些集合的交集。我们举一些例子：

• forall a. a是所有类型的交集，也就是{⊥}
• [forall a. Show a => a]代表一种所含元素均为forall a. Show a => a类型的列表类型，Show Typeclass限定了只能在Show的instance里取交集

我们随便定义一个existential datatype(下面我们用∀代替forall，用∃代替exists)：

1

data T = ∀ a. MkT a

其中MkT的含义是产生一个T类型：

1
2

MkT :: forall a. a -> T
MkT :: a -> T {- 等价 -}

那么当我们对MkT进行解构的时候又会发生什么呢？比如进行模式匹配的时候：

1

f (MkT x) = ...

此时x的类型可以是任意的，也就是说我们可以用存在量词来表示x：x :: ∃ a. a。我们知道存在这种类型x，但不清楚x的真正类型。这样的定义同构于上边我们用全称量词的定义，即这两种定义等价：

1
2
3

data T = ∀ a. MkT a
data T = MkT (∃ a. a)

而Haskell选择了前者的表达方式(forall)，即在Haskell中existential type通过forall关键字来实现。（为何不用exists？我也不清楚。。）

所以现在再回头来看我们之前定义的ShowObj类型，我们可以把它转化为用存在量词表达的existential type:

1
2
3

data ShowObj = forall a. Show a => S a
data ShowObj' = S' (exists a. Show a => a) {- Haskell里不能这么写 -}

在Haskell各种类库中existential type用的非常多，例如Control.Monad.ST中的runST：

1

runST :: forall α. (forall s. ST s α) -> α

这里先不展开写了，后边有时间多实践实践再说。。。

Heterogeneous List

待填坑。。Miles Sabin大神的Shapeless库中的 Heterogeneous List(HList) 值得一读。。

References

• Scala Language Specification, 3.2.10
• Haskell/Existentially quantified types
• GHC Users Guide, 9.4.6. Existentially quantified data constructors
• Typelevel - Existential types are not raw types