[Haskell-cafe] type metaphysics

[Martijn van Steenbergen]

Hi Gregg,

Firsly: I'm not an expert on this, so if anyone thinks I'm writing 
nonsense, do correct me.

There are many answers to the question "what is a type?", depending on 
one's view.

One that has been helpful to me when learning Haskell is "a type is a 
set of values." When seen like this it makes sense to write:
() = { () }
Bool = { True, False }
Maybe Bool = { Nothing, Just True, Just False }

Recursive data types have an infinite number of values. Almost all types 
belong to this group. Here's one of the simplest examples:

data Peano = Zero | Suc Peano

There's nothing wrong with a set with an infinite number of members.

Gregg Reynolds wrote:
> 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.  

Int has 2^32 values, just like in Java. You can verify this in GHCi:

Prelude> (minBound, maxBound) :: (Int, Int)
(-2147483648,2147483647)

Integer, on the other hand, represents arbitrarily big integers and 
therefore has an infinite number of elements.

> 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

Haskell has types which have uncountably many values. They are all 
functions of the form A -> B, where A is an infinite type (either 
countably or uncountably).

If a set is countable, you can enumerate the set in such a way that you 
will reach each member eventually. For Haskell this means that if a type 
"a" has a countable number of values, you can define a list :: [a] that 
will contain all of them.

I hope this helps! Let us know if you have any other questions.

Martijn.