编译时检查 Nat 的总和？

Question

我尝试编写一个类型类SumEq5，使其HList 类型参数的前两个字段加起来为5：

trait SumEq5[A]
object SumEq5 {
  def apply[L <: HList](implicit ev: SumEq5[L]): SumEq5[L] = ev

  implicit def sumEq5Ev[L <: HList, A <: Nat, B <: Nat](
    implicit hcons: IsHCons.Aux[L, A, B :: HNil],
             ev: Sum.Aux[A, B, _5]
  ): SumEq5[L] = new SumEq5[L] {}
}

但它似乎不起作用：

import shapeless._
import shapeless.nat._
import net.SumEq5

scala> SumEq5[_0 :: _5 :: HNil]
<console>:19: error: could not find implicit value for 
    parameter ev: net.SumEq5[shapeless.::[shapeless.nat._0,shapeless.::
       [shapeless.nat._5,shapeless.HNil]]]
       SumEq5[_0 :: _5 :: HNil]

请告诉我为什么_0 :: _5 :: HNil 没有证据表明它的两个Nat 等于5。

编辑

根据 Denis Rosca 在shapeless's gitter 的帮助更新了问题。

Answer 1

如果您想推广到任意长度的HLists，Dale Wijnand 和 Marcus Henry 指出的方向是正确的，但是如果您真的只想容纳两个元素 HLists，那么以下是一个相当简单的解决方案，

scala> import shapeless._, nat._, ops.nat._
import shapeless._
import nat._
import ops.nat._

scala> :paste
// Entering paste mode (ctrl-D to finish)

trait SumEq5[A]

object SumEq5 {
  def apply[L <: HList](implicit ev: SumEq5[L]): SumEq5[L] = ev

  implicit def sumEq5AB[A <: Nat, B <: Nat]
    (implicit ev: Sum.Aux[A, B, _5]): SumEq5[A :: B :: HNil] =
      new SumEq5[A :: B :: HNil] {}
}

// Exiting paste mode, now interpreting.

defined trait SumEq5
defined object SumEq5

scala> SumEq5[_0 :: _5 :: HNil]
res0: SumEq5[_0 :: _5 :: HNil]] = SumEq5$$anon$1@658c5e59

这里的主要区别在于，实例是为两个元素列表显式定义的，而不是为一般列表定义的，前提是存在一个列表恰好具有两个元素的证据。

根据 Dale 的更新，我们可以将其概括为包含至少两个（而不是正好两个）元素的 HLists，同样无需任何额外的见证，

scala> import shapeless._, nat._, ops.nat._
import shapeless._
import nat._
import ops.nat._

scala> :paste
// Entering paste mode (ctrl-D to finish)

trait SumEq5[A]

object SumEq5 {
  def apply[L <: HList](implicit ev: SumEq5[L]): SumEq5[L] = ev

  implicit def sumEq5AB[A <: Nat, B <: Nat, T <: HList]
    (implicit ev: Sum.Aux[A, B, _5]): SumEq5[A :: B :: T] =
      new SumEq5[A :: B :: T] {}
}

// Exiting paste mode, now interpreting.

defined trait SumEq5
defined object SumEq5

scala> SumEq5[_0 :: _5 :: HNil]
res0: SumEq5[_0 :: _5 :: HNil]] = SumEq5$$anon$1@658c5e59

Answer 2

我只能为您提供部分答案，即（解决方法）解决方案，但不明白为什么原始版本不能按预期工作。

看来你不能直接要求IsHCons.Aux[L, A, B :: HNil]，你需要一点一点地做：

1. IsHCons.Aux[L, A, L2]，然后
2. IsHCons.Aux[L2, B, HNil]

因此，编译：

import shapeless._, nat._, ops.hlist._, ops.nat._

trait SumEq5[A]
object SumEq5 {
  def apply[L <: HList](implicit ev: SumEq5[L]): SumEq5[L] = ev

  implicit def sumEq5Ev[L <: HList, L2 <: HList, A <: Nat, B <: Nat](
    implicit hcons0: IsHCons.Aux[L, A, L2],
             hcons: IsHCons.Aux[L2, B, HNil],
             ev: Sum.Aux[A, B, _5]
  ): SumEq5[L] = new SumEq5[L] {}
}

object T {
  def main(args: Array[String]): Unit = {
    SumEq5[_0 :: _5 :: HNil]
  }
}

---

从 Miles Sabin's answer 开始，可以对其进行调整以支持 2 个或更多元素的任何 HList，其中前两个元素的总和为 5，如下所示：

import shapeless._, nat._, ops.hlist._, ops.nat._

trait SumEq5[A]
object SumEq5 {
  def apply[L <: HList](implicit ev: SumEq5[L]): SumEq5[L] = ev

  implicit def sumEq5Ev[L1 <: HList, L2 <: HList, L3 <: HList, A <: Nat, B <: Nat](
    implicit hcons1: IsHCons.Aux[L1, A, L2],
             hcons2: IsHCons.Aux[L2, B, L3],
             ev: Sum.Aux[A, B, _5]
  ): SumEq5[L1] = new SumEq5[L1] {}
}

object T {
  def main(args: Array[String]): Unit = {
    SumEq5[_0 :: _5 :: HNil]
  }
}