scala类型系统:柯里-霍华德同构

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

在这个系列之前的这篇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复合类型是类型AB的子类型:

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等于TU才行。

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

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

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

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

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

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

相当于:

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

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

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

scala类型系统:柯里-霍华德同构》上有6条评论

  1. Earthson Lu 陆云飞

    X =:= T //或
    X =:= U

    这个貌似有点问题。实际上这里能够协变的,应该是X <:< T Or X <: Nothing) => Nothing <: Nothing with U => Nothing) => Nothing

    X => Nothing >:> T => Nothing with U => Nothing

    于是我们得到 X <:< T Or X <:< U

    参数位置都是逆变位置。这个测试也得到它能接受协变参数(用AnyVal和String,能接受Double)。非常漂亮的形式Orz

    回复
  2. Earthson Lu 陆云飞

    我试了下,这样貌似也可以啊。

    type ¬[A] = A => Nothing
    type ∨[T, U] = ¬[T] with ¬[U]
    type |∨|[T, U] = { type λ[X] = (T ∨ U) <: i
    case s : String => s.length
    }

    我感觉这个主要就是用了函数类型的参数逆变来把关系的方向反转。

    回复
    1. Earthson Lu 陆云飞

      不好意思,代码没格式化。


      type ¬[A] = A => Nothing
      type ∨[T, U] = ¬[T] with ¬[U]
      type |∨|[T, U] = { type λ[X] = (T ∨ U) <: i
      case s : String => s.length
      }

      size(3)
      size("123")

      回复
      1. Earthson Lu 陆云飞

        type ¬[A] = A => Nothing
        type ∨[T, U] = ¬[T] with ¬[U]
        type |∨|[T, U] = { type λ[X] = (T ∨ U) <: i
        case s : String => s.length
        case h : Double => -1
        }

        size(3)
        size("123")

        回复
  3. Earthson Lu 陆云飞

    放弃了,不知道怎么保持代码结构。无效

    回复
  4. hongjiang 文章作者

    补充一下中文wiki地址:http://zh.wikipedia.org/wiki/%E6%9F%AF%E9%87%8C-%E9%9C%8D%E5%8D%8E%E5%BE%B7%E5%90%8C%E6%9E%84

    回复

发表评论

电子邮件地址不会被公开。 必填项已用*标注