Substructural types

A type system is substructural just when it fails to satisfy at least one of the usual structural rules, e.g. weakening, contraction, or exchange.

Perhaps the most common case is a linear system that omits weakening and contraction, thus requiring all variables to be used exactly once, but not imposing any restrictions on their ordering.

Languages with substructural types

• Granule
• Idris 2
• Linear Haskell
• ATS

References

• See the Wikipedia page on substructural type systems.