通过柯里-霍华德同构实现联合类型
在这个系列之前的这篇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)即程序。