
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