为什么类型检查失败？ （scala.compiletime.ops.int）

Question

我正在制作一个自己的固定大小向量类，并且此代码被拒绝

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)

此消息：

[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`:

但是当我在

Dim + 1

的定义中将

S[Dim]

更改为

::

时，它就起作用了。

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

为什么会出现这种情况？

S

和

+ 1

有不同吗？

Answer 1

是的，

S

和

+ 1

确实不同。

type S[N <: Int] <: Int

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

它们在编译器内部实现。

Scala 并不是一个真正的定理证明器。 它允许您证明定理，但不会为您证明定理。 Scala 知道

10 + 1

或

1 + 10

是

S[10]

但不知道

n + 1

或

1 + n

是

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

即使

S

和

+

是归纳实现的

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]

很明显

_1 + n =:= S[n]

但不明显

n + _1 =:= S[n]

（这是一个待证明的定理）

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

如果您针对第二个参数归纳定义加法

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

那么反之亦然

n + _1 =:= S[n]

变得显而易见，但

_1 + n =:= S[n]

必须被证明

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

如何在 Scala 2.13 中定义自然数归纳法？