通过柯里-霍华德同构实现联合类型

在这个系列之前的这篇blog scala类型系统：10) 交集类型与联合类型 里曾提到过实现union类型的另一种方式是柯里-霍华德同构

这段代码是从这里看到的：

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
}

scala> size(3)
res0: Int = 3

scala> size("three")
res1: Int = 5

要理解这段类型证明，先要了解复合类型，结构类型，函数类型的逆变，类型投影，以及type-lambda等，这些点可以从之前的blog里参考。

对于普通的class来说，A with B复合类型是类型A或B的子类型:

scala> import scala.reflect.runtime.universe._

scala> class A; class B;

scala> typeOf[A with B] <:< typeOf[A]
res0: Boolean = true

但对于函数类型，因为其参数类型是逆变的，所以情况正好反过来：

scala> typeOf[ A=>Nothing ] <:< typeOf[ (A with B)=>Nothing ]
res1: Boolean = true

用图来看：

 __________               _________________________ 
|          |             |                         |
|     A    |             |  (A with B) => Nothing  |
|__________|             |_________________________|
      ^                               ^ 
      |                               | 
 __________               _________________________ 
|          |             |                         |
| A with B |             |        A => Nothing     |
|__________|             |_________________________|  

所以，我们把上文中定义的：¬[¬[A]] 和 ¬[¬[T] with ¬[U]] 两个表达式展开的话，会发现这两个函数类型是有继承关系的(如果参数类型A与T或U相同的话)：

//¬[¬[A]]
scala> type T1 = (A=>Nothing) => Nothing  

//¬[¬[T] with ¬[U]]
scala> type T2 = ((A=>Nothing) with (B=>Nothing)) => Nothing  

scala> typeOf[T1] <:< typeOf[T2]
res3: Boolean = true

然后定义了一个结构类型：

type |∨|[T, U] = { type λ[X] = ¬¬[X] <:< (T ∨ U) }

这个结构类型里的λ是一个类型工厂，当传入给它某个类型参数时，它会构造出一个新的类型 ¬¬[X] <:< (T ∨ U) ，这个是中缀写法，还原成普通类型写法是: <:<[¬¬[X], (T ∨ U)] 关于 <:< 这个类型是用于约束两个类型关系的，它是在Predef里定义的:

sealed abstract class <:<[-From, +To] extends (From => To) with Serializable

它要求 ¬¬[X] 是类型 T v U (即v[T,U])的子类型。

而这个要求，我们前边证明 ¬[¬[X]] 和 ¬[¬[T] with ¬[U]] 的关系时已经论证过了，当类型参数X与T或U一致时即：

// 只有当
X =:= T //或 
X =:= U 

//下面的约束才成立
¬¬[X] <:< (T ∨ U) 

那么现在来单独用λ这个类型构造器，它的表达方式为 (T |v| U)#λ，这是一段type-lambda，它描述的是一个构造器类型，它可以由类型参数X，构造出一个复杂的约束类型:

<:<[(X=>Nothing)=>Nothing, ((T=>Nothing) with (U=>Nothing))=>Nothing]

这个约束类型能够编译通过的前提如前边所说，需要X等于T或U才行。

现在我们把用一个具体的，由Int和String类型参数构造的 |∨|[Int, String] 类型中的λ类型构造器用Factory来表示：

type Factory[T] = (Int |∨| String)#λ[T]

这个Factory类型构造器，对于任何类型参数 T，构造出的类型展开后为:

<:<[(T=>Nothing)=>Nothing, ((Int=>Nothing) with (String=>Nothing))=>Nothing]

也就是说T必须是Int或String才能满足。最后用隐式参数的方式(context bound)在方法定时时描述这种约束

def size[T: Factory](p: T) = ...

相当于：

def size[T](p: T)(implicit ev: Factory[T]) ...

如果你纳闷这个ev隐式参数是哪里来的，参考一下以前的这篇: scala类型系统：22) 类型约束与特定方法

整个过程只涉及到类型证明，与以前的实现方式对比不需要显式提供任何隐式转换或隐式参数(只用到了语言默认提供的一个隐式参数)，也没有创建任何“单例”或“实例对象”，柯里-霍华德同构可以简单理解为类型证明(type-lambda)即程序。