[Haskell-cafe] type metaphysics

[Ryan Ingram]

2009/2/2 Luke Palmer <lrpalmer at gmail.com>:
> 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:

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