[Haskell-cafe] type metaphysics

[Lennart Augustsson]

The Haskell function space, A->B, is not uncountable.
There is only a countable number of Haskell functions you can write,
so how could there be more elements in the Haskell function space? :)
The explanation is that the Haskell function space is not the same as
the functions space in set theory.  Most importantly Haskell functions
have to be monotonic (in the domain theoretic sense), so that limits
the number of possible functions.

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

  -- Lennart

On Mon, Feb 2, 2009 at 3:49 PM, Martijn van Steenbergen
<martijn at van.steenbergen.nl> wrote:
> 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.
>
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>