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?