Re: [Haskell-cafe] type metaphysics

Hi, Am Montag, den 02.02.2009, 14:41 -0800 schrieb Dan Piponi:

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

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

toSame _ = (const True, const True)

;-) Joachim -- Joachim "nomeata" Breitner mail: mail@joachim-breitner.de | ICQ# 74513189 | GPG-Key: 4743206C JID: nomeata@joachim-breitner.de | http://www.joachim-breitner.de/ Debian Developer: nomeata@debian.org