尼姆：如何证明不是零？-Java 学习之路

对我来说，Nim最有趣的功能之一是 not nil 注释，因为它基本上允许在编译器的帮助下静态地完全排除各种NPE /访问冲突错误 . 但是，我在实践中很难使用它 . 让我们考虑一个最基本的用例：

type
  SafeSeq[T] = seq[T] not nil

这里的一个直接陷阱是即使实例化这样的_472252也不是那么容易 . 这次尝试

let s: SafeSeq[int] = newSeq[int](100)

失败，错误 cannot prove 'newSeq(100)' is not nil ，这是令人惊讶的，因为人们可能会认为 newSeq 根本不是零 . 解决方法似乎使用这样的帮助：

proc newSafeSeq*[T](size: int): SafeSeq[T] =
  # I guess only @[] expressions are provably not nil
  result = @[]
  result.setlen(size)

当尝试用 SafeSeq 做某事时会出现下一个问题 . 例如，人们可能期望当你映射 SafeSeq 时，结果应该不再为零 . 但是，这样的事情也失败了：

let a: SafeSeq[int] = @[1,2,3]
let b: SafeSeq[string] = a.mapIt(string, $it)

一般问题似乎是，只要返回类型变为普通 seq ，编译器似乎忘记了 not nil 属性并且无法再证明它 .

我现在的想法是介绍一个小的（可以说是丑陋的）辅助方法，它允许我实际证明 not nil ：

proc proveNotNil*[T](a: seq[T]): SafeSeq[T] =
  if a != nil:
    result = a # surprise, still error "cannot prove 'a' is not nil"
  else:
    raise newException(ValueError, "can't convert")

# which should allow this:
let a: SafeSeq[int] = @[1,2,3]
let b: SafeSeq[string] = a.mapIt(string, $it).proveNotNil

但是，编译器也无法在此处证明 not nil . 我的问题是：

在这种情况下，如何帮助编译器推断 not nil ？
这项功能的长期目标是什么，即是否有计划推断 not nil 更强大？手册 proveNotNil 的问题在于它可能不安全，并且反对编译器负责证明它的想法 . 但是，如果仅在非常罕见的情况下才需要 proveNotNil ，那么它不会受到太大伤害 .

注意：我知道 seq 试图与 nil 无关，即使在 nil 情况下一切正常 . 但是，这仅适用于Nim . 当连接C代码时，零隐藏原则成为bug的危险源，因为 nil 序列在Nim方面是无害的......

1 回答

使用 isNil magic检查nil：

type SafeSeq[T] = seq[T] not nil
proc proveNotNil[T](s: seq[T]): SafeSeq[T] =
  if s.isNil: # Here is the magic!
    assert(false)
  else:
    result = s
let s = proveNotNil newSeq[int]()

回复于 2024-04-29T23:14:49+08:00

尼姆：如何证明不是零？

1 回答

相关问题