[Haskell-cafe] type metaphysics

Ryan Ingram ryani.spam at gmail.com
Mon Feb 2 17:39:25 EST 2009

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

More information about the Haskell-Cafe mailing list