Where Do Type Systems Come From?

Watch Oregon Programming Language School lectures &quot;Basic Proof Theory&quot; by Frank Pfenning.<p><a href="https:&#x2F;&#x2F;www.cs.uoregon.edu&#x2F;research&#x2F;summerschool&#x2F;summer15&#x2F;curriculum.html" rel="nofollow">https:&#x2F;&#x2F;www.cs.uoregon.edu&#x2F;research&#x2F;summerschool&#x2F;summer15&#x2F;cu...</a><p>Very clean and easy to follow video lectures on the relation between, types, programs, and logical proofs. One does not need functors and monoids to appreciate the beauty of functional type systems. (And to see why such type systems are indeed discovered rather than invented.)

It&#x27;s a common misconception that Russell&#x2F;Whitehead &quot;invented&quot; type theory. In fact, Frege had already made the very insightful distinction between functional and non-functional types in the 1890s -- <i>this</i> was the key development that Russell based his hierarchy of types on. See &quot;Function and Concept&quot; (1891)[1]. It was a growing and communal sentiment that a (meta-)theory of types would make certain mathematical concepts more palatable.<p>If anything, I think the conceptual father of type theory is Gottlob Frege, and Alonzo Church was the first to apply it concretely.<p>[1] <a href="http:&#x2F;&#x2F;fitelson.org&#x2F;proseminar&#x2F;frege_fac.pdf" rel="nofollow">http:&#x2F;&#x2F;fitelson.org&#x2F;proseminar&#x2F;frege_fac.pdf</a>

If you haven&#x27;t thought much about type systems but want to understand what the big deal is, I wrote a post specifically for you [1]. It draws motivation for wanting a good static type system from first principles.<p>[1] <a href="https:&#x2F;&#x2F;gilbert.ghost.io&#x2F;type-systems-for-beginners-an-introduction&#x2F;" rel="nofollow">https:&#x2F;&#x2F;gilbert.ghost.io&#x2F;type-systems-for-beginners-an-intro...</a>

Nice article. I especially liked:<p>&gt; 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.<p>Here I had no idea that JavaScript implicitly typed `runFunction` that way. That&#x27;s cool.<p>Also, I never thought of &quot;higher-order functions&quot; as breaking into a countable hierarchy of nth-order functions, which is an interesting thought. In Haskell the hierarchy would start off as<p><pre><code> zerothOrderFunction :: a firstOrderFunction :: a -&gt; b SecondOrderFunction :: a -&gt; (b -&gt; c) SecondOrderFunction&#x27; :: (a -&gt; b) -&gt; c </code></pre> In general, an nth-order function is a function which either<p>1. Takes an (n-1)th order function as an input and returns a simple type.<p>2. Takes a simple type as an input and returns an (n-1)th order function as an output.<p>The upshot is that typed programming languages not only catch bugs, but prevent you from legally expressing many non-sensical expressions (analogous to the set theory paradoxes). For example, consider the expression<p><pre><code> (\x -&gt; x x) (\x -&gt; x x) </code></pre> If you expand this expression, it reduces to itself:<p><pre><code> (\x -&gt; x x) (\x -&gt; x x) == (\x -&gt; x x) (\x -&gt; x x) </code></pre> In a purely untyped language, this expression would be legal. But what would be its meaning? Arguably, it is non-sense, and should be excluded from the set of legally expressible expressions. The way to do this is through a type system. And indeed, if you typed this statement into a Haskell REPL you would get a type error; this statement can actually be proven to be untypable (IIRC).<p>On the other hand, this means that typed systems are in some sense <i>strictly less expressive than their untyped counterparts</i>. It would therefore be interesting if somebody found an expression which was both (i) meaningful and (ii) <i>only</i> expressible in an untyped language. You would then have an argument for untyped languages :-)

What a great piece!<p>I wish the author would expand on this piece with either more installments or a even short book.<p>I find myself interested in type systems as it relates to programming language design but I haven&#x27;t found much middle ground between the basic types described in introductory texts about a language and the opposite extreme heavy academic texts such as the ones the author is breaking down in this article.<p>Can anyone recommend any other such middle ground resources on type systems and type system theory?

There&#x27;s another approach, from Boyer and Moore. Boyer and Moore built up mathematics from constructs at the Peano axiom level (zero, add1, etc.) plus recursive functions that must terminate. It&#x27;s constructive mathematics; there are no quantifiers, no ∀ or ∃. [1] They built an automatic theorem prover in the 1970s and 1980s that works on this theory. (I recently made it work on Gnu Common LISP and put it on Github, so people can run it again.)[2]<p>In Boyer-Moore theory, all functions are total - you can apply any function to any object. Types are predicates. Here&#x27;s a definition of ORDERED for a list of number:<p><pre><code> (DEFN ORDERED (L) (IF (LISTP L) (IF (LISTP (CDR L)) (IF (LESSP (CADR L) (CAR L)) F (ORDERED (CDR L))) T) T)) </code></pre> If L is not a list, it is considered to be ordered. This makes it a total function, runnable on any input, even though the result for the &quot;wrong&quot; type is not useful. This provides the benefits of types without requiring a theory of types. It&#x27;s a very clean way to look at the foundations of mathematics. It&#x27;s simpler than Russell and Whitehead.<p>When you prove things using definitions like this, there&#x27;s a lot of case analysis. This gets worse combinatorially; a theorem with four variables with type constraints will generate at least 2⁴ cases, only one of which is interesting. Most of the cases, such as when L is not a list, are trivial, but have to be analyzed. Computers are great at this, and the Boyer-Moore prover deals with those cases without any trouble. But it went against a long tradition in mathematics of avoiding case analysis. That made this approach unpopular with the generation of pre-computer mathematicians. Today, it would be more acceptable.<p>(It&#x27;s fun to run the Boyer-Moore prover today. In the 1980s, it took 45 minutes to grind through the basic theory of numbers. Now it takes a few seconds.)<p>[1] <a href="https:&#x2F;&#x2F;www.amazon.com&#x2F;Computational-Logic-Robert-S-Boyer&#x2F;dp&#x2F;1483236528" rel="nofollow">https:&#x2F;&#x2F;www.amazon.com&#x2F;Computational-Logic-Robert-S-Boyer&#x2F;dp...</a> [2] <a href="https:&#x2F;&#x2F;github.com&#x2F;John-Nagle&#x2F;nqthm" rel="nofollow">https:&#x2F;&#x2F;github.com&#x2F;John-Nagle&#x2F;nqthm</a>

Reminded me of Gödel&#x27;s incompleteness theorems.<p>First incompleteness theorem<p>Any consistent formal system F within which a certain amount of elementary arithmetic can be carried out is incomplete; i.e., there are statements of the language of F which can neither be proved nor disproved in F.<p>Second incompleteness theorem<p>For any consistent system F within which a certain amount of elementary arithmetic can be carried out, the consistency of F cannot be proved in F itself.

I share the author&#x27;s frustration with wikipedia sometimes - people usually go to wikipedia for a distilled, comprehensible description of the subject matter. What he quoted was certainly not comprehensible, even to someone well-educated in CS foundations.

I loved this because I have read most of the source material in the context of logic, but never made the lead to type theory in computer science.

Types are close to adjoint functors &#x2F; adjunctions and partial evaluation. Assigning restricted information to part of a structure to gain knowledge through limitation (math).

Type Systems come from Russel - yup. But the notion of Type has an interesting origin in the west as well (I would love to read&#x2F;understand histories of this concept from other cultures, but I am ignorant for now).<p>My reading is that it was invented by Scotus as Haecceity ! This was required by Catholic Christianity because of the difficulty that The Creed introduces about the identity of God - there are three entities which represent God, the Trinity - how to account for this? Well; the thisness of God is joined with the thisness of man, the thisness of the creator and the thisness of the thing which is motion (I have never understood The Holy Spirit). You can think of this as multiple inheritance! Theologians then had to account for &quot;why three&quot; as you can carry on making aspects of god with this mechanism infinitely, god the mother, god the lover, god the hunter and so on. But there are three - why? The answer was provided by Scotus&#x27;s student Occam, entities should not multiply beyond necessity and hence there are three aspects of god because it is necessary for creation that there are.<p>The fun bit it that this procession of thought is somewhat guessed at because writing things like this down or debating them publically was a quick route to the afterlife via a bonfire!

This article was very well written. It finally clicked for me why &quot;hugher-order functions&quot; are named the way they are.<p>Any more articles in this vein?

&quot;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!&quot;<p>This is great point, and I think it is absolutely worthwhile to put time into researching better, more powerful type systems.<p>Tony Hoare said[1] that his research into formal systems and his hope that the pr Framing world would embrace these new innovations that increase safety and reliability was futile, but I think what we need <i>is a new approach, with particular care given to practicality and adoptability</i>.<p>[1] <a href="https:&#x2F;&#x2F;en.wikipedia.org&#x2F;wiki&#x2F;Tony_Hoare" rel="nofollow">https:&#x2F;&#x2F;en.wikipedia.org&#x2F;wiki&#x2F;Tony_Hoare</a>

I feel kinda alone on HN, Lobste.rs and LtU in not having in-depth knowledge or opinions on type systems. I get that these underpin the technology we as programmers use every single day, but I&#x27;m a little ashamed that I can&#x27;t get excited about the subject and feel like it&#x27;s too late for me to bother trying.

&gt; That’s the equivalent of writing type annotations for programming functions. And the goal is avoiding bugs instead of logical contradictions.<p>mh, given Curry–Howard correspondence, aren&#x27;t those the same? so the goal is indeed not having logical contradictions?

&quot;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.&quot;<p>It&#x27;s actually just a belief. Nothing suggests that type systems and type theories can be improved to be practical at preventing bugs. I&#x27;d say it&#x27;s the opposite, even with as much understanding about the nature of bugs as we have today, they don&#x27;t look very promising, unlikely to make it even into the top ten of other different approaches.

I found Tomas Petricek&#x27;s essay on &quot;Against a universal definition of &#x27;Type&#x27;&quot; very informative. He argues that the word &#x27;type&#x27; has shifted shape many times since Frege&#x2F;Russel, in that the intuition behind them is different. He also argues that multiplicity of definition is a good thing.<p><a href="http:&#x2F;&#x2F;tomasp.net&#x2F;academic&#x2F;papers&#x2F;against-types&#x2F;" rel="nofollow">http:&#x2F;&#x2F;tomasp.net&#x2F;academic&#x2F;papers&#x2F;against-types&#x2F;</a>

Nice article about type theory.<p>&gt; Why there’s so much research around types if perfectly applying them to programming languages is impractical?<p>Somehow Haskell does this perfectly. Whaddya say to that?

Types aren&#x27;t just for programming and philosophy. Strongly Typed Neural Networks are also a thing. <a href="https:&#x2F;&#x2F;arxiv.org&#x2F;abs&#x2F;1602.02218" rel="nofollow">https:&#x2F;&#x2F;arxiv.org&#x2F;abs&#x2F;1602.02218</a>

TL;DR - Type theory == being careful about the domain a function can be applied in (adding meters to seconds or strings to sets should not be possible).

Don&#x27;t they teach this stuff in school?

Distinctly unimpressed by this post. The author seems to have an axe to grind with mathematicians as a class, which, as we would have been told in school, isn&#x27;t &#x27;big or clever&#x27;.<p>The whole of programming, nevermind types, perhaps the most mathematical part of modern programming, arises from mathematics. There&#x27;s some good history here, but the early paragraphs in particular are a display of ignorance if not arrogance.<p>The author quotes Newton, the very chap who&#x27;s said to have said he merely stood on the shoulders of giants (to &#x27;see&#x27; such insight). Any programmer in the 21st century stands on the shoulders of mathematicians and computer scientists of the 20th,; who were in turn standing on the shoulders of the mathematicians of the 19th centuries.