我正在做一个自己的固定大小的向量类,这段代码被拒绝了
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
不同吗?
1条答案
按热度按时间v7pvogib1#
是的,
S
和+ 1
确实不同。字符串
它们在编译器内部实现。
Scala不是一个真正的定理证明器。它允许你证明定理,但不会为你证明定理。Scala知道
10 + 1
或1 + 10
是S[10]
,但不知道n + 1
或1 + n
是S[n]
型
即使
S
和+
是感应实现的,型
很明显
_1 + n =:= S[n]
,但不明显n + _1 =:= S[n]
(这是一个有待证明的定理)型
如果你根据第二个参数归纳地定义加法,
型
则反之亦然
n + _1 =:= S[n]
变得明显,但_1 + n =:= S[n]
必须被证明型
How to define induction on natural numbers in Scala 2.13?