3 ms·

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 expre

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.

two_handfuls 2y ago
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.
- throwaway17_17 2y ago
  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).

two_handfuls 2y ago

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.

throwaway17_17 2y ago
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).