Termination and type systems

[Dirk Thierbach]

David Hopwood <david.nospam.hopwood at blueyonder.co.uk> 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