Where do Type Systems Come From?
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 predates programming languages! What problems were mathematicians trying to solve when they developed type theory, a curious programmer might ask.
The development of a theory of types started with Bertrand Russell in the beginning of the 20th century in Appendix B of The Principles of Mathematics (1903). It was developed as part of the effort to to describe new foundations for mathematics from which all mathematical truths could in principle be proven using symbolic logic.
In short, type theory was developed to be an alternative to set theory as the foundation of mathematical proofs in symbolic logic due to its ability to solve some contradictions stemming from naive set theory. ^{3} Later, type theory referred to a whole class of formal systems. There are many type theories.
In part I of his Mathematical Logic as Based on the Theory of Types paper published in 1908, Russell lists many of such contradictions and finds a commonality in them.
In all the above contradictions (which are merely selections from an indefinite number) there is a common characteristic, which we may describe as selfreference or reflexiveness.
The simplest form of this kind of contradiction is the person who says â€śI am lying;â€ť if she is lying, she is speaking the truth and if she is speaking the truth, she is lying. Russell rewrites â€śI am lyingâ€ť many times to find the root cause of the contradiction.
â€śI am lyingâ€ť becomes â€śThere is a proposition which I am affirming and which is falseâ€ť. All propositions that say â€śthere is soandsoâ€ť may be regarded as saying that the negation of â€śsoandsoâ€ť is not always true. We can now rewrite â€śI am lyingâ€ť to â€śIt is not true of all propositions that either I am not affirming them or they are trueâ€ť in other words â€śIt is not true for all propositions p that if I affirm p, p is true.â€ť The â€śI am lyingâ€ť paradox results, according to Russell, from regarding that as a proposition. This makes it evident that the notion of â€śall propositionsâ€ť is illegitimate; for otherwise, there must be propositions (such as the above) which are about all propositions, and yet can not, without contradiction, be included among the propositions they are about. Whatever we suppose to be â€śall propositions,â€ť statements about them generate new propositions which must lie outside â€śall propositionsâ€ť to avoid a contradiction. Regarding â€śall propositionsâ€ť as a meaningless phrase will avoid us many contradictions. Similarly, in set theory, we should not consider â€śthe set of all setsâ€ť to be a legitimate set.
In part IV, Russell proposes the hierarchy of types
A type is defined as the range of significance of a propositional function, i.e., as the collection of arguments for which the said function has values. Whenever an apparent variable occurs in a proposition, the range of values of the apparent variable is a type, the type being fixed by the function of which â€śall valuesâ€ť are concerned. The division of objects into types is necessitated by the reflexive fallacies which otherwise arise.
Thatâ€™s the equivalent of writing type annotations for programming functions. And the goal is avoiding bugs instead of logical contradictions.
Itâ€™s called hierarchy of types because it separates propositions into orders:
A proposition containing no apparent variable we will call an elementary proposition. [â€¦] The terms of elementary propositions we will call individuals; these form the first or lowest type.
[â€¦]
Elementary propositions together with such as contain only individuals as apparent variables we will call firstorder propositions. These form the second logical type.
[â€¦] We can thus form new propositions in which firstorder propositions occur as apparent variables. These we will call secondorder propositions; these form the third logical type. Thus, e.g, if Epimenides asserts that â€śall firstorder propositions affirmed by me are false,â€ť he asserts a secondorder proposition; he may assert this truly, without asserting truly any firstorder proposition, and thus no contradiction arises.
For a programming analogy, letâ€™s try to create a function capable of running all functions
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 

All programs above are syntactically valid. program1
and program2
will finish
(they halt). program3
also finishes, but will be due to an error caught by
JavaScript interpreter checks.
1 2 3 4 5 6 

program3
fails because runFunction
can only run firstorder functions and
runFunction
is a secondorder function â€“ a function that takes a firstorder
function as a parameter.
If we redefine runFunction
in Typescript as
1 2 3 

The typechecker will yell at us about program3
1 2 3 4 5 6 

Every programmer knows that type systems canâ€™t prevent all bugs. Similarly, type theory wasnâ€™t enough to describe new foundations for mathematics from which all mathematical truths could in principle be proven using symbolic logic. It wasnâ€™t enough because this goal in its full extent is unattainable.
Even though theoretically, type theories and type systems are not enough to prevent all the problems in logic and programming, they can be improved and refined to prevent an increasingly number of problems in the practice of logic and programming. That means the research for better practical type systems is far from over!
References
Russell, Bertrand, â€śThe Principles of Mathematicsâ€ť, 1903.
Russell, Bertrand, â€śMathematical Logic as Based on the Theory of Typesâ€ť, 1908, American Journal of Mathematics.
Coquand, Thierry, â€śType Theoryâ€ť, The Stanford Encyclopedia of Philosophy.
Constable, Robert, The Triumph of Types: Principia Mathematicaâ€™s Impact on Computer Science,, 2011, Proceedings of 10th Annual Oregon Programming Languages Summer School.
Notes

In fact, automatic proof assistants rely on type theories to achieve correctness (e.g. Coq).Â ↩

Making a distinction between type theory and type system is necessary. A programming language type system is analogous to a type theory. A type system is a feature of a programming language. Itâ€™s concerned with how to represent types in a machine and other things.Â ↩

A quick explanation of these paradoxes can be found in the Stanford Encyclopedia of Phylosophy.Â ↩