[Haskell-cafe] type metaphysics

[Jonathan Cast]

On Mon, 2009-02-02 at 17:30 +0100, Krzysztof Skrzętnicki wrote:
> 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). 

Haskell possesses models[1] in which the carriers of all types are
countable.  Haskell also possesses the models[2] which do assign
uncountable carriers to several Haskell types --- a -> b whenever a has
an infinite carrier (and b is not a degenerate type of the form

newtype B = B B

), [b] under the same conditions on b, etc.  In many cases, these are
the most insightful models, and I those models are what people mean when
they talk about e.g. [Int] having an un-countable denotation.

jcc

[1] IIUC all models based on recursion theory have this property
[2] IIUC most models based on domain theory have this property