如何在 Scala 3 中证明 `Tuple.Map[H *: T, F] =:= (F[H] *: Tuple.Map[T, F])`

我正在尝试编写一个包含元组类型给定实例的特征（是的，我知道summonAll存在）：

trait TupleInstances[C[_], T <: Tuple] {
  val instances: Tuple.Map[T, C]
}

given[C[_]]: TupleInstances[C[_], EmptyTuple] with {
  val instances = EmptyTuple
}

inline given[C[_], H, T <: Tuple] (using ch: C[H], ti: TupleInstances[C, T]): TupleInstances[C, H *: T] with {
  val instances: Tuple.Map[H *: T, C] = ch *: ti.instances
}

并得到错误

 val instances: Tuple.Map[H *: T, C] = ch *: ti.instances
  |                                        ^^^^^^^^^^^^^^^^^^
  |               Found:    C[H] *: Tuple.Map[T, C]
  |               Required: Tuple.Map[H *: T, C]
  |
  |               Note: a match type could not be fully reduced:
  |
  |                 trying to reduce  Tuple.Map[T, C]
  |                 failed since selector  T
  |                 does not match  case EmptyTuple => EmptyTuple
  |                 and cannot be shown to be disjoint from it either.
  |                 Therefore, reduction cannot advance to the remaining case
  |
  |                   case h *: t => C[h] *: scala.Tuple.Map[t, C]

所以本质上我需要向所有人证明这一点F[_], Tup:

Tuple.Map[Tup, F] =:= (F[Tuple.Head[Tup]] *: Tuple.Map[Tuple.Tail[Tup], F])

我该如何去做呢？

首先，TupleInstances[C[_], EmptyTuple] (for C[_] and trait TupleInstances[C[_], T <: Tuple]） 是不正确的

Type argument C[?] does not have the same kind as its bound [_$1]

正确是更高尚的TupleInstances[C, EmptyTuple] or TupleInstances[C[*], EmptyTuple] (with scalacOptions += "-Ykind-projector") or TupleInstances[[t] =>> C[t], EmptyTuple]. TupleInstances[C[_], EmptyTuple]最终应该意味着相同，但目前它意味着存在TupleInstances[C[?], EmptyTuple].

多态方法适用于 lambda 类型，但不适用于 Scala 3 中的类型通配符

高级类型参数中下划线的使用规则

第二，

• 匹配类型，以及

• 类型类

是在 Scala 3 中执行类型级计算的两种不同方法（如 Scala 2 中的类型投影和类型类，或者 Haskell 中的类型族和类型类）。如果你想混合使用它们，一些极端情况是可能的。

您可以再添加一项约束

trait TupleInstances[C[_], T <: Tuple]:
  def instances: Tuple.Map[T, C]
object TupleInstances:
  given[C[_]]: TupleInstances[C, EmptyTuple] with
    val instances = EmptyTuple

  given[C[_], H, T <: Tuple](using
    ch: C[H],
    ti: TupleInstances[C, T],
    ev: (C[H] *: Tuple.Map[T, C]) =:= Tuple.Map[H *: T, C] // <-- HERE!!!
  ): TupleInstances[C, H *: T] with
    val instances: Tuple.Map[H *: T, C] = ch *: ti.instances

或者使用summonFrom and inline

import scala.compiletime.summonFrom

trait TupleInstances[C[_], T <: Tuple]:
  def instances: Tuple.Map[T, C]
object TupleInstances:
  given[C[_]]: TupleInstances[C, EmptyTuple] with
    val instances = EmptyTuple

  given[C[_], H, T <: Tuple](using
    ch: C[H],
    ti: TupleInstances[C, T]
  ): TupleInstances[C, H *: T] with
    inline def instances: Tuple.Map[H *: T, C] =
      summonFrom {
        case _: ((C[H] *: Tuple.Map[T, C]) =:= Tuple.Map[H *: T, C]) =>
          ch *: ti.instances
      }

Scala 并不是一个真正的定理证明器。它可以检查C[H] *: Tuple.Map[T, C] =:= Tuple.Map[H *: T, C]对于具体的C, H, T但不能任意

如何在 Scala 2.13 中定义自然数归纳法？

此外，您还应该重新考虑是否要根据匹配类型而不是类型类来制定整个逻辑

import scala.compiletime.{erasedValue, summonInline}

inline def tupleInstances[C[_], T <: Tuple]: Tuple.Map[T, C] = erasedValue[T] match
  case _: EmptyTuple => EmptyTuple
  case _: (h *: t)   => summonInline[C[h]] *: tupleInstances[C, t]

或者您想根据类型类而不是匹配类型来制定整个逻辑

trait TupleInstances[C[_], T <: Tuple]:
  type Out <: Tuple
  def instances: Out
object TupleInstances:
  given[C[_]]: TupleInstances[C, EmptyTuple] with
    type Out = EmptyTuple
    val instances = EmptyTuple

  given[C[_], H, T <: Tuple](using
    ch: C[H],
    ti: TupleInstances[C, T]
  ): TupleInstances[C, H *: T] with
    type Out = C[H] *: ti.Out
    val instances = ch *: ti.instances

在Scala 3中，如何替换已删除的通用类型投影？

Dotty 提供什么来替代类型投影？