所谓的联合类型(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