[Haskell-cafe] type metaphysics
Luke Palmer
lrpalmer at gmail.com
Mon Feb 2 13:06:04 EST 2009
On Mon, Feb 2, 2009 at 9:47 AM, Martijn van Steenbergen <
martijn at van.steenbergen.nl> wrote:
> Lennart Augustsson wrote:
>
>> 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.
>>
>
> I was thinking about a fixed function type A -> B having uncountably many
> *values* (i.e. implementations). Not about the number of function types of
> the form A -> B. Is that what you meant?
>
> For example, fix the type to Integer -> Bool. I can't enumeratate all
> possible implementations of this function. Right?
That question has kind of a crazy answer.
In mathematics, Nat -> Bool is uncountable, i.e. there is no function Nat ->
(Nat -> Bool) which has every function in its range.
But we know we are dealing with computable functions, so we can just
enumerate all implementations. So the computable functions Nat -> Bool are
countable.
However! If we have a function f : Nat -> Nat -> Bool, we can construct the
diagonalization g : Nat -> Bool as: g n = not (f n n), with g not in the
range of f. That makes Nat -> Bool "computably uncountable".
In summary, the set of total computable functions Nat -> Bool is a countable
set, but this fact is not observable by any algorithm. (so is it
*really*countable after all? :-)
Luke
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/haskell-cafe/attachments/20090202/25c37219/attachment-0001.htm
More information about the Haskell-Cafe
mailing list