Saying "latently-typed language" is making a category mistake

[David Hopwood]

Patricia Shanahan wrote:
> Vesa Karvonen wrote:
> ...
> 
>> An example of a form of informal reasoning that (practically) every
>> programmer does daily is termination analysis.  There are type systems
>> that guarantee termination, but I think that is fair to say that it is
>> not yet understood how to make a practical general purpose language, whose
>> type system would guarantee termination (or at least I'm not aware of
>> such a language).  It should also be clear that termination analysis need
>> not be done informally.  Given a program, it may be possible to formally
>> prove that it terminates.
> 
> To make the halting problem decidable one would have to do one of two
> things: Depend on memory size limits, or have a language that really is
> less expressive, at a very deep level, than any of the languages
> mentioned in the newsgroups header for this message.

I don't think Vesa was talking about trying to solve the halting problem.

A type system that required termination would indeed significantly restrict
language expressiveness -- mainly because many interactive processes are
*intended* not to terminate.

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. Such a type system could work by treating some dependent
type parameters as variants which must strictly decrease in a recursive
call or loop. For example, consider a recursive quicksort implementation.
The type of the 'sort' routine would take an array of length
(dependent type parameter) n. Since it only performs recursive calls to
itself with parameter strictly less than n, it is not difficult to prove
automatically that the quicksort terminates. The programmer would probably
just have to give hints in some cases as to which parameters are to be
treated as variants; the rest can be inferred.

-- 
David Hopwood <david.nospam.hopwood at blueyonder.co.uk>