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

huangapple
go评论79阅读模式
英文:

How to prove that `Tuple.Map[H *: T, F] =:= (F[H] *: Tuple.Map[T, F])` in Scala 3

问题

I'm trying to write a trait that contains given instances for a tuple type (yes I know that summonAll exists):

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

and getting the error

  1.  val instances: Tuple.Map[H *: T, C] = ch *: ti.instances
  2.   |                                        ^^^^^^^^^^^^^^^^^^
  3.   |               Found:    C[H] *: Tuple.Map[T, C]
  4.   |               Required: Tuple.Map[H *: T, C]
  5.   |
  6.   |               Note: a match type could not be fully reduced:
  7.   |
  8.   |                 trying to reduce  Tuple.Map[T, C]
  9.   |                 failed since selector  T
  10.   |                 does not match  case EmptyTuple => EmptyTuple
  11.   |                 and cannot be shown to be disjoint from it either.
  12.   |                 Therefore, reduction cannot advance to the remaining case
  13.   |
  14.   |                   case h *: t => C[h] *: scala.Tuple.Map[t, C]

So essentially I need to prove that for all F[_], Tup:

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

How do I go about doing that?

英文:

I'm trying to write a trait that contains given instances for a tuple type (yes I know that summonAll exists):

  1. trait TupleInstances[C[_], T <: Tuple] {
  2.   val instances: Tuple.Map[T, C]
  3. }
  5. given[C[_]]: TupleInstances[C[_], EmptyTuple] with {
  6.   val instances = EmptyTuple
  7. }
  9. inline given[C[_], H, T <: Tuple] (using ch: C[H], ti: TupleInstances[C, T]): TupleInstances[C, H *: T] with {
  10.   val instances: Tuple.Map[H *: T, C] = ch *: ti.instances
  11. }

and getting the error

  1.  val instances: Tuple.Map[H *: T, C] = ch *: ti.instances
  2.   |                                        ^^^^^^^^^^^^^^^^^^
  3.   |               Found:    C[H] *: Tuple.Map[T, C]
  4.   |               Required: Tuple.Map[H *: T, C]
  5.   |
  6.   |               Note: a match type could not be fully reduced:
  7.   |
  8.   |                 trying to reduce  Tuple.Map[T, C]
  9.   |                 failed since selector  T
  10.   |                 does not match  case EmptyTuple => EmptyTuple
  11.   |                 and cannot be shown to be disjoint from it either.
  12.   |                 Therefore, reduction cannot advance to the remaining case
  13.   |
  14.   |                   case h *: t => C[h] *: scala.Tuple.Map[t, C]

So essentially I need to prove that for all F[_], Tup:

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

How do I go about doing that?

答案1

得分: 1

Firstly, TupleInstances[C[_], EmptyTuple] (for C[_] and trait TupleInstances[C[_], T <: Tuple]) is incorrect:

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

Correct is higher-kinded TupleInstances[C, EmptyTuple] or TupleInstances[C[*], EmptyTuple] (with scalacOptions += "-Ykind-projector") or TupleInstances[[t] =>> C[t], EmptyTuple]. TupleInstances[C[_], EmptyTuple] is supposed to mean the same eventually but currently it means existential TupleInstances[C[?], EmptyTuple].

Secondly, match types, and type classes are two different ways to perform type-level calculations in Scala 3 (like type projections and type classes in Scala 2 or like type families and type classes in Haskell). If you want to mix them, some corner cases are possible.

You can add one more constraint:

  1. trait TupleInstances[C[_], T <: Tuple]:
  2.   def instances: Tuple.Map[T, C]
  3. object TupleInstances:
  4.   given[C[_]]: TupleInstances[C, EmptyTuple] with
  5.     val instances = EmptyTuple
  7.   given[C[_], H, T <: Tuple](using
  8.     ch: C[H],
  9.     ti: TupleInstances[C, T],
  10.     ev: (C[H] *: Tuple.Map[T, C]) =:= Tuple.Map[H *: T, C] // <-- HERE!!!
  11.   ): TupleInstances[C, H *: T] with
  12.     val instances: Tuple.Map[H *: T, C] = ch *: ti.instances

Or using summonFrom and inline:

  1. import scala.compiletime.summonFrom
  3. trait TupleInstances[C[_], T <: Tuple]:
  4.   def instances: Tuple.Map[T, C]
  5. object TupleInstances:
  6.   given[C[_]]: TupleInstances[C, EmptyTuple] with
  7.     val instances = EmptyTuple
  9.   given[C[_], H, T <: Tuple](using
  10.     ch: C[H],
  11.     ti: TupleInstances[C, T]
  12.   ): TupleInstances[C, H *: T] with
  13.     inline def instances: Tuple.Map[H *: T, C] =
  14.       summonFrom {
  15.         case _: ((C[H] *: Tuple.Map[T, C]) =:= Tuple.Map[H *: T, C]) =>
  16.           ch *: ti.instances
  17.       }

Scala is not an actual theorem prover. It can check that C[H] *: Tuple.Map[T, C] =:= Tuple.Map[H *: T, C] for specific C, H, T but can't for arbitrary.

Also, you should reconsider whether you'd like to formulate the whole logic in terms of match types rather than type classes:

  1. import scala.compiletime.{erasedValue, summonInline}
  3. inline def tupleInstances[C[_], T <: Tuple]: Tuple.Map[T, C] = erasedValue[T] match
  4.   case _: EmptyTuple => EmptyTuple
  5.   case _: (h *: t)   => summonInline[C[h]] *: tupleInstances[C, t]

or you'd like to formulate the whole logic in terms of type classes rather than match types:

  1. trait TupleInstances[C[_], T <: Tuple]:
  2.   type Out <: Tuple
  3.   def instances: Out
  4. object TupleInstances:
  5.   given[C[_]]: TupleInstances[C, EmptyTuple] with
  6.     type Out = EmptyTuple
  7.     val instances = EmptyTuple
  9.   given[C[_], H, T <: Tuple](using
  10.     ch: C[H],
  11.     ti: TupleInstances[C, T]
  12.   ): TupleInstances[C, H *: T] with
  13.     type Out = C[H] *: ti.Out
  14.     val instances = ch *: ti.instances

I hope this helps!

英文:

Firstly, TupleInstances[C[_], EmptyTuple] (for C[_] and trait TupleInstances[C[_], T <: Tuple]) is incorrect

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

Correct is higher-kinded TupleInstances[C, EmptyTuple] or TupleInstances[C[*], EmptyTuple] (with scalacOptions += "-Ykind-projector") or TupleInstances[[t] =>> C[t], EmptyTuple]. TupleInstances[C[_], EmptyTuple] is supposed to mean the same eventually but currently it means existential TupleInstances[C[?], EmptyTuple].

https://stackoverflow.com/questions/74267610/polymorphic-method-works-with-type-lambda-but-not-with-type-wildcard-in-scala-3

https://stackoverflow.com/questions/63942937/rules-for-underscore-usage-in-higher-kinded-type-parameters

Secondly,

  • match types, and

  • type classes

are two different ways to perform type-level calculations in Scala 3 (like type projections and type classes in Scala 2 or like type families and type classes in Haskell). If you want to mix them, some corner cases are possible.

You can add one more constraint

  1. trait TupleInstances[C[_], T <: Tuple]:
  2.   def instances: Tuple.Map[T, C]
  3. object TupleInstances:
  4.   given[C[_]]: TupleInstances[C, EmptyTuple] with
  5.     val instances = EmptyTuple
  7.   given[C[_], H, T <: Tuple](using
  8.     ch: C[H],
  9.     ti: TupleInstances[C, T],
  10.     ev: (C[H] *: Tuple.Map[T, C]) =:= Tuple.Map[H *: T, C] // <-- HERE!!!
  11.   ): TupleInstances[C, H *: T] with
  12.     val instances: Tuple.Map[H *: T, C] = ch *: ti.instances

Or using summonFrom and inline

  1. import scala.compiletime.summonFrom
  3. trait TupleInstances[C[_], T <: Tuple]:
  4.   def instances: Tuple.Map[T, C]
  5. object TupleInstances:
  6.   given[C[_]]: TupleInstances[C, EmptyTuple] with
  7.     val instances = EmptyTuple
  9.   given[C[_], H, T <: Tuple](using
  10.     ch: C[H],
  11.     ti: TupleInstances[C, T]
  12.   ): TupleInstances[C, H *: T] with
  13.     inline def instances: Tuple.Map[H *: T, C] =
  14.       summonFrom {
  15.         case _: ((C[H] *: Tuple.Map[T, C]) =:= Tuple.Map[H *: T, C]) =>
  16.           ch *: ti.instances
  17.       }

Scala is not an actual theorem prover. It can check that C[H] *: Tuple.Map[T, C] =:= Tuple.Map[H *: T, C] for specific C, H, T but can't for arbitrary

https://stackoverflow.com/questions/75742747/how-to-define-induction-on-natural-numbers-in-scala-2-13

Also you should reconsider whether you'd like to formulate the whole logic in terms of match types rather than type classes

  1. import scala.compiletime.{erasedValue, summonInline}
  3. inline def tupleInstances[C[_], T <: Tuple]: Tuple.Map[T, C] = erasedValue[T] match
  4.   case _: EmptyTuple => EmptyTuple
  5.   case _: (h *: t)   => summonInline[C[h]] *: tupleInstances[C, t]

or you'd like to formulate the whole logic in terms of type classes rather than match types

  1. trait TupleInstances[C[_], T <: Tuple]:
  2.   type Out <: Tuple
  3.   def instances: Out
  4. object TupleInstances:
  5.   given[C[_]]: TupleInstances[C, EmptyTuple] with
  6.     type Out = EmptyTuple
  7.     val instances = EmptyTuple
  9.   given[C[_], H, T <: Tuple](using
  10.     ch: C[H],
  11.     ti: TupleInstances[C, T]
  12.   ): TupleInstances[C, H *: T] with
  13.     type Out = C[H] *: ti.Out
  14.     val instances = ch *: ti.instances

https://stackoverflow.com/questions/75227132/in-scala-3-how-to-replace-general-type-projection-that-has-been-dropped

https://stackoverflow.com/questions/50043630/what-does-dotty-offer-to-replace-type-projections

huangapple
  • 本文由 发表于 2023年4月17日 01:56:54
  • 转载请务必保留本文链接：https://go.coder-hub.com/76029463.html
  • dotty
  • match-types
  • scala
  • scala-3
  • type-level-computation
匿名

发表评论

匿名网友

:?: :razz: :sad: :evil: :!: :smile: :oops: :grin: :eek: :shock: :???: :cool: :lol: :mad: :twisted: :roll: :wink: :idea: :arrow: :neutral: :cry: :mrgreen:

确定