Lambda the Ultimate

The use of first-class objects as types, as in Ruby and Smalltalk, is more part of the program expression itself than of any meaningful type-system.

I think this should be emphasized. The way the term "type" is used in the static and dynamic worlds is just different. I doubt you'll find any definition that encompasses both of those usages without becoming absurdly general (like, "a classification system"), so I suggest simply looking for two distinct definitions.

Very roughly, static type systems tend to classify terms, while dynamic types (note that I do not say type "systems") tend to classify values. In this sense they have something in common, but really I think it's better to regard them as completely different.

Type theory means static type theory. There is really no useful theory of what dynamic languages call "types," although there are design cultures for specific languages, e.g, Smalltalk program design tradition.

I think this should be emphasized. The way the term "type" is used in the static and dynamic worlds is just different.

I agree on the emphasis, and add that types also mean something different in modeling languages. In particular, UML classes are often referred to as types, but we're talking about problem domain analysis and identifying real world entities; there is no math involved in doing so, other than relational modeling to ensure these entities pass the Indivisibility Argument in modeling the real world.

Short answer: beware and aware of the context of a vocabulary word.

... each type has a denumerable number of values, which assures that there are only a denumerable number of types.

If a set is denumerable (size aleph null), the set of its subsets is not (size aleph one.) It only makes a difference in theory, since our computers all have finite memories. (Which is not to say that in theory is unimportant. It's just different from in practice in at least this one way.) (Posts correcting other posts always introduce new errors, and I'm sure this one does, too.)

In practice, of course, only finitely many values are representable, which means there are only a finite number of types.

I'm puzzled by the statement that only finitely many values are representable. Could you give a definition of this concept? In my naïve understanding, the following Haskell code:

data Nat = Zero | Succ Nat

describes the classical type with countably infinitely many elements; and, while, on the one hand, we can certainly only write out explicitly a finite number of its elements in any given program, on the other hand, there is no element that can't be so described ^*. To take it further, there's a single program with the property that, for any given element ^* of Nat, it will ‘represent’ it in finite time:

let nats = Zero : map Succ nats in show nats

It thus seems to me that all elements of the type are representable. Of course, though, you know all this, which makes me think that I must not have the right definition of ‘representable’.

When I first tried to learn about a rigorous foundation for the theory of types (which is not too far away from when I last tried to learn about it, so take this with a grain of thought), I was immediately drawn, as a mathematician, to the idea of types as sets—but then I saw that types are not sets. Of course, the abstract immediately says “[t]he title is not a statement of fact”, and moves on to less provocative waters, but it has left me puzzled. For example, a term in most type systems has only one type (or, at best, a polymorphic type like Num a => a); but, in real life, an element of an infinite set will belong to infinitely many of its subsets (so we would need, in pseudo-Haskell, some sort of type constraint like term :: type `Contains` term => type, which seems so vague as to be useless). Again, this is all just coming from my attempts to generalise my mathematical understanding way too far into computer science. Could you clarify the meaning of the equation in your title?

^* I'm intentionally ignoring the (non-)distinction between data and co-data that leads to constructions like

inf = Succ inf

because I don't understand it well enough to feel confident of not saying something foolish.

For example, a term in most type systems has only one type ... but, in real life, an element of an infinite set will belong to infinitely many of its subsets

The root of the difficulties with the "type = set" definition that others are pointing out is that that a set is a first order entity in the universe of sets, whereas a type is a second order entity defined over some other universe of terms or values, and is intended to partition those terms or values in some restricting way.

This pretty much precludes it being closed under all the same operations that sets are closed under.

PS I got a smile from your implied definition of "real life". ;-)

The 'types = subsets' notion too easily confuses readers, who take that and tweak it ever so slightly to 'subtypes = subsets', which fails to capture covariance vs. contravariance and the resulting multi-dimensional data-type lattices.

The 'subsets' notion also doesn't generalize well to types on the structure of the program or the relationships between values, such as dependent typing, constraint typing, linear typing, uniqueness types.

I've abandoned use of 'subsets' in attempting to explain types for these reasons.

That paper was pretty much exactly what I was looking for. It is nice to see that typing is also being explored through dynamic semantics as well.

Perhaps it's worth pointing to this and this very old thread on the subject. In particular, I still feel, intuitively, that Ontic has important things to teach us in this regard.