Prod在shapeless中的整数值

Question

在兴奋地玩着shapeless自然数时，我想知道获得例如nats乘积的整数值的最好方法是什么。

摘自shapeless nat.scala

trait Prod[A <: Nat, B <: Nat] {
  type Out <: Nat
}

trait ProdAux[A <: Nat, B <: Nat, C <: Nat]

object Prod {
  implicit def prod[A <: Nat, B <: Nat, C <: Nat](implicit diff : ProdAux[A, B, C]) = new Prod[A, B] {
    type Out = C
  }
}

object ProdAux {
  import Nat._0

  implicit def prod1[B <: Nat] = new ProdAux[_0, B, _0] {}
  implicit def prod2[A <: Nat, B <: Nat, C <: Nat, D <: Nat]
    (implicit ev1 : ProdAux[A, B, C], ev2 : SumAux[B, C, D]) = new ProdAux[Succ[A], B, D] {}
}

到目前为止，我已经给出了简单的定义

def toInt[A <: Nat, B <: Nat, C <: Nat](p: Prod[A, B])
    (implicit paux: ProdAux[A, B, C], iv: ToInt[C]): Int = iv()

事实上，这种方法需要一些冗余的等价代码实现，比如和、差、阶乘等，所以我更愿意使用“默认”方法toInt[A <: Nat]。

你会怎么做？是否可以使用内部类型(Prod#Out、Sum#Out等)？

Answer 1

很抱歉我之前错过了这个问题(顺便说一句，shapeless mailing list是一个问这个问题的好地方)。

我认为您稍微误解了Prod类型类的作用:它的实例本身不是Nat，它们见证了三个Nat之间的关系，即(A * B) == C。因此，将Prod实例转换为Int并没有多大意义，或者更确切地说，如果是这样的话，结果值对应于A、B或C中的任何一个或所有这些值的三元组也同样有意义。

为了在方法定义中用作证明术语，您所显示的样式与预期的基本一致……有关示例，请参阅here。显然，这并不能很好地解决REPL上的问题。为了让它更流畅一点，你可以试着这样做，

def prod[A <: Nat, B <: Nat](implicit prod : Prod[A, B]) =
  new { def toInt(implicit ti : ToInt[prod.Out]) = ti() }

这允许REPL交互，例如，

scala> prod[_2, _3].toInt
res0: Int = 6

如果这仍然不是你想要的，那么请前往邮件列表，勾勒出你想要做的事情。