使用无形状的方法需要更多的证据

Question

我昨天和几个同事一起探索 Shapeless，我们决定编写一个玩具方法，当该参数是Int时，将一个添加到 case 类的第一个参数中

：

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编译器不够聪明，无法从h和ev中得出ev2。问题是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)
}

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