scala - 使用 Shapeless 的方法所需的证据多于必要的证据

Question

昨天我和几个同事在探索Shapeless，我们决定写一个玩具方法来向case类的第一个参数添加一个，当该参数是Int时。 :

def addOneToCaseClass[C, H <: HList, E, T <: HList]
    (c: C)
    (implicit gen: Generic.Aux[C, H],
              h:   IsHCons.Aux[H, E, T],
              ev:  E =:= Int,
              ev2: (Int :: T) =:= H
    ): C = {

  val hList = gen.to(c)

  val elem = hList.head
  val tail = hList.tail

  val newElem = elem + 1

  gen.from(newElem :: tail)
}

在我看来， ev2参数是多余的——当然可以推断出 E :: T =:= Int :: T ，但编译器无法做到这一点。

有什么特别的原因吗？

Answer 1

您的直觉是合理的，但不幸的是 Scala 编译器不够聪明，无法派生 ev2来自 h和 ev .问题是h仅确定 H分解为 E :: T ，它不成立相反，即 E和 T合并等于 H .

我能想到的最简洁的表述与你的原著相似，但少了一个见证人，

def addOneToCaseClass[C, R <: HList, T <: HList](c: C)
  (implicit
    gen: Generic.Aux[C, R],
    h: IsHCons.Aux[R, Int, T],
    ev: (Int :: T) =:= R) = {
  val hList = gen.to(c)
  val elem = hList.head
  val tail = hList.tail
  gen.from(elem+1 :: tail)
}

在这里，我们能够消除 E =:= Int 的证明。通过使用 h表明 R分解为 Int :: T .但是我们仍然需要证明 Int :: T等于 R搬回 gen与更新的元素。