Re: [Haskell-cafe] type metaphysics

On Mon, Feb 2, 2009 at 3:41 PM, Dan Piponi wrote:

2009/2/2 Luke Palmer :

...

But Nat ~> Bool is computably uncountable, meaning there is no injective (surjective?) function Nat ~> (Nat ~> Bool), by the diagonal argument above.

Given that the Haskell functions Nat -> Bool are computably uncountable, you'd expect that for any Haskell function (Nat -> Bool) -> Nat there'd always be two elements that get mapped to the same value.

So here's a programming challenge: write a total function (expecting total arguments) toSame :: ((Nat -> Bool) -> Nat) -> (Nat -> Bool,Nat -> Bool) that finds a pair that get mapped to the same Nat.

Ie. f a==f b where (a,b) = toSame f

Presumably under the condition that a /= b. It's unlikely that you can. At least you can't use Escardo's trick, because while the space of pairs of cantor spaces (cantor space = Nat -> Bool) is compact, the space of pairs of *different* cantors spaces is not. This is witnessed by the following function: f (a,b) = length (takeWhile id (zipWith (==) a b)) This function finds the first index at which they differ. Since they are guaranteed to be different, this function is total. Thus, if the space of nonequal cantor spaces were compact, then so too would be Nat, which we know is not the case. Luke