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 vari

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