On Mon, Feb 2, 2009 at 9:47 AM, Martijn van Steenbergen < martijn@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