[Haskell-cafe] type metaphysics

[Luke Palmer]

On Mon, Feb 2, 2009 at 3:41 PM, Dan Piponi <dpiponi at gmail.com> wrote:

> 2009/2/2 Luke Palmer <lrpalmer at gmail.com>:
>
> > 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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/haskell-cafe/attachments/20090202/b0d8bc40/attachment.htm