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? It turns out mathematicians are the ones behind the development of most of the work related to type systems – type theory. 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.

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.

Bertrand Russell – Widely held to be one of the 20th century's premier logicians.

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. 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 self-reference 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 so-and-so” may be regarded as saying that the negation of “so-and-so” 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 first-order propositions. These form the second logical type.

[…] We can thus form new propositions in which first-order propositions occur as apparent variables. These we will call second-order propositions; these form the third logical type. Thus, e.g, if Epimenides asserts that “all first-order propositions affirmed by me are false,” he asserts a second-order proposition; he may assert this truly, without asserting truly any first-order 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

function runFunction(func) { return func(1); } function addTwo(param) { return 2 + param; } function multiplyByTwo(param) { return 2 * param; } function program1() { return runFunction(addTwo); } function program2() { return runFunction(multiplyByTwo); } function program3() { return runFunction(runFunction); }

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

>> program1() 3 >> program2() 2 >> program3() TypeError: func is not a function

program3 fails because runFunction can only run first-order functions and runFunction is a second-order function – a function that takes a first-order function as a parameter.

If we redefine runFunction in Typescript as

1 2 3

function runFunction(func: (param: number) => any) { return func(1); }

The type-checker will yell at us about program3

1 2 3 4 5 6

function program3() { return runFunction(runFunction); } ^ Argument of type '(func: (param: number) => any) => any' is not assignable to parameter of type '(param: number) => any'. Types of parameters 'func' and 'param' are incompatible. Type 'number' is not assignable to type '(param: number) => any'. function runFunction(func: (param: number) => any): any

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

from Hacker News https://ift.tt/3uwCnTB