Prod的Int值在无形(Int value of Prod in shapeless)

Prod的Int值在无形(Int value of Prod in shapeless)

在兴奋中玩弄无形的自然数字，我想知道什么是获得整数值的最佳方法，例如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()

事实上，这种方法需要稍微冗余的等效代码实现，例如sums，diffs，factorials等。所以我宁愿能够使用“默认”方法来使用toInt[A <: Nat] 。

你会怎么做？ 是否可以使用内部类型（ Prod#Out ， Sum#Out ，...）？

Playing around with shapeless natural numbers in excitement, I wonder what could be the best approach to getting the integer value of e.g. a product of nats.

Excerpt from 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] {} }

So far I've come up with the straightforward definition of

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

As a matter of fact that approach would require somewhat redundant implementations of the equivalent code for e.g. sums, diffs, factorials etc. So I'd rather be able to use the "default" method toInt[A <: Nat].

How would you do it? And is it possible to use the inner types (Prod#Out, Sum#Out, ...)?

最满意答案

对不起，我早些时候错过了这个问题（BTW， 无形邮件列表是提出这类问题的好地方）。

我认为你有点误解了Prod类型的角色：它的实例本身不是Nat ，它们是三个Nat之间关系的见证，即(A * B) == C 因此，将Prod实例转换为Int s并不是真的有意义。 或者更确切地说，如果确实如此，那么结果值对应于A ， B或C任何A ，或者所有这些值的三倍都是有意义的。

为了在方法定义中用作证明术语，您所展示的样式非常符合预期...请参阅此处以获取示例。 显然，这对于在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

如果这仍然不是你想要的那么，请转到邮件列表并勾画出你想要做的事情。

Sorry I missed this question earlier (BTW, the shapeless mailing list is a good place to ask this kind of question).

I think you've slightly misunderstood the role of the Prod type class: its instances aren't themselves Nats, they're witnesses of a relation holding between three Nats, namely that (A * B) == C. As such, it doesn't really make all that much sense to convert Prod instances to Ints. Or rather, if it did, it'd make just as much sense for the resulting value to correspond to any of A, B or C, or the triple of all of them.

For use as proof terms in method definitions, the style you've shown is pretty much as intended ... see here for an example. Clearly though, this doesn't work very well for playing around with things on the REPL. To make that a bit smoother you could try things along the lines of,

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

which allows REPL interactions like,

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

If this still isn't quite what you're after then please head over to the mailing list and sketch out what you'd like to be able to do.