[Haskell-cafe] Re: type metaphysics

[oleg at okmij.org]

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.