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

[Patricia Shanahan]

Chris Smith wrote:
> Patricia Shanahan <pats at acm.org> 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.
> 
> Patricia, perhaps I'm misunderstanding you here.  To make the halting 
> problem decidable is quite a different thing than to say "given a 
> program, I may be able to prove that it terminates" (so long as you also 
> acknowledge the implicit other possibility: I also may not be able to 
> prove it in any finite bounded amount of time, even if it does 
> terminate!)
> 
> The fact that the halting problem is undecidable is not a sufficient 
> reason to reject the kind of analysis that is performed by programmers 
> to convince themselves that their programs are guaranteed to terminate.  
> Indeed, proofs that algorithms are guaranteed to terminate even in 
> pathological cases are quite common.  Indeed, every assignment of a 
> worst-case time bound to an algorithm is also a proof of termination.
> 
> This is, of course, a very good reason to reject the idea that the 
> static type system for any Turing-complete language could ever perform 
> this same kind analysis.
> 

Of course, we can, and should, prefer programs we can prove terminate.
Languages can make it easier or harder to write provably terminating
programs.

Patricia