On Mon, Feb 2, 2009 at 11:14 PM,
I believe the original notion of type by Russell is most insightful, bridging the semantic notion of type (type as a set of values) and the syntactic notion (type system as a syntactic discipline, a statically decidable restriction on terms).
That point is discussed at some length in Sec 3 (pp. 7-8) of http://okmij.org/ftp/Computation/FLOLAC/lecture.pdf
Fantastic! That's exactly the sort (heh) of thing I was looking for.
Incidentally, Russell has published his paper that introduced types as we in Computer Science know them in 1908. Last year there was 100th anniversary of types. I have been trying to prompt people to have a party and celebrate the occasion -- alas, to no avail.
Also the 100th anniversary of Zermelo's "Untersuchungen über die Grundlagen der Mengenlehre I" (Investigations in the foundations of set theory) - pretty tough competition. Maybe a "Set Theory v. Type Theory All-star Smackdown" would draw a crowd. Lots of beer, mud-wrestling, monster trucks, that sort of thing. Thanks much, gregg