[Haskell-cafe] type metaphysics

[Reid Barton]

On Mon, Feb 02, 2009 at 02:41:36PM -0800, Dan Piponi 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

(Warning: sketchy argument ahead.)  Let f :: (Nat -> Bool) -> Nat be a
total function and let g0 = const True.  The application f g0 can
only evaluate g0 at finitely many values, so f g0 = f (< k) for any k
larger than all these values.  So we can write

> toSame f = (const True, head [ (< k) | k <- [1..], f (const True) == f (< k) ])

and toSame is total on total inputs.

Regards,
Reid