How to initialize objects and arrays and not have the Warning: Cannot prove that 'result' is initialized. This will become a compile time error in the future. [ProveInit] message? My goal is not to disable that compiler warning with compiler flags or pragma, but to write the correct code for the nim compiler.
When the default value of a type is not compatible with the default value of a composed type (i.e. object), the compiler complains when you start using that object if it is not correctly initialized. For an object, the way to avoid the [ProveInit] warning is to use the default type converter, like:
type
Val = range[10 .. 100]
Mu = object
i: int
j: Val
proc initMu(i: int, j: Val): Mu =
result = Mu(i: i, j: j)
proc initMumu(i: int, j: int): Mu =
result = Mu(i: i, j: j)
var
m: Mu
m = initMu(1, 20)
echo m
m = initMumu(1, 20)
echo m
But when initializing arrays, the compiler is more strict and I haven't found the way to initialize them without warnings.
type
Val = range[10 .. 100]
Ga = array[3, Val]
Gaga = array[2, array[2, Val]]
proc initGa(a: openArray[int]): Ga =
# Ga() converter not compatible with openArray
#result = Ga(a)
# Initializing item by item gives warnings
for i in low(a) .. high(a):
result[i] = Val(a[i])
proc initGaga(a: array[2, array[2, Val]]): Gaga =
result = Gaga(a)
var
n: Ga
r: Gaga
n = initGa([20, 25, 30])
echo n
# Will not compile
#r = initGaga([[10, 20], [30, 40]])
r = initGaga([[Val(10), 20], [Val(30), 40]])
echo r
There are some parts of my code where I can prove that an array is correctly initialized, so I could disable the compiler warning locally. But there are other parts where I can't prove it easily and if it's not the case, there's a bug in my algorithm and I want the assistance of the compiler to warn me of such cases.
How can it be done?
Your problem is openArrray
See here for an example with no warnings: https://play.nim-lang.org/#ix=23KE
You must initialize your result variable manually, and then assign to the result element by element. Unfortunately I don't know a more concise way to initialize the array in your case (without using macros). Or you can just ignore the warning of course.
Why you cannot assign an openArray to an array:
An openArray is a read only reference to an array (or sequence).
You can access elements and read them, but you cannot assign the openarray reference itself. This would create a mutable reference to the array, and defeat the purpose of the read only behavior.
In you example, you shut up the compiler warning because you initialize result with static default values:
proc initGa(a: openArray[int]): Ga =
# no warnings!
# openArray is not compatible with array!
# this is why result = Ga(a) does not work
result = [Val(10), Val(10), Val(10)] <<<< Here the compiler sees result as initialized
for i in low(a) .. high(a):
result[i] = Val(a[i])
I know that an openArray in proc parameters is read only, but the nim compiler will copy its values to result if compatible. From the documentation, Any array with a compatible base type can be passed to an openarray parameter, the index type does not matter. I should have been able to call the initGa proc with an array[int] and return an array[Val] as int and Val are compatible. But that's another subject of discussion...
In my code, the proc looks like:
type
Val = range['A' .. 'Z']
Board = array[1 .. 10, array[1 .. 10, Val]]
Position = tuple[int, int]
proc initBoard(pieces: seq[Position]): Board =
# Now I must initialize result with default value, let say 'A' and
# then fill it with the content of pieces.
...
What I'm missing either:
The first way is best but I don't know if it already exists. In fact, I think that this problem occurs only with array or collections as you can always initialize object fields with the default converter.
I know that an openArray in proc parameters is read only, but the nim compiler will copy its values to result if compatible.
No it will not copy anything. Nim Arrays work like C arrays. It would be equivalent to the C code:
void *arr= const void* openArray
It creates a mutable reference, which cannot happen. It's similar to a Rust borrow.
You can do that because I've used an array instead of a seq[Val] in my small example. When using a dynamic array whose size is not known at compile time, you can't write such code (and that's the reason I used an openArray in my example).
You can write such code! It's easier with a seq[Val] because it computes the size at runtime.
Here is your first example using seq: https://play.nim-lang.org/#ix=23Qp
Here is your second example with seq: https://play.nim-lang.org/#ix=23Qr
I should have been able to call the initGa proc with an array[int] and return an array[Val] as int and Val are compatible.
No! That should not be allowed at all. Int and Val are not compatible! They are distinct types! This is an important feature of Nim that prevents mistakes. Specifically, in your example the Int(0) is not a valid Val type. Nim prevents you from making this mistake.
Nim types are like a Ada types. Just because two types are binary compatible does not mean they are semanticaly compatible (this is why we have the distinct keyword like type meter = distinct Int You cannot convert an int type to a meter type without explicit casting. Range type works the same way.
As Board items default values '0' are not in Val, the compiler will complain with the [ProveInit] warning, and because that's a multidimensional array, I can't tell the compiler that it is initialized if I use multiple initialization loops.
You would not use multiple initialization loops. You would write something like this:
result = array[
array[Val('A'),Val('A'),Val('A'),Val('A'),Val('A'),Val('A'),Val('A'),Val('A'),Val('A'),Val('A')],
array[Val('A'),Val('A'),Val('A'),Val('A'),Val('A'),Val('A'),Val('A'),Val('A'),Val('A'),Val('A')],
array[Val('A'),Val('A'),Val('A'),Val('A'),Val('A'),Val('A'),Val('A'),Val('A'),Val('A'),Val('A')],
array[Val('A'),Val('A'),Val('A'),Val('A'),Val('A'),Val('A'),Val('A'),Val('A'),Val('A'),Val('A')],
array[Val('A'),Val('A'),Val('A'),Val('A'),Val('A'),Val('A'),Val('A'),Val('A'),Val('A'),Val('A')],
array[Val('A'),Val('A'),Val('A'),Val('A'),Val('A'),Val('A'),Val('A'),Val('A'),Val('A'),Val('A')],
array[Val('A'),Val('A'),Val('A'),Val('A'),Val('A'),Val('A'),Val('A'),Val('A'),Val('A'),Val('A')],
array[Val('A'),Val('A'),Val('A'),Val('A'),Val('A'),Val('A'),Val('A'),Val('A'),Val('A'),Val('A')],
array[Val('A'),Val('A'),Val('A'),Val('A'),Val('A'),Val('A'),Val('A'),Val('A'),Val('A'),Val('A')],
array[Val('A'),Val('A'),Val('A'),Val('A'),Val('A'),Val('A'),Val('A'),Val('A'),Val('A'),Val('A')],
]
What I'm missing... a way to specify a default initializer for the Val type, that would be called by the compiler when creating a new variable of type Val, particularly for array and collections.
What you need is a default initializer for array. It has nothing to do with val.
I do think Nim should auto initialize the result variable. I'm not sure if this is a bug in the "proveInit" algorithm or a bug in the way nim is initializing result. It may be worth a bug report but I'm not sure.
as an alternative, I wrote a macro to "initialize" arrays for you: https://play.nim-lang.org/#ix=23QD
What you need is a default initializer for array. It has nothing to do with Val.
According to Nim documentation about variables initialization, array[0.., Val] is initialized to default(Val) which in that case is default(int) and 0 is out of the valid range, reason why the compiler complains.
If I could write (using a new keyword zero to indicate the default value of the type) :
type
Val = range['A' .. 'Z'] zero 'A'
I do think Nim should auto initialize the result variable. I'm not sure if this is a bug in the "proveInit" algorithm or a bug in the way nim is initializing result. It may be worth a bug report but I'm not sure.
From what I can see in the debugger, result is initialized/filled with 0. And this is conformed to the documentation about variables initialization.
As an alternative, I wrote a macro to "initialize" arrays for you.
Thanks. It's more a workaround than a satisfaying solution but I'll see if I can use it in my code. Using the no warning pragma is shorter though ;-)
I understand what you are saying now.
Based on your last reply, I modified the macro to take a "default initialization expression" parameter: https://play.nim-lang.org/#ix=23Zl
The syntax could be made "more beautiful" but I think it closely approximates the feature you are looking for.
The other relevant documentation is here: https://nim-lang.org/docs/manual.html#statements-and-expressions-return-statement
Specifically:
The result variable is always the return value of the procedure. It is automatically declared by the compiler. As all variables, result is initialized to (binary) zero
Nim memsets the memory to binary 0 by default when a variable is initialized (It does not take into account the type at that stage) This is an important thing for memory security etc..., But, as you observe, does not necessarily result in a semantically correct default value for a type. (This is called out in the manual. It's known behavior.)
I agree with you that being able to set a semantically correct default value for a type is a useful feature, but consider that it is not fundamental.
A related issue has been discussed previously here: https://github.com/nim-lang/RFCs/issues/126
and here: https://github.com/nim-lang/RFCs/issues/48
Notably, other popular languages such as Go work the exact same way. There is precedent for the current behavior and there are real costs associated with adding this behavior to the language.
The thing that I am unsure about is how the current behavior should interact with the "Proveinit" algorithm. Proveinit is counter intuitive but technically correct in this case. It is reminding you that Nim has not set a semantically valid default value and you must do so yourself.
Thanks. It's more a workaround than a satisfaying solution but I'll see if I can use it in my code. Using the no warning pragma is shorter though ;-)
It is a work around, but IMO, it is more correct that setting the "no warning" pragma. That silences the warning, which you explicitly stated that you did not want:
My goal is not to disable that compiler warning with compiler flags or pragma, but to write the correct code for the nim compiler.
Unlike disabling or ignoring the warning, my macro solution produces "correct" code :-P.
IMHO, the beauty of Nim is that macros allow you to "fix" small holes in the spec like this in an elegant way. Believe or not, it is actually idiomatic Nim to do something like this. Pick your poison :-P
--warning[ProveInit]:off
It's been like this for years, so don't worry. The same goes for locklevels.
I've some places in my code where I can prove that the variables are correctly initialized but the compiler can't, and other places where I'm not sure the variables are correctly initialized and the compiler correctly find out they are not... So these warning have real use. I just want to reduce the false positive rate.
What is the goal of adding constraints to a language like types to have the compiler help you find bugs when the constraints are not respected, if you disable them instead of helping the compiler enforce them?