[Haskell-cafe] Re: type metaphysics

[Ryan Ingram]

On Mon, Feb 2, 2009 at 3:55 PM, Benedikt Huber <benjovi at gmx.net> wrote:
> 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.

Thanks for the insight, I see the contradiction!

Luke said:
> But we know we are dealing with computable functions, so we can just
> enumerate all implementations.  So the computable functions
> Nat -> Bool are countable.

The contradiction is this: f, as specified by Luke enumerates all
computable functions.  But f is uncomputable!  So while we can show
that the number of computable functions is at most countable (due to
the number of programs being countable), we cannot actually enumerate
which ones they are.  Since f is uncomputable, so is g.

Therefore, there is no diagonalization; even if we had a magic oracle
that enumerated the set of computable functions, g would not be
present, since it is not computable!

On the other hand, if we allow f to construct nonterminating
functions, as in my implementation, g does not diagonalize, as
Benedikt pointed out!

  -- ryan