向量维度的编译时检查答案

【问题标题】：Compile-time check for vector dimension向量维度的编译时检查
【发布时间】：2011-02-12 14:19:38
【问题描述】：

我正在 scala 中实现一些轻量级的数学向量。我想在编译时使用类型系统来检查向量的兼容性。例如，尝试将一个维数为 2 的向量与另一个维数为 3 的向量相加会导致编译错误。

到目前为止，我将维度定义为案例类：

sealed trait Dim
case class One() extends Dim
case class Two() extends Dim
case class Three() extends Dim
case class Four() extends Dim
case class Five() extends Dim

这里是向量定义：

class Vec[D <: Dim](val values: Vector[Double]) {

  def apply(i: Int) = values(i)

  def *(k: Double) = new Vec[D]( values.map(_*k) )

  def +(that: Vec[D]) = {
    val newValues = ( values zip that.values ) map { 
      pair => pair._1 + pair._2
    }
    new Vec[D](newValues)
  }

  override lazy val toString = "Vec(" + values.mkString(", ") + ")"

}

这个解决方案效果很好，但是我有两个问题：

如何添加一个返回维度的dimension():Int 方法（即Vec[Three] 为3）？
如何在不提前声明所有需要的案例类的情况下处理更高的维度？

PS：我知道有很好的现有数学向量库，我只是想提高我对 scala 的理解。

【问题讨论】：

标签： scala types

【解决方案1】：

我的建议：

Peano Numbers by Apocalysp（链接到第一部分，其他部分如下）
Church Numerals 由 Jim McBeath 提供

【讨论】：

啊啊啊，类型级编程的乐趣。
是的，但是要解决我的问题，我如何将 peano 类型“转换”为 Int 以及如何自动构建与给定 Int 对应的正确 peano 类型？
@paradigmatic 你不能做 Int -> Peano。这需要依赖类型，Scala 不支持。将 Peano 转换为 Int 很简单，留给读者作为练习。 ;-) 对于支持依赖类型的语言，请参阅 Agda 和 Coq。

【解决方案2】：

我的建议是这样的：

sealed abstract class Dim(val dimension:Int)

object Dim {
  class One extends Dim(1)
  class Two extends Dim(2)
  class Three extends Dim(3)

  implicit object One extends One
  implicit object Two extends Two
  implicit object Three extends Three
}

case class Vec[D <: Dim](values: Vector[Double])(implicit dim:D) {

  require(values.size == dim.dimension)

  def apply(i: Int) = values(i)

  def *(k: Double) = Vec[D]( values.map(_*k) )

  def +(that: Vec[D]) = Vec[D](
     ( values zip that.values ) map {
      pair => pair._1 + pair._2
  })

  override lazy val toString = values.mkString("Vec(",", ",")")
}

当然，您只能通过这种方式对向量长度进行运行时检查，但正如其他人已经指出的那样，您需要使用 Church 数字或其他类型级编程技术来实现编译时检查。

  import Dim._
  val a = Vec[Two](Vector(1.0,2.0))
  val b = Vec[Two](Vector(1.0,3.0))
  println(a + b)
  //--> Vec(2.0, 5.0) 

  val c = Vec[Three](Vector(1.0,3.0)) 
  //--> Exception in thread "main" java.lang.ExceptionInInitializerError
  //-->        at scalatest.vecTest.main(vecTest.scala)
  //--> Caused by: java.lang.IllegalArgumentException: requirement failed

【讨论】：

【解决方案3】：

如果您不想走 Peano 路线，您始终可以使用 D 构造您的 Vec，然后使用实例通过 Dim 伴随对象确定维度。例如：

object Dim {
  def dimensionOf(d : Dim) = d match {
    case One => 1
    case Two => 2
    case Three => 3
  }
}
sealed trait Dim

我认为作为选择，您应该使用案例对象而不是案例类：

case object One extends Dim
case object Two extends Dim

然后在您的矢量上，您可能必须实际存储 Dim：

object Vec {
  def vec1 = new Vec[One](One)
  def vec2 = new Vec[Two](Two)
  def vec3 = new Vec[Three](Three)
}

class Vec[D <: Dim](d : D) {
  def dimension : Int = Dim dimensionOf d
  //etc

【讨论】：