About the state of art that I'm running ahead of Type Theory I have the these questions all related about history of Types.

  1. Where did the idea of Type come from? (It seems that all start when Russell and Whitehead propose a way to avoid the contradiction that we know today as Russell's Paradox, am I right?)
  2. Before considering the type concept, was there something similar? (Maybe a refinement of a set, but I don't find a reference distinct of Russell).
  3. Who was the first person to put it on formal terms? (Was Russell with this paper of 1908 or ?
  • 1
    $\begingroup$ There has been a bunch of discussions on this topic in recent years on the TYPES forum. Here is an entry-point to one of their conclusions. $\endgroup$ – gallais Apr 29 '16 at 19:03
  • $\begingroup$ For its use in compilers, early languages needed type information to compile (and some still do). This notion of type ended up developing somewhat separately of the type-theoretic notion, I think. $\endgroup$ – jmite Jun 1 '16 at 16:34

Depends on how deep you want to go. I believe Russell was the guy who introduced the concept in a specifically set-theoretic context, but the concept itself is as old as the hills, it's really the notion of universals and particulars expressed in a modern mathematical / computational form. I wouldn't be surprised if Liebniz did something vaguely like types, if you look at his stuff in the right way.

You might have better luck at the History of Math and Science exchange.

| cite | improve this answer | |
  • $\begingroup$ @Andrej Bauer: Well then it's a good that I didn't claim that he did, as you can see from my second sentence. See also secton 1, sentence 1 of the SEP article on Type Theory. $\endgroup$ – user48832 Jun 1 '16 at 17:29
  • $\begingroup$ @Andrej Bauer: It's not a representation of anything Russel did or did not do. It's an expression of my understanding. I happen to think its also correct. Notice I did not say "originate". $\endgroup$ – user48832 Jun 1 '16 at 17:52
  • $\begingroup$ @Andrej Bauer: And I believe I understand your point about not claiming that Russel's type ideas are set theoretic ideas. But I think it would be stretch to go to the other extreme and deny that his type ideas were introduced in a set theoretic context. $\endgroup$ – user48832 Jun 1 '16 at 17:57
  • $\begingroup$ If your objection is that he wasn't the first then please expand. That was the OP's question - where did it gwt started? - and I'd like to know too. $\endgroup$ – user48832 Jun 1 '16 at 18:01
  • $\begingroup$ @Andrej Bauer: The very first sentence of the appendix to which you refer starts "The doctrine of types is here put forward tentatively, as affording a possible solution of the contradiction;..." In my view "the contradiction" is a clear and direct reference to the previous discussion, which is all about, well, classes, but that just reflects a change in vocab between then and now. It seems very clear he had what we now call "sets" (and maybe more) in mind. $\endgroup$ – user48832 Jun 1 '16 at 18:28

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.