Every time I want to quickly understand something about an advanced type system or programming language concept I get lost when I see something like this on Wikipedia:
Linear type systems are the internal language of closed symmetric monoidal categories, much in the same way that simply typed lambda calculus is the language of Cartesian closed categories. More precisely, one may construct functors between the category of linear type systems and the category of closed symmetric monoidal categories.
Why there’s so much research around types if perfectly applying them to programming languages is impractical? 1 It turns out mathematicians are the ones behind the development of most of the work related to type systems – type theory.2 One might think they do this to support programming languages. After all, it’s part of the job of mathematicians to formalize what other disciplines developed with a more practical mindset. Infinitesimal calculus was greatly advanced by Isaac Newton to solve immediate problems in physics for example. But the development and study of type theory pre-dates programming languages! What problems were mathematicians trying to solve when they developed type theory, a curious programmer might ask.