Substructural type system

Ordered types correspond to noncommutative logic where exchange, contraction and weakening are discarded.

[1]: 30–31  Without the exchange property, an object may only be used when at the top of the modelled stack, after which it is popped off, resulting in every variable being used exactly once in the order it was introduced.

This allows the system to safely deallocate an object after its use,[1]: 6  or to design software interfaces that guarantee a resource cannot be used once it has been closed or transitioned to a different state.

The nomenclature offered by substructural type systems is useful to characterize resource management aspects of a language.

Uses that don't transfer ownership – borrowing – are not in scope of this interpretation, but lifetime semantics further restrict these uses to be between allocation and deallocation.

As with manual resource management, a practical problem is that any early return, as is typical of error handling, must achieve the same cleanup.

This becomes pedantic in languages that have stack unwinding, where every function call is a potential early return.