类型系统 | Existential Type | Scala ++ Java ++ Haskell

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关键字)。举个例子:

简单表示 完整表示 含义
Seq[_] Seq[T] forSome {type T} T可以是Any类型的任意子类
Seq[_ <: A] Seq[T] forSome {type T <: A} T可以是A类型的任意子类
Seq[_ >: Z <: A] Seq[T] forSome {type T >: Z <: A} T可以是A类型的任意子类,同时需要是Z类型的父类

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

下面我们来探究一下existentialforall的真正含义。我们可以将类型看作是某些值的集合,比如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

文章目录
  1. 1. Existential type in Java
  2. 2. Existential type in Scala
  3. 3. Existential type in Haskell
  4. 4. Heterogeneous List
  5. 5. References