[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
The history of type theory is actually rather well laid out at
http://en.wikipedia.org/wiki/History_of_type_theory.
I have not read this book
http://www.amazon.com/History-Philosophy-Constructive-Synthese-Library/dp/9048154030
but it appears topical.
However, I am quite surprised that no one has yet mentioned "A Modern
Perspective on Type Theory",
http://www.springer.com/mathematics/book/978-1-4020-2334-7
which takes a historical path through type theory. Perhaps because the
types mailing list is inhabited by mainly PL people?
Having said that, I want to focus on a particular aspect of the question:
On 2014-05-12 1:47 PM, Vladimir Voevodsky wrote:
The types which we use today are a constructive tool. For example, types in
Ocaml are a device without which writing many programs would be extremely
inconvenient.
While many have been quite philosophical about what this means, I think
something quite simple is being forgotten here: pattern matching.
Without types, eliminators for sums are very awkward to deal with.
While one can argue how much benefit there is in types for those whose
values are given largely through their introduction form, types really
shine when types are largely given by their elimination forms. Oh, it
is possible to program entirely in terms of eliminators, but the results
are "extremely inconvenient" indeed!
To me, types enable a nice concept of sum types, which in turn enable a
nice notion of pattern matching . [I use 'enable' here, knowing that
one can do pattern matching without sums and without types, but the
results are not as compelling.] And pattern matching allows programs to
be written much more succinctly and clearly than without.
Jacques
