Linear/affine lifetimes without subtyping

Are there any type systems similar to rust that don't depend on subtyping ? Can we express that one value must be consumed or dropped before another? For instance if I had an array of huge values on the heap and I would like to operate on a single item using a reference to it, the compiler would need to be sure I had finished with the reference before I could mutate or drop the parent array.

Linear and affine typing systems have been developed in the context of linear logic and process calculi. Most developments of such types do not use subtyping. The system in (1) is pioneering for its use of linearity, as are (2, 3) which introduced session types which are heavily based on linearity. See also the CSTheory Stackexchange thread Determinism and pi-calculus for some other (related) typing systems that make heavy use of linearity and affinity. While all this work is for process calculi, note that sequential behaviour is a well-behaved special case of concurrency and affinity in Rust is closely related (the same) as affinity in process theory.

• N. Kobayashi, B. C. Pierce, D. N. Turner, Linearity and the Pi-Calculus.

• K. Takeuchi, K. Honda, M. Kubo, An Interaction-based Language and its Typing System.

• K. Honda, V. T. Vasconcelos, M. Kubo, Language Primitives and Type Disciplines for Structured Communication-based Programming.

StackExchange Computer Science Q#81401, answer score: 5