尼姆:如何证明不是零？

Question

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

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

这里的一个直接陷阱是即使实例化这样的SafeSeq事情并不容易.这次尝试

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)

当尝试用a做某事时会出现下一个问题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端只是无害的......

Answer 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]()