scala类型系统:28) 依赖类型

依赖类型是用在type class模式中的一种场景,当type class中存在多个类型参数时,某个类型参数可以由其他类型参数来决定。

这个概念是从shapeless作者的blog里看到的,依赖类型也是源自haskell的一种扩展

Functional dependencies are a near-standard extension to Haskell (present in GHC and elsewhere) which allow constraints on the type parameters of type classes to be expressed and then enforced by the compiler.They allow the programmer to state that some of the type parameters of a multi-parameter type class are completely determined by the others.

先看一下他举的例子,假设矩阵类型与矢量类型以及Int类型在做笛卡尔乘积运算时,结果类型取决于这两者的组合:

Matrix  *   Matrix  -> Matrix  //矩阵 * 矩阵 得到 矩阵
Matrix  *   Vector  -> Vector  //矩阵 * 矢量 得到 矢量
Matrix  *   Int     -> Matrix  //矩阵 * Int 得到 矩阵 
Int     *   Matrix  -> Matrix  //Int * 矩阵 得到 矩阵

因为结果类型受入参类型的约束,我们在设计函数时,可以把结果类型约束为满足这种组合的情况,用scala来实现

scala> trait Matrix 

scala> trait Vector

scala> trait MultDep[A, B, C] //定义一个笛卡尔运算时需要依赖类型,用于约束结果类型

我们通过隐式对象提供各种类型的组合时的依赖类型:

scala> implicit object mmm extends MultDep[Matrix, Matrix, Matrix]
scala> implicit object mvv extends MultDep[Matrix, Vector, Vector]
scala> implicit object mim extends MultDep[Matrix, Int, Matrix]
scala> implicit object imm extends MultDep[Int, Matrix, Matrix]

检验一下隐式对象:

scala> implicitly[MultDep[Matrix, Matrix, Matrix]] // OK: Matrix * Matrix -> Matrix
scala> implicitly[MultDep[Matrix, Vector, Vector]] // OK: Matrix * Vector -> Vector
scala> implicitly[MultDep[Matrix, Vector, Matrix]] // Error 没有定义过这种组合

现在在笛卡尔积的方法上增加这个隐式参数,来限制参数类型和结果类型必须符合我们的组合要求:

def mult[A, B, C](a : A, b : B)(implicit instance : MultDep[A, B, C]) : C =
{ 
    null.asInstanceOf[ C ]
}

这样我们在运行mult方法时,当传入的参数类型不符合我们用隐式对象提供的组合时,编译器直接会帮我们检查出来:

val r1 : Matrix = mult(new Matrix {}, new Matrix{}) // Compiles
val r2 : Vector = mult(new Matrix {}, new Vector{}) // Compiles
val r3 : Matrix = mult(new Matrix {}, 2)            // Compiles
val r4 : Matrix = mult(2, new Matrix {})            // Compiles
val r5 : Matrix = mult(new Matrix {}, new Vector{}) // 错误,结果类型应该是Vector

在scala的集合库中,当从一种类型的集合转换到另一种类型的集合时,比如执行mapto方法时会调用CanBuildFrom这个隐式参数来判断当前类型是否可转换为目标类型:

def map[B, That](f: A => B)(implicit bf: CanBuildFrom[Repr, B, That]): That = {
    val b = bf(repr)
    b.sizeHint(this)
    for (x <- this) b += f(x)
    b.result
}

这个CanBuildFrom type class 里面有三个类型参数:Repr, B, That

而这三个类型其实是有依赖的关系的,即 That 类型,是由ReprB类型决定的:

// 由 List[_], String 构造 List[String]
scala> implicitly[CanBuildFrom[List[Int], String, List[String]]]

// 由 Set[_], Double 构造 Set[Double]
scala> implicitly[CanBuildFrom[Set[String], Double, Set[Double]]]

// 由 List[_], Int 构造的是 List[Int] 与 Set[String] 目标类型不一致
scala> implicitly[CanBuildFrom[List[String], Int, Set[Int]]]

// 由 List[_], Int 构造的是 List[Int] 与 List[Double] 目标类型不一致
scala> implicitly[CanBuildFrom[List[String], Int, List[Double]]]

scala类型系统:28) 依赖类型》上有8条评论

  1. funnuy

    Functional dependencies不是依赖类型,它原来是关系数据库理论里的概念,用来表示类型之间的函数关系,更像是type level function和逻辑式编程。例如MultDep和CanBuildFrom可以看作有两个类型做参数的函数。

    Dependent type是指是依赖于值的类型。我最近看来了一个视频,里面就有介绍scala里的依赖类型的实现:

    回复
  2. funnuy

    我再想想,scala中用implicit object+trait不能完全表示functional dependencies。

    第一个问题,单从定义是看不出类型参数间的依赖关系的。

    例如trait MultDep[A, B, C],这个定义并没有说C是依赖于A和B,这种依赖关系需要文档记录。

    相反,在Haskell里, MultDep 会这样写:class MultDep a b c | a b -> c,明确表明了c是依赖于a和b的( a b -> c )。

    第二个问题是,scala里能定义冲突的implicit object,例如


    scala> implicit object mmm extends MultDep[Matrix, Matrix, Matrix]
    scala> implicit object mmv extends MultDep[Matrix, Matrix,, Vector]

    这就不能推导出正确的implict,必须显式传递:


    val v1 : Vector = mult(new Matrix {}, new Matrix{}) // 错误,mmm和mmv都满足参数要求
    val v2 : Vector = mult(new Matrix {}, new Matrix{})(mmv) // OK

    而在Haskell,当定义了a b -> c这样的依赖关系之后,就不能定义冲突的实例。

    虽然实践上可能不会有问题(谁会故意去定义冲突的implicit object呢?就算冲突也能被轻易发现),但这的确不能完全实现functional dependencies。

    回复
    1. hongjiang 文章作者

      是的,scala并不是设计时就支持依赖类型,所以缺乏一种有效的声明和描述。只是通过隐式参数实现了接近的效果。

      回复
  3. hongjiang 文章作者

    今天看到一篇文章《Typed Shell:给Unix Shell加上类型系统》http://www.soimort.org/posts/158/,
    即用Idris实现了一个带有类型的shell,想起在讨论“依赖类型”的时候,评论里有人提到过这门语言,Idris主要受Haskell和ML的影响,设计之初就把依赖类型作为它的一个主要特性。

    回复
  4. hongjiang 文章作者

    再补充一篇wiki:http://zh.wikipedia.org/wiki/%E4%BE%9D%E8%B5%96%E7%B1%BB%E5%9E%8B 里面提到一些支持依赖类型的语言:

    一些以证明辅助为主要目的的编程语言采用强函数式编程(total functional programming),这消除了停机问题,同时也意味着通过它们自身的核心语言无法实现任意无限递归,不是图灵完全的,如 Coq 和 Agda;另外一些依赖类型编程语言则是图灵完全的,如 Idris、由 ML 派生而来的 ATS 和 由 F# 派生而来的 F*。

    回复

发表评论

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