I tried the old not-nil pragma back in 2000 or so, and it definitely wasn’t ready for prime time. Today I thought I’d try strictNotNil with the current Nim 1.6.10, so I added it in one source file and sprinkled in a few not nil annotations. As expected there were some legit warnings, but also several that were incorrect.
I managed to reduce one of them down to a test case that’s about as trivial as you can get:
{.experimental: "strictNotNil".}
type Foo* = object
foo: int
proc doSomething* (f: ref Foo not nil) =
echo "Foo = ", f.foo
proc answer* (f: ref Foo) =
if f.isNil:
return
doSomething(f) # Error: cannot prove 'f' is not nil
This fails with the error shown above. However, using an else block fixes it:
proc answer* (f: ref Foo) =
if f.isNil:
return
else:
doSomething(f) # now this is ok 🤯
This bug makes it appear that the compiler’s control-flow analysis doesn’t understand what a return statement does.
I find that hard to believe, since there’s a lot of non-experimental stuff in Nim that depends on this kind of analysis. So what’s going wrong here?
(PS: I have found other places where testing x.isNil helps the compiler prove safety, but x == nil doesn’t. What’s the difference?)
That was mostly a design decision and proving anything that contains unstructured control flow is much harder than you think. Compare it to ML's (Rust's, Swift's ...) pattern matching to understand why it's done this way.
"Use early return to save levels of indentation" is just completely and objectively wrong. Unstructured control flow requires much more advanced algorithms for analysis.
"Use early return to save levels of indentation" is just completely and objectively wrong.
Of course it isn’t. If it’s objectively wrong, show me a formal proof. What you mean is “In my well-informed opinion it’s wrong.” One can disagree with that, and plenty of people do, vehemently. (Back when I was at Google, their C/C++ style guide mandated early returns in some cases.) I remember back in the 80s when I coded in Pascal, I found the lack of a return statement made some procedures miserable to write.
In any case, that ship has sailed. You already put a `return` statement in your language, Andreas. It’s official, it’s supported, and I’ve seen a lot of Nim code that uses it. If that complicates some of your compiler logic, don’t blame us.
I know that strictNotNil is clearly marked Experimental, thus unfinished, so I’m not upset that it has this problem; although I do wish that this limitation had been called out in the docs, since it would have saved me at least an hour of time yesterday.
That was mostly a design decision
That worries me; does it mean you don’t plan to make strictNotNil support return statements? If so, maybe you could add an explicit error message to that effect. Are there other upcoming language features that are going to have similar limitations?
If it’s objectively wrong, show me a formal proof.
Formal proof: Without return (and break, continue) you can prove "not nil-ability" with an abstract syntax tree traversal. With return you need a control flow graph.
See for example, https://ieeexplore.ieee.org/document/288377
It's not my fault that style guidelines are written by people who do not understand control flow.
The manual says that return should work: https://nim-lang.org/docs/manual_experimental.html#strict-not-nil-checking-unstructured-control-flow-rules
And it has an example with break to support that. Which also fails when adapted to the above example:
proc answer* (f: ref Foo) =
for a in [1]:
if f.isNil:
break
# here f: not Nil , because if nil, we would have breaked
doSomething(f) # Error: cannot prove 'f' is not nil
A clearly outlined language that has the current or the documented behavior, either's preferable to a language with a blurry outline. Even if people can be extremely productive by writing in "Nim Minus Minus", where neither return nor default values in const blocks complicate things, that book hasn't been written yet, and of Nim the tendency to proceed towards mastery of the tool by using all of its features in all of their use-cases.