[TYPES] types

[Jacques Carette]

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