[Haskell-cafe] type metaphysics

[Richard O'Keefe]

Talking about the class of all Haskell types is a little tricky.
If one program has
	data Foo x = Ick x | Ack x
and another program has
	data Bar y = Ack y | Ick y
are {Program1}Foo and {Program2}Bar the same type or not?
They are certainly isomorphic.

Any Haskell program can be represented as a sequence of bytes.
(Proof: take your source tree, and use tar, pax, cpio, or whatever.)
There is therefore a countable infinity of Haskell programs.
In Haskell 98, a program can generate at most a countable infinity
of types (taking a 'type' here to be an element of the "Herbrand
base" generated by the type constructors, speaking somewhat loosely).
So surely there can be at most a countable infinity of Haskell types?