[Haskell-cafe] Re: type metaphysics

[Benedikt Huber]

Ryan Ingram schrieb:
> 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:

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