[Haskell-cafe] type metaphysics

[Dan Piponi]

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
--
Dan

(PS I think this is hard. But my brain might be misfiring so it might
be trivial.)