Hi, The concept of "type" seems to be a little like porno: I know it when I see it, but I can't define it (apologies to Justice Stewart). I've picked through lots of documents that discuss types in various ways, but I have yet to find one that actually says what a type "really" is. For example, definitions of the typed lambda calculus usually define some type symbols and rules like "a : T means a is of type T", and then reasoning ensues without discussion of what "type" means. The only discussion I've found that addresses this is at the Stanford Encyclopedia of Philosophy, article "Types and Tokens" [1]. It's all very philosophical, but there is one point there that I think has relevance to Haskell. It's in section 4.1, discussing the distinction between types and sets: "Another closely related problem also stems from the fact that sets, or classes, are defined extensionally, in terms of their members. The set of natural numbers without the number 17 is a distinct set from the set of natural numbers. One way to put this is that classes have their members essentially. Not so the species homo sapiens, the word 'the', nor Beethoven's Symphony No. 9. The set of specimens of homo sapiens without George W. Bush is a different set from the set of specimens of homo sapiens with him, but the species would be the same even if George W. Bush did not exist. That is, it is false that had George W. Bush never existed, the species homo sapiens would not have existed. The same species might have had different members; it does not depend for its existence on the existence of all its members as sets do." So it appears that one can think of a type as a predicate; any token (value?) that satisfies the predicate is a token (member?) of that type. This gives a very interesting way of looking at Haskell type constructors: a value of (say) Tcon Int is anything that satisfies "isA Tcon Int". The tokens/values of Tcon Int may or may not constitute a set, but even if they, we have no way of describing the set's extension. My hunch is that it /cannot/ be a set, although I'm not mathematician enough to prove it. My reasoning is that we can define an infinite number of data constructors for it, including at least all possible polynomials (by which I mean data constructors of any arity taking args of any type). To my naive mind this sounds suspiciously like the set of all sets, so it's too big to be a set. In any case, Tcon Int does not depend on any particular constructor, just as homo sapiens does not depend on any particular man. So it can't be a set because it doesn't have its members essentially. (I suspect this leads to DeepThink about classical v. constructivist mathematics, but that's a subject for a different discussion.) I'm not sure that works technically, but it seems kinda cool. My question for the list: is the collection of e.g. Tcon Int values a set, or not? If it is, how big is it? Thanks, gregg [1] http://plato.stanford.edu/entries/types-tokens/