Can't write type-safe implementations of Tuple methods

[TomasMikula]

The implementations of Tuple methods delegate to unsafe runtime.Tuples methods and then use a type cast (asInstanceOf).

Tuples bring generic programming to Scala 3 shows how we could safely implement the ++ (concat) method.

However, I'm at a loss to know how to safely implement other methods, such as drop, take, splitAt, to the point that I don't think it's possible (but perhaps just undocumented?).

Below is a failed attempt at implementing the drop method. I would be happy to be shown the correct way, but for now I just think it is not possible.

Compiler version

3.0.0-RC

Minimized example

import compiletime._
import compiletime.ops.int._
import Tuple.Drop

def drop[T <: Tuple, N <: Int](t: T, n: N): Drop[T, N] =
  n match {
    case _ : 0 => t
    case n : S[n1] => t match {
      case _ : EmptyTuple => EmptyTuple
      case (_ *: t1): (_ *: t1) => drop[t1, n1](t1, n-1)
    }
  }

Output

-- [E007] Type Mismatch Error: drop.scala:9:29 ---------------------------------
9 |      case _ : EmptyTuple => EmptyTuple
  |                             ^^^^^^^^^^
  |Found:    EmptyTuple.type
  |Required: T match {
  |  case EmptyTuple => EmptyTuple
  |  case 
  |    [x, xs <: Tuple] =>> 
  |      scala.runtime.MatchCase[x *: xs, LazyRef(scala.Tuple.Drop[xs, n1])]
  |} <: Tuple
  |
  |where:    T  is a type in method drop with bounds >: (?1 : EmptyTuple.type) and <: Tuple
  |          n1 is a type in method drop with bounds <: Int

longer explanation available when compiling with `-explain`
-- [E007] Type Mismatch Error: drop.scala:10:52 --------------------------------
10 |      case (_ *: t1): (_ *: t1) => drop[t1, n1](t1, n-1)
   |                                                    ^^^
   |                Found:    Int
   |                Required: n1
   |
   |                where:    n1 is a type in method drop with bounds <: Int

longer explanation available when compiling with `-explain`
2 errors found

[odersky]

Moving to discussions. It would be good if others could participate.

[nicolasstucki]

I believe the way to do it is using inline. The issue is that it will be O(n²) and will generate a lot of code.

[TomasMikula]

I believe the way to do it is using inline.

Can you elaborate? Just naively adding inline to def drop has no effect (I get the same 2 errors).

The issue is that it will be O(n²) and will generate a lot of code.

Let's not worry about that for now. (The O(n²) would go away if I used a custom recursive tuple implementation. Now I just want to explore what's possible wrt. abstracting over arity.)

[LPTK]

The problem is the n-1 part. It's never going to work unless you somehow partially-evaluate it at compile time, which I believe is what @nicolasstucki was suggesting, and which would probably require a transparent inline method. However, I'm pretty sure this is not what you want, as we don't necessarily know the size as a constant at compile time. Also I don't actually see how this would help type check your definition without having to use casts.

So I think you're going to have much fewer troubles going with the usual way sized vectors are done in dependently-typed languages (look up how it's done in, eg, Idris, if you don't know). Especially now that #12397 is in. The main problem is that forces you to use a custom, inefficient Nat data type. We should be able to use Int, but for that we'd need a value-level S constructor reflecting the type-level S. Its absence from the library seems like a big omission.

[TomasMikula]

That's actually not missing. As you point out, match types can fill this role. And before that, in Scala 2, type projection could do it. Sure, it's not particularly convenient, but unifying term and type functions is definitely not required.

Match types are the point of investigation of this discussion. This thread though digresses into an alternative approach. It is definitely not convenient. One quickly runs into problems like: given a, b: Drop[T, N], the compiler doesn't know that a.Out = b.Out, i.e. it doesn't know that Drop[T, N] is something like a function.

I disagree, given "dependent type" in your narrower sense. Dependent type theories in the line going back to Martin Löf included the notion of type equality/identity, which is essentially a "proto inductive type".

Let me clarify. What I meant by "a dependently typed language not needing GADTs" was just that it can encode a GADT using a plain ADT (an enumeration of cases/indices) and a function from that ADT to Type.

[LPTK]

it can encode a GADT using a plain ADT (an enumeration of cases/indices) and a function from that ADT to Type

Can it? How do you encode Eq a b, so as to write an implementation for forall a b. Eq a b -> a -> b?

[TomasMikula]

it can encode a GADT using a plain ADT (an enumeration of cases/indices) and a function from that ADT to Type

Can it? How do you encode Eq a b, so as to write an implementation for forall a b. Eq a b -> a -> b?

OK, and a built-in equality type :)

[LPTK]

Actually, you'd still be missing some form of existential quantification. It's an essential ingredient of modern "dependently-typed" languages, supported for instance through dependent pairs, inductive types, or GADTs. This includes Scala – which supports it through object types with abstract type members.

[TomasMikula]

Yeah, I was kind of implicitly assuming existential quantification. It is actually already at the very core of the imagined encoding of a GADT. It would be Σ (i: I) f(i) where f: I -> Type and I is a simple enumeration. And f might need to return a dependent pair as well.