David Hopwood <[EMAIL PROTECTED]> wrote: > 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. Maybe the paper "Linear types and non-size-increasing polynomial time computation" by Martin Hofmann is interesting in this respect. >From the abstract: We propose a linear type system with recursion operators for inductive datatypes which ensures that all definable functions are polynomial time computable. The system improves upon previous such systems in that recursive definitions can be arbitrarily nested; in particular, no predicativity or modality restrictions are made. It does not only ensure termination, but termination in polynomial time, so you can use those types to carry information about this as well. > 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). That would be certainly nice, but it may be almost impossible to do in practice. It's already hard enough to guarantee termination with the extra information present in the type annotation. If this information is not present, then the language has to be probably restricted so severely to ensure termination that it is more or less useless. - Dirk -- http://mail.python.org/mailman/listinfo/python-list
