diagonalizacion.lhs

Mail de Conor McBride en la lista de mails de haskell (creo)
----------------------------------------------------------------------------------------------------------------------------
Hi

I'm sorry about the level of consternation this discussion seems to be
generating, so let me attempt to clarify my previous remarks.

The diagonalization argument which shows that any total language
misses some total programs is the usual one: Godel-code everything in
sight, then make the alleged universal program eat a twisted copy of
itself. It's the Epimenides/Cantor/Russell/Quine/Godel/Turing
argument. And it goes like this...

  Suppose we have a programming language in which all expressions
  compute to a value excluding bottom. For sake of argument, let's
  code expressions and values as natural numbers (an ascii source file
  is just a big number; so is a finite output). In particular, every
  function f from Nat to Nat which lives in the language is quoted by a
  code (quote f) :: Nat, and we know a total function which unquotes,
  executing a coded f at a given argument

>    eval :: Nat -> (Nat -> Nat)

  with spec

>    eval (quote f) x = f x
>    eval _         _ = 0

  Given such a function, I can summon up its evil cousin, with spec:

>    evil :: Nat -> Nat

>    evil code = 1 + (eval code code)

  Now, if eval is total, so is evil. But if evil lies within our language,
  it will have a number. Without loss of generality, quote evil is a human
  number and that number is 666. So, we get

>    evil 666
>    = 1 + (eval 666 666)
>    = 1 + evil 666

  which is plainly untrue.

  Hence evil is a total function which is not expressible in the language
  (so eval better not be expressible either).

Of course, for any language of total functions, its Halting Problem is
trivial, but that's beside the point.  There is no largest class of
recognizably terminating programs, because no such class can include
its own *evaluation* function, which is by definition terminating.
Given a total language L, we can always construct a strictly larger
language L', also recognizable, which also includes the eval function
for L.

Meanwhile, back in the cafe, why should Haskellers give a monkeys? Two
reasons: one pertinent now, one potential.

Firstly, when we make (or Haskell derives) recursive instance
declarations, we might like to know that

  (1) the compiler will not go into a spin when attempting to compute the
        object code which generates the dictionary for a given instance
  (2) the code so generated will not loop at run-time

You might argue that (1) is not so important, because you can always
ctrl-C, but (2) is more serious, because if it fails, you get the
situation where the compiler approves your program, then breaks it
by inserting bogus code, promising to deliver an instance which does
not actually exist.

To guarantee these properties, we essentially need to ensure that the
instance declaration language is a terminating fragment of Prolog. The
various flags available now are either way too cautious or way too
liberal: what's a suitable middle way? There is no most general choice.

Secondly, might it be desirable to isolate a recognizable sublanguage of
Haskell which contains only total programs?  Pedagogically, Turner argues
that it's useful to have a `safe' language in which to learn.
Rhetorically, making bottom a value is just sophistry to hide the fact
that looping and match failure are pretty bad side-effects available
within an allegedly pure language---preferable to core-dumps or wiping
your hard drive, but still bad. Logically, if you want to show a program
is correct, it helps if you can get its totality for free. Pragmatically,
there are fewer caveats to optimizing bottomless programs.

As we've seen, such a sublanguage (perhaps called `Ask', a part of Haskell
which definitely excludes Hell) cannot contain all the angels, but it
certainly admits plenty of useful ones who can always answer mundane
things you might Ask. It's ironic, but not disastrous that lucifer, the
evaluation function by which Ask's angels bring their light, is himself an
angel, but one who must be cast into Hell.

Yours religiously

Conor
----------------------------------------------------------------------------------------------------------------------------