[Haskell-cafe] Re: type metaphysics

Ryan Ingram schrieb:

2009/2/2 Luke Palmer :

...

However! If we have a function f : Nat -> Nat -> Bool, we can construct the diagonalization g : Nat -> Bool as: g n = not (f n n), with g not in the range of f. That makes Nat -> Bool "computably uncountable".

This is making my head explode. How is g not in the range of f?

In particular, f is a program, which I can easily implement; given:

f is 'easy to implement' if it enumerates all functions, not just total ones. Otherwise, f is hard to implement ;) In the first case, if we have (f n n) = _|_, then g n = not (f n n) = _|_ as well, so the diagonalization argument does not hold anymore. But I do agree that proofs by contradiction do not map well to haskell ... benedikt

compiler :: String -> Maybe (Nat -> Bool) mkAllStrings :: () -> [String] -- enumerates all possible strings

I can write f as

f n = validPrograms () !! n where validPrograms = map fromJust . filter isJust . map compiler . mkAllStrings

Now, in particular, mkAllStrings will generate the following string at some index, call it "stringIndexOfG":

<source code for compiler> <source code for mkAllStrings> <source code for f> g n = not (f n n)

This is a valid program, so the compiler will compile it successfully, and therefore there is some index "validProgramIndexOfG" less than or equal to "stringIndexOfG" which generates this program.

But your argument seems to hold as well, so where is the contradiction?

-- ryan