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?
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 higherkinded TupleInstances[C, EmptyTuple]
or TupleInstances[C[*], EmptyTuple]
(with scalacOptions += "Ykindprojector"
) 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 typelevel 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?