3 ms·
Ok so the list is linear sure, but how can the compiler statically verify that the list will be empty when the program terminates? The emptying could be in a c
by two_handfuls 2y ago
Ok so the list is linear sure, but how can the compiler statically verify that the list will be empty when the program terminates?
The emptying could be in a completely different function, called under some arbitrarily complex condition.
- verdagon 2y agoA really good question. In short, a linear List (or array, or hash map, etc) will only have two available destroyer functions: 1. drop_into(list, func): It consumes the list, calling the given `func` for each element. 2. expect_empty(list): Consumes the list, panicking if the list isn't empty.
- two_handfuls 2y agoI see, so in that second case it’s a runtime check rather that a static check. That makes sense.
- lmm 2y agoDepends on the rest of your type system. If your language is capable of tracking whether a list is empty then it can allow dropping empty lists without a runtime check.
- fallingsquirrel 2y agoI bet expect_empty could be defined roughly as: fn expect_empty(list) { drop_into(list, () => panic()); } (pardon my made up syntax) If you want to discourage runtime checks, you could even make the programmer do the above themselves since it's a one-liner anyway.