3

兴奋地玩弄无形的自然数，我想知道获得例如 nats 乘积的整数值的最佳方法是什么。

摘自无形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...）？

4

1 回答 1

2

抱歉，我之前错过了这个问题（顺便说一句，无形邮件列表是提出这类问题的好地方）。

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

为了在方法定义中用作证明术语，您所展示的样式几乎与预期的一样......请参阅此处以获取示例。但是很明显，这对于在 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

如果这仍然不是您所追求的，那么请前往邮件列表并勾勒出您希望能够做什么。

于 2012-02-26T18:03:46.740 回答