Comment by lmm | Hacker News Reader

Comment by lmm | Hacker News Reader

Parent Full thread

> Can’t the program just accidentally stash the linear type in some list and forget about it?

No, because the type of the list elements would have to be that linear type (and that linear type is not a subtype of any normal type, not even an "Any" type if you have one). So you can only put linear-typed values into a list type that obeys the rules of linear typing (so e.g. you might be able to split the list into head and tail, but you can't just drop n elements from it - and of course the type of the list itself will be linear, or maybe polymorphic in the linearness of its element type), and if you want to implement a more general-purpose list implementation you won't be able to add linear-typed values to that list.

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.

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

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.

Reply on news.ycombinator.com