
2 Feb
2009
2 Feb
'09
5:04 p.m.
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?