1

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?

Improve this question
0

1 Answer 1

Reset to default
1

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?

Improve this answer
Sign up to request clarification or add additional context in comments.

16 Comments

Thanks for your answer, I have a few questions: 1) Is is not possible to prove this statement in general? I suppose I could use my outside knowledge and simply cast, but it's not nice to do. 2) Why is it not possible to combine type classes and match types? Is there a rule of thumb when to use one or the other? I'm more used to a combined or type-class only approach from Scala 2 and Haskell. 3) In your second example, why did you use summonFrom with a single case instead of summon or summonInline?
@Grisu47 Thanks for accepting and upvoting. "Is is not possible to prove this statement in general?" The question is what "to prove some statement in Scala" means. In Scala 3 you can define Map with type classes scastie.scala-lang.org/DmytroMitin/BuSg4NaRSXKHsV7khA3NmA or match types scastie.scala-lang.org/DmytroMitin/BuSg4NaRSXKHsV7khA3NmA/1 (similarly, in Scala 2 you can define it with type classes scastie.scala-lang.org/DmytroMitin/of0jdN9xS9SJEPnADmhu7A or type projections scastie.scala-lang.org/DmytroMitin/of0jdN9xS9SJEPnADmhu7A/1 ,
@Grisu47 in Haskell you can prove it with type classes or type families). According to Curry-Howard correspondence, statements correspond to types, proofs of statements correspond to values (closed terms) of these types. In a dependently typed language like Idris, Agda, Coq etc., a = b is a type for any two values a, b (with the only constructor refl(a) of type a = a). So to prove an equality a = b in such a language means to construct a value of the type a = b.
@Grisu47 But Scala is not a fully dependently typed language. If you define Map with type classes then to prove Map[H *: T, F] =:= (F[H] *: Map[T, F]) probably means to construct a value of this type and actually the inductive implicit Map.hcons is such a value (with match types you have less control on proofs). So in Scala you're proving statements, you're convincing the compiler, not compiler itself does. Scala is not an actual theorem prover stackoverflow.com/questions/75742747 It can prove Map[H *: T, F] =:= (F[H] *: Map[T, F]) for concrete H, T, F
@Grisu47 like Map[Int *: String *: EmptyTuple, List] =:= List[Int] *: List[String] *: EmptyTuple but can't for arbitrary H, T, F because Scala knows how to construct implicits of finite fixed length but doesn't know how to construct implicits of unknown non-fixed length.
|

Start asking to get answers

Find the answer to your question by asking.

Ask question

Explore related questions

See similar questions with these tags.