10

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

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

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

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

因错误而失败cannot prove 'newSeq(100)' is not nil，这令人惊讶，因为人们可能会认为 anewSeq不是 nil。一种解决方法似乎使用这样的助手：

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

尝试使用SafeSeq. 例如，人们可能期望当您映射 a 时SafeSeq，结果不应再次为 nil。但是，这样的事情也会失败：

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 代码时，nil-hiding-principle 成为错误的危险来源，因为nil序列仅在 Nim 方面是无害的......

4

1 回答 1

16

使用isNil魔法来检查 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]()
于 2015-09-09T22:28:09.220 回答