On Mon, Feb 2, 2009 at 11:14 PM, <oleg@okmij.org> wrote:

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