On 12-Jun-1998, Alastair Reid <[EMAIL PROTECTED]> wrote:
>
> Fergus Henderson <[EMAIL PROTECTED]> points out that our exception handling
> scheme hits problems if you hit an infinite loop instead of an exception.
>
> Yes, this is a problem - and not a pretty one.
>
> Fixes:
...
> 3) Add timeouts (and ctrl-C handling) into the mix - practical
> approximations to solving the halting problem.
>
> Fergus then lists a bunch of options and says:
>
> > Of these options, I'm afraid that (a), the status quo, is looking to me
> > like the best of a bad lot, albeit with (c) (i) a close second.
>
> ... some of us have to write programs that keep working. For example,
> I'm busy hacking on our Robo-Haskell code at the moment - it just isn't
> acceptable for that kind of code to print an error message and halt.
For programs like that, where reliability is very important, wouldn't
it be better to use deterministic exceptions [i.e. (c)(i)], even if
it means giving up some optimization?
> As far as I can see, that means we either have to eliminate pattern
> match failure, the error function, heap overflow, stack overflow
> and infinite loops or we have to add exception handling in some form.
Well, eliminating pattern match failure would not be a bad idea.
I think it's better to require programmers to put explicit calls to `error'
if that's what they want.
Regarding infinite loops, and the use of the `error' function, in the
long term future I hope we see systems that have much better support
for the use of formal methods, so that system and the program could
between them provide proofs of termination and proofs that `error' is
never called. Much work has already been done in this general area,
including some by some of my colleagues [1], but there is still much to
be done -- making this practical is still very much a research issue.
Regarding resource exhaustion such as heap overflow, stack overflow,
and (for hard real-time programs) timeouts, yes, you do need to provide
a way of handling these, and these are going be have to be nondeterministic,
at least from the program's point of view (that is, at the level of the
denotational semantics rather than the operational semantics).
But that doesn't necessarily mean that you should use the same
approach for other kinds of exceptions -- as noted in other messages
in this thread, resource failures are different to other kinds of exceptions.
I suppose that overall, the disadvantages of nondeterminstic exceptions
(compared to the status quo) for program portability and reliability
is likely to be significantly outweighed by the advantage in expressiveness,
and the consequently increased robustness that they provide.
I was a bit shocked when first I realized that the nondeterminism could affect
termination so easily, but on reflection I guess that in the big picture
this is likely to be a rare event and so even nondeterministic exceptions
are likely to be a significant win overall.
However, for reliability and portability, if Haskell does end up
adopting nondeterministic exceptions, I'd like to see a requirement
that implementations offer an option which would inhibit any
optimizations that might affect which exceptions were thrown.
The interface would remain the same (using NDSet and/or the IO monad),
so the effect of this option would just that the operational semantics
would be more tightly specificied.
[1] Termination analysis for Mercury.
Chris Speirs, Zoltan Somogyi and Harald Sondergaard.
Technical Report 97/9, Department of Computer Science, University
of Melbourne, Melbourne, Australia, July 1997, 25 pages.
Available via <http://www.cs.mu.oz.au/mercury/papers.html>.
This paper presents the algorithms of the Mercury termination
analyser, discusses how real-world aspects of the language such as
modules, higher-order features, foreign language code, and
declarative input/output can be handled, and evaluates the
performance of the analyser both on a set of standard test
programs and on the Mercury compiler itself.
A shorter version of this paper was published in the
Proceedings of the Fourth International Static Analysis Symposium,
Paris, France, September 1997.
--
Fergus Henderson <[EMAIL PROTECTED]> | "I have always known that the pursuit
WWW: <http://www.cs.mu.oz.au/~fjh> | of excellence is a lethal habit"
PGP: finger [EMAIL PROTECTED] | -- the last words of T. S. Garp.
