There is a family of unusual type systems called substructural type systems. Many programmers have never encountered them, while other have encountered them without realizing what they are or what’s the idea behind them. We will try to shed some light on where substructural type systems come from, by giving a quick tour of their theoretical background, which comes from sequent calculus. To keep this short enough, we will go only over the parts that are useful for examining type systems.
