所谓的联合类型(union type)，在逻辑上是“或”的意思，如A or B or C。
假设我们想实现这样一个函数size，它可以计算一个联合类型对象（Int与String）的长度。我们期望size函数只接受Int类型或String类型（以及它们的子类型，如Null和Nothing）的对象，而不接受任何其他类型的对象：
1 2 3 4 5 6 7 8
| def size(x: Int ∨ String) = x match { case i: Int => i case s: String => s.length } size(24) == 24 size("fuck") == 4 size(1.0)
|
Scala中的Either类型可以提供一种不支持子类型的联合类型。举个例子，用Either实现size函数：
1 2 3 4 5 6 7 8
| def size(x: Either[Int, String]) = x match { case Left(i) => i case Right(s) => s.length } size(Left(24)) == 24 size(Right("fuck")) == 4 size(Left("lv"))
|
我们可以观察出一个问题，那就是要使用Either类型就不可避免要把对象包装成Either类型（Left或Right），这是不方便的。我们需要一些奇技淫巧来实现一个原生类型版本(unboxed)的size函数，这就是下面要介绍的Curry-Howard Isomorphism（柯里-霍华德同构）。
Curry-Howard Isomorphism
Curry-Howard Isomorphism 通过命题表示了计算机程序与数理逻辑之间的直接联系(逻辑上的等价关系)，即我们可以利用数理逻辑中的某些东西来去表示程序中的特定逻辑。比如在Curry-Howard 同构中，有以下的等价关系：
| 含义 |
类型系统(Scala) |
命题逻辑 |
| 联合类型（并，析取） |
A ∨ B（∨为自定义的析取类型） |
A ∨ B |
| 交集类型（交，合取） |
A with B |
A ∧ B |
| 子类型（蕴含） |
A <: B |
A ⇒ B |
因此联合类型可以表示为析取式，如P ∨ Q ∨ R。
那么如何根据Curry-Howard 同构实现一个析取类型呢？我们可以先利用德摩根定律(De Morgan’s laws)做一个转化。已知德摩根定律：
用Scala代码就可以表示为：
1
| (A ∨ B) =:= ¬[¬[A] with ¬[B]]
|
这样，问题就转化成了如何实现一个否定类型(¬)。我们从另一个角度去利用Curry-Howard 同构。在类型系统理论中，存在以下等价关系：
| 类型 |
Scala Type |
对应命题逻辑 |
| Sum Type |
A ∨ B（∨为自定义的析取类型） |
析取(A ∨ B) |
| Product Type |
(A, B) |
合取(A ∧ B) |
| Function Type |
Function1[A, B] |
蕴含(A ⇒ B) |
再根据以下的等价关系：
我们就可以写出Scala中对应的类型：
这样我们就可以定义两个类型：
1 2
| type ¬[A] = A => Nothing type ∨[T, U] = ¬[¬[T] with ¬[U]]
|
在REPL里测试一下：
1 2 3 4 5 6 7 8 9
| scala> type ¬[A] = A => Nothing defined type alias $u00AC scala> type ∨[T, U] = ¬[¬[T] with ¬[U]] defined type alias $u2228 scala> implicitly[Int <:< (Int ∨ String)] <console>:13: error: Cannot prove that Int <:< ∨[Int,String]. implicitly[Int <:< (Int ∨ String)]
|
嗯？哪里出问题了？我们来分析一下(Int ∨ String)这个类型：
1 2
| scala> :k ∨[Int, String] scala.Function1's kind is F[-A1,+A2]
|
原来(Int ∨ String)的类型是函数类型，也就是说我们创造的Union Type是函数类型，那Int类型自然不是(Int ∨ String)的子类型了，因为它连函数类型都不是。我们需要将<:<操作符左边的类型转化成函数类型，比如双重否定类型（逻辑上相当于原类型，但其类型为函数类型）：
再测试一下：
1 2 3 4 5 6 7 8 9 10 11 12
| scala> type ¬¬[A] = ¬[¬[A]] defined type alias $u00AC$u00AC scala> implicitly[¬¬[Int] <:< (Int ∨ String)] res2: <:<[¬¬[Int],∨[Int,String]] = <function1> scala> implicitly[¬¬[String] <:< (Int ∨ String)] res3: <:<[¬¬[String],∨[Int,String]] = <function1> scala> implicitly[¬¬[Double] <:< (Int ∨ String)] <console>:14: error: Cannot prove that ¬¬[Double] <:< ∨[Int,String]. implicitly[¬¬[Double] <:< (Int ∨ String)]
|
成功了！¬¬[Int]和¬¬[String]都是∨[Int,String]的子类型。把Int换成Double，无法通过编译。下面我们就可以利用隐式转换实现我们的size函数了：
1 2 3 4
| def size[T](t: T)(implicit ev: (¬¬[T] <:< (Int ∨ String))) = t match { case i: Int => i case s: String => s.length }
|
测试一下，结果very good～
1 2 3 4 5 6 7 8 9 10
| scala> size(24) res5: Int = 24 scala> size("Scala") res6: Int = 5 scala> size(6.666) <console>:15: error: Cannot prove that ¬¬[Double] <:< ∨[Int,String]. size(6.666) ^
|
最后还可以用type lambda来简化函数的参数，省掉implicit：
1 2 3 4 5 6 7
| type |∨|[T, U] = { type λ[X] = ¬¬[X] <:< (T ∨ U) } def size[T: (Int |∨| String)#λ](t: T) = t match { case i: Int => i case s: String => s.length }
|
所以我们union type及size函数的最终实现为：
1 2 3 4 5 6 7 8 9
| type ¬[A] = A ⇒ Nothing type ∨[T, U] = ¬[¬[T] with ¬[U]] type ¬¬[A] = ¬[¬[A]] type |∨|[T, U] = { type λ[X] = ¬¬[X] <:< (T ∨ U) } def size[T : (Int |∨| String)#λ](t : T) = t match { case i : Int ⇒ i case s : String ⇒ s.length }
|
总结一下，整个过程的本质都是在进行类型推导和证明，因此我们可以将Curry-Howard Isomorphism理解为类型证明即程序。
其实类型系统还有很多好玩的东西，比如dependent type。。后边可以用Scala玩玩~
References
