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?

Dmytro Mitin
  • 48,194
  • 3
  • 28
  • 66
Grisu47
  • 530
  • 5
  • 16

1 Answers1

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?

Dmytro Mitin
  • 48,194
  • 3
  • 28
  • 66
  • 1
    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 Apr 26 '23 at 08:07
  • 1
    @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 https://scastie.scala-lang.org/DmytroMitin/BuSg4NaRSXKHsV7khA3NmA or match types https://scastie.scala-lang.org/DmytroMitin/BuSg4NaRSXKHsV7khA3NmA/1 (similarly, in Scala 2 you can define it with type classes https://scastie.scala-lang.org/DmytroMitin/of0jdN9xS9SJEPnADmhu7A or type projections https://scastie.scala-lang.org/DmytroMitin/of0jdN9xS9SJEPnADmhu7A/1 , – Dmytro Mitin Apr 26 '23 at 09:11
  • 1
    @Grisu47 in Haskell you can prove it with type classes or type families). According to [Curry-Howard correspondence](https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_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`. – Dmytro Mitin Apr 26 '23 at 09:11
  • 1
    @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 https://stackoverflow.com/questions/75742747 It can prove `Map[H *: T, F] =:= (F[H] *: Map[T, F])` for concrete `H`, `T`, `F` – Dmytro Mitin Apr 26 '23 at 09:12
  • 1
    @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. – Dmytro Mitin Apr 26 '23 at 09:12
  • 1
    @Grisu47 *"I suppose I could use my outside knowledge and simply cast"* There is a difference between casting and using implicit hint `(using A =:= B)` or `summonFrom { case _: A =:= B => ...}`. Casting will be checked at runtime (so you say the compiler not to check anything at compile time at all and trust you completely, let runtime/JVM check). Implicit hint will be checked at compile time when `H`, `T`, `F` will be inferred to be some concrete types. Checking at compile time is better than at runtime because failing earlier is better than failing later. – Dmytro Mitin Apr 26 '23 at 09:19
  • 1
    @Grisu47 *"Why is it not possible to combine type classes and match types"* It's completely possible. Like I did. `Tuple.Map` is from match types, `using ev: (C[H] *: Tuple.Map[T, C]) =:= Tuple.Map[H *: T, C]` or `summonFrom { case _: ((C[H] *: Tuple.Map[T, C]) =:= Tuple.Map[H *: T, C]) =>` is from type classes. Just you should be prepared that some corner cases are possible, maybe you'll have to use such implicit hints, maybe you'll have to introduce them manually, – Dmytro Mitin Apr 26 '23 at 09:28
  • 1
    @Grisu47 maybe there will be many such hints for complicated calculations. For example see https://stackoverflow.com/questions/75467905 I had to use 5 hints until I found a shorter way to convince the compiler. – Dmytro Mitin Apr 26 '23 at 09:28
  • 1
    @Grisu47 *"Is there a rule of thumb when to use one or the other"* The rule of thumb is to keep formulating your type-level logic mostly via type classes if you started with them or mostly via match types if you started with them. For example if you started with `Tuple.Map`, which is a match type in Scala 3 standard library, then try to continue mostly with match types. If you started with `shapeless.ops.hlist.Mapped`, which is a type class in Scala 2 Shapeless-2, then try to continue mostly with type classes. But surely you can mix type classes and match types. – Dmytro Mitin Apr 26 '23 at 09:34
  • 1
    @Grisu47 Scala is a very flexible language. You can always do the same thing in many different ways in Scala. – Dmytro Mitin Apr 26 '23 at 09:34
  • 1
    @Grisu47 *"why did you use `summonFrom` with a single case instead of `summon` or `summonInline`?"* I guess I could use `summonInline` instead of `summonFrom`. You can play with that. I could replace `summonFrom { case _: A =:= B => ...` with `given A =:= B = summonInline[A =:= B]`. Just inside `summonFrom`, `ev: A =:= B` is an implicit automatically while with `summonInline` I have to use `given`. Just `summonInline[A =:= B]` doesn't bring the implicit conversion to the scope. So `summonFrom` seems to be a little shorter. – Dmytro Mitin Apr 26 '23 at 09:54
  • 1
    @Grisu47 But there is a big difference between `summonFrom`/`summonInline` vs. `summon`. This is like a difference between `implicit` vs. `implicitly` https://stackoverflow.com/a/59399278/5249621 https://stackoverflow.com/a/74439731/5249621 https://stackoverflow.com/a/64242256/5249621 https://stackoverflow.com/questions/74148670 https://stackoverflow.com/questions/67258252 https://stackoverflow.com/questions/75504891 Or between `c.inferImplicitValue`/`q"implicitly[...]"` vs. `implicitly[...]` . – Dmytro Mitin Apr 26 '23 at 09:54
  • 1
    @Grisu47 The thing is where and when implicit is resolved. With `summon`, implicit is resolved now and here. With `summonInline`/`summonFrom` implicit resolution is postponed till inlining, implicit will be resolved in the scope around macro expansion or inlining. – Dmytro Mitin Apr 26 '23 at 09:54
  • A proof is a value. So to prove the statement in general would be to give a function `given [F, H, T <: Tuple]: (F[H] *: Tuple.Map[T, F] =:= Tuple.Map[H *: T, F])`. Since `=:=` is sealed, I can not construct it directly. I could cast `summon[Tuple.Map[H *: T, F] =:= Tuple.Map[H *: T, F]].asInstanceOf[F[H] *: Tuple.Map[T, F] =:= Tuple.Map[H *: T, F]]`, which is hardly a sound proof. The other option is to outline a proof to the compiler by constructing an instance of above by manipulating other instances of `=:=` using the provided lemmas (functions of `=:=`) but I don't know how to do that. – Grisu47 Apr 26 '23 at 18:00
  • @Grisu47 The only sound way to construct `=:=` manually is `<:<.refl[A]`. You should keep in mind that `=:=` is not real equality. For example it's not symmetric https://stackoverflow.com/a/76027876/5249621 (see also the links there). With type classes you can do https://scastie.scala-lang.org/DmytroMitin/jSI5BkMQTLmlVvmU7vj02Q or https://scastie.scala-lang.org/DmytroMitin/jSI5BkMQTLmlVvmU7vj02Q/2, not https://scastie.scala-lang.org/DmytroMitin/jSI5BkMQTLmlVvmU7vj02Q/3 but https://scastie.scala-lang.org/DmytroMitin/jSI5BkMQTLmlVvmU7vj02Q/5 – Dmytro Mitin Apr 27 '23 at 08:47
  • @Grisu47 With match types https://scastie.scala-lang.org/DmytroMitin/jSI5BkMQTLmlVvmU7vj02Q/6 https://scastie.scala-lang.org/DmytroMitin/jSI5BkMQTLmlVvmU7vj02Q/7 – Dmytro Mitin Apr 27 '23 at 08:47