Hacker News Reader

Comment by two_handfuls | Hacker News Reader

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.

View on HN

A 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.

I see, so in that second case it’s a runtime check rather that a static check. That makes sense.

Depends 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.

I 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.

Reply on news.ycombinator.com