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

[Patricia Shanahan]

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.

A language for which the halting problem is decidable must also be a
language in which it is impossible to simulate an arbitrary Turing
machine (TM). Otherwise, one could decide the notoriously undecidable TM
halting problem by generating a language X program that simulates the TM
and deciding whether the language X program halts.

One way out might be to depend on the boundedness of physical memory. A
language with a fixed maximum memory size cannot simulate an arbitrary
TM. However, the number of states for a program is so great that a
method that depends on its finiteness, but would not work for an
infinite memory model, is unlikely to be practical.

Patricia