Marshall wrote: > David Hopwood wrote: > >>A type system that required an annotation on all subprograms that do not >>provably terminate, OTOH, would not impact expressiveness at all, and would >>be very useful. > > Interesting. I have always imagined doing this by allowing an > annotation on all subprograms that *do* provably terminate. If > you go the other way, you have to annotate every function that > uses general recursion (or iteration if you swing that way) and that > seems like it might be burdensome.
Not at all. Almost all subprograms provably terminate (with a fairly easy proof), even if they use general recursion or iteration. If it were not the case that almost all functions provably terminate, then the whole idea would be hopeless. If a subprogram F calls G, then in order to prove that F terminates, we probably have to prove that G terminates. Consider a program where only half of all subprograms are annotated as provably terminating. In that case, we would be faced with very many cases where the proof cannot be discharged, because an annotated subprogram calls an unannotated one. If, on the other hand, more than, say, 95% of subprograms provably terminate, then it is much more likely that we (or the inference mechanism) can easily discharge any particular proof involving more than one subprogram. So provably terminating should be the default, and other cases should be annotated. In some languages, annotations may never or almost never be needed, because they are implied by other characteristics. For example, the concurrency model used in the language E (www.erights.org) is such that there are implicit top-level event loops which do not terminate as long as the associated "vat" exists, but handling a message is always required to terminate. > Further, it imposes the > annotation requirement even where the programer might not > care about it, which the reverse does not do. If the annotation marks not-provably-terminating subprograms, then it calls attention to those subprograms. This is what we want, since it is less safe/correct to use a nonterminating subprogram than a terminating one (in some contexts). There could perhaps be a case for distinguishing annotations for "intended not to terminate", and "intended to terminate, but we couldn't prove it". I do not know how well such a type system would work in practice; it may be that typical programs would involve too many non-trivial proofs. This is something that would have to be tried out in a research language. -- David Hopwood <[EMAIL PROTECTED]> -- http://mail.python.org/mailman/listinfo/python-list
