scalascala-3type-level-computationdottymatch-types

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):

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
}

and getting the error

 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]

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

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

How do I go about doing that?


Solution

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

    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].

    Polymorphic method works with type lambda, but not with type wildcard in Scala 3

    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

    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
    

    Or using 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 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

    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

    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]
    

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

    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
    

    In Scala 3, how to replace General Type Projection that has been dropped?

    What does Dotty offer to replace type projections?