Can't seem to use match types with inline method and recursion

Question
1

I’d like to use match types to help me create a Nat type with nice ergonomics. On the surface it seems like a great fit: we can take integer literals and resolve the corresponding Nat type using a match type. That part works.

The problem is, I can’t seem to use an inline method to create the corresponding value.

Here is the code:

Since we are dealing with an inline method, and we know the value is also inline and const, it seems like we should be able to fully compute the match type before actually inlining, and verify that things typecheck.

Related, although the match type uses scala.compiletime.ops.int.-[I, 1] it doesn’t seem like I have any means to actually create a value of that type. I tried casting, but that seems to make it not inline as a constant and so despite the code compiling, if you try to use it, it will fail.

It seems like I should be able to take the match type implementation and create an inline function that does the same thing, but despite poking at this a number of ways I can’t seem to make it work.

Any suggestions?

2

I have tried to declare and use a match type as you have and also found that it does not work. First, be aware that you are using the integer as a Singleton and you are using its object type. So in your method you have access to the i.type. The return type FromInt[I] is not the same as FromInt[n.type].

Second, when using inline, you must match the return type that you declared with the actual type. Unfortunately, this means that we need to use asInstanceOf[FromInt[_]]. I don’t think the direct use of the Int ops will cut it. That being said, note that this has a run-time cost and may throw a run-time exception.

Here is a working example of my homegrown Tuple:

  sealed trait Tup
  case object EmpT extends Tup
  case class TCons[H, T <: Tup](head: H, tail: T) extends Tup


  @showAsInfix
  type +:[A,T<:Tup] = TCons[A, T] 

  /** A tuple of 0 elements */
  type EmpT = EmpT.type

  extension [A, T <: Tup] (a: A) def +: (t: T): TCons[A, T] =
    TCons(a, t)

  extension [L <: Tup, R <: Tup] (l: L) inline def ++ (r: R): Concat[L, R] =
    concat(l,r)

  object +: {
    def unapply[H, T <: Tup](x: H +: T): (H, T) = (x.head, x.tail)
  }

  type Drop[T <: Tup, N <: Int] <: Tup = N match
    case 0 => T
    case S[n1] => T match
      case EmpT => EmpT
      // case TCons[x, xs] => Drop[xs, n1]
      case x +: xs => Drop[xs, n1]
  

  inline def drop[L <: Tup, N <: Int](l: L, n: N): Drop[L, n.type] =
    inline if n < 0
    then
      error("Can only drop positive number of elements")
    inline if n == 0
    then
      l.asInstanceOf[Drop[L,n.type]]
    else
      inline l match
        case EmpT => 
          inline if n != 0
          then
            error("Number of elements to drop exceeds length of list.")
          else 
            l.asInstanceOf[Drop[L,n.type]]
        case list : TCons[_, _] =>
          drop(list.tail, n-1).asInstanceOf[Drop[L,n.type]]

I have made quite a few experiments, including the use of transparent. As you are now aware, from one of the Dotty issues you are tracking, there are still open problems related to typing.

Indeed I have looked and did not find out how to do this. Wonder if it is due to some fundamental type restriction.

I also assumed this, but have been continuously thwarted in my attempts to get code working. For the very simple cases were your match type can reflect the inline code
output, this is ok (as in your case). Once your code gets more complicated (such as selecting an item from a recursive structure that requires comparisons), the impedance mismatch between inline and match type starts causing difficulties.

As a side note, many times simple issues, like not being able to declare a value with a fully typed constant and using that to take advantage of the inline if and match, makes this technique unnecessarily more difficult to use. In your case, the line:

inline if i < 0 then

will work, but this won’t:

val c = 0
inline if i < c then

but this will:

inline val c = 0
inline if i < c then

Also when you call fromInt[I <: Int](inline i: I), this will work:

fromInt(2):

this won’t:

val c = 2
fromInt(c):

this will:

inline val c = 2
fromInt(c):

But when using a more complex structure for input, such as your Nat, the inline val declaration won’t work unless you pass use it directly as a parameter.

Hope this will be useful to you.

1 Like