为什么这个类型检查失败？(scala.compiletime.ops.int)

jw5wzhpr 于 4个月前发布在 Scala

关注(0)|答案(1)|浏览(76)

我正在做一个自己的固定大小的向量类，这段代码被拒绝了

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不同吗？

scala

来源：https://stackoverflow.com/questions/77555127/why-this-typecheck-fails-scala-compiletime-ops-int

1条答案

按热度按时间

v7pvogib1#

是的，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

型
How to define induction on natural numbers in Scala 2.13?

赞(0）回复(0）举报 4个月前

我来回答

为什么这个类型检查失败？(scala.compiletime.ops.int)

1条答案

相关问题

热门标签

最新问答