Search code examples
scalacompile-timetypecheckingscala-3

Why this typecheck fails? (scala.compiletime.ops.int)


I was making a own fixed-size vector class and this code was rejected

import scala.compiletime.ops.int._

enum Tensor1[Dim <: Int, +T]:
  case Empty extends Tensor1[0, Nothing]
  case Cons[N <: Int, A](head: A, tail: Tensor1[N, A]) extends Tensor1[S[N], A]

  def ::[SuperT >: T](operand: SuperT): Tensor1[Dim + 1, SuperT] = Cons(operand, this)

with this message:

[error] Tree: Tensor1.Cons.apply[Dim, SuperT](operand, this)
[error] I tried to show that
[error]   Tensor1.Cons[Dim, SuperT]
[error] conforms to
[error]   Tensor1[Dim + (1 : Int), SuperT]
[error] but the comparison trace ended with `false`:

but when I changed Dim + 1 to S[Dim] in definition of ::, it works.

  def ::[SuperT >: T](operand: SuperT): Tensor1[S[Dim], SuperT] = Cons(operand, this)

Why this happens? Are S and + 1 different?


Solution

  • Yes, S and + 1 are indeed different.

    type S[N <: Int] <: Int
    
    type +[X <: Int, Y <: Int] <: Int
    

    They are implemented in compiler internals.

    Scala is not an actual theorem prover. It allows you to prove theorems but doesn't prove theorems for you. Scala knows that 10 + 1 or 1 + 10 are S[10] but doesn't know that n + 1 or 1 + n are S[n]

    summon[10 + 1 =:= S[10]] //compiles
    summon[1 + 10 =:= S[10]] //compiles
    
    type n <: Int
    //summon[n + 1 =:= S[n]] // doesn't compile
    //summon[1 + n =:= S[n]] // doesn't compile
    

    Even when S and + are implemented inductively

    sealed trait Nat
    class S[N <: Nat] extends Nat
    object _0 extends Nat
    type _0 = _0.type
    type _1 = S[_0]
    
    type +[N <: Nat, M <: Nat] = N match
      case _0 => M
      case S[n] => S[n + M]
    

    it's obvious that _1 + n =:= S[n] but not obvious that n + _1 =:= S[n] (this is a theorem to be proved)

    type n <: Nat
    summon[_1 + n =:= S[n]] // compiles
    //summon[n + _1 =:= S[n]] // doesn't compile
    

    If you define addition inductively with respect to the 2nd argument

    type +[N <: Nat, M <: Nat] = M match
      case _0 => N
      case S[m] => S[N + m]
    

    then vice versa n + _1 =:= S[n] becomes obvious but _1 + n =:= S[n] has to be proved

    //summon[_1 + n =:= S[n]] // doesn't compile
    summon[n + _1 =:= S[n]] // compiles
    

    How to define induction on natural numbers in Scala 2.13?