The simplest method, omitting the type checking that would be required to verify that any ‘usage’ pre-destruction, any time the type checker encounters an expression that creates a value of linear type the ID (in whatever representation the compiler uses) could be stored in a list of linear object, then when the explicit destruction function is called on a linear object that ID is removed from the list. At the end of compilation (or more likely type checking) if the list is not empty the programmer clearly did not destruct some linear object and an error is issued.

But you’re allowed to destroy in a different function. How does the compiler recognize which ID the variable has?

Also, consider:

    for i in range(100): 
      array[i] = mylinearvariable
    for j in range(100):
      x=complicated(j)
      destroy array[x]

In this case it seems potentially extremely difficult for the compiler to know statically that the array will be empty in the end.

As to recognizing what ID a variable has, compilers often associate a global unique ID with each variable that exists in the translation unit. So when some variable x (or really any semantic object) is initialized to whatever its value is the compiler maps that source code x with ID 16373 (or whatever encoding the compiler is using for the mapping). This ID is what would be held in a ‘linear context’, probably in the type checker, and that ID is removed from the context when it is passed to an appropriate ‘destruction’ function.

As to the pseudo-code, it seems like the ‘mylinearvariable’ is being copied 100 times and placed in the array slots. This is probably not possible for most descriptions of linear types, a key component of said types are that only one can exist. I have some qualms with TFA’s description of their types as linear, although I am pretty sure I understand the usage and acknowledge it is somewhat accepted terminology. Even in TFA I don’t think they would accept such semantics for their linear type. If ‘mylinesrvariable’ is a constructor of sorts creating unique linear objects in each slot, each of those would have an ID in the compiler that would be independently removing each of those IDs when said object is handed to the destroy statement. This sort of simple list/map between objects and IDs only works because the types are linear which means only one exists and there must be a single explicit usage of that object (which is the destruction in the semantics proposed in TFA).

It could, but then that List would have to be linear itself, and then the program would make sure that you eventually drain the list and destroy each element.

(One caveat is for linears in globals, which aren't implemented in Vale yet. We haven't decided which strategy we're going with there, but TFA talks about some)

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