Termination and type systems

[Dirk Thierbach]

David Hopwood <david.nospam.hopwood at blueyonder.co.uk> wrote:
> Dirk Thierbach wrote:

> That's interesting, but linear typing imposes some quite severe
> restrictions on programming style. From the example of 'h' on page 2,
> it's clear that the reason for the linearity restriction is just to
> ensure polynomial-time termination, and is not needed if we only want
> to prove termination.

Yes. It's just an example of what can be actually done with a typesystem.

>> 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.

> I think you're overestimating the difficulty of the problem. The fact
> that *in general* it can be arbitrarily hard to prove termination, can
> obscure the fact that for large parts of a typical program, proving
> termination is usually trivial.

Yes. The problem is the small parts where it's not trivial (and the
size of this part depends on the actual problem the program is trying
to solve). Either you make the language so restrictive that these
parts are hard (see your remark above) or impossible to write, or
you'll be left with a language where the compiler cannot prove
termination of those small parts, so it's not a "type system" in the
usual sense.

Of course one could write an optional tool that automatically proves
termination of the easy parts, and leaves the rest to the programmer,
but again, that's a different thing.

- Dirk