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 The one of the main points of these FLOLAC lecture notes was to justify and illustrate the claim that A type is a (quickly decidable) approximation of a dynamic behavior that can be derived from the form of an expression. (The other claim was the relationship between sharing and polymorphism). 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.
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
participants (2)
-
Gregg Reynolds -
oleg＠okmij.org