Re: [Haskell-cafe] type metaphysics

Do they? Haskell is a programing language. Therefore legal Haskell types has to be represented by some string. And there are countably many strings (of which only a subset is legal type representation, but that's not important). All best Christopher Skrzętnicki On Mon, Feb 2, 2009 at 17:09, Gregg Reynolds wrote:

On Mon, Feb 2, 2009 at 10:05 AM, Andrew Butterfield wrote:

...

Martijn van Steenbergen wrote:

...

...

To my naive mind this sounds suspiciously like the set of all sets, so it's too big to be a set.

Here you're probably thinking about the distinction between countable

and

...

uncountable sets. See also:

http://en.wikipedia.org/wiki/Countable_set

No - it's even bigger than those !

He is thinking of proper classes, not sets.

http://en.wikipedia.org/wiki/Class_(set_theory)

Yes, that's my hypothesis: type constructors take us outside of set theory (ZF set theory, at least). I just can't prove it.

Thanks,

g _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe