[Haskell-cafe] type metaphysics

[Gregg Reynolds]

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/