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

[Matthias Blume]

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

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

Most interactive processes are written in such a way that they
(effectively) consist of an infinitely repeated application of some
function f that maps the current state and the input to the new state
and the output.

   f : state * input -> state * output

This function f itself has to terminate, i.e., if t has to be
guaranteed that after any given input, there will eventually be an
output.  In most interactive systems the requirements are in fact much
stricter: the output should come "soon" after the input has been
received.

I am pretty confident that the f for most (if not all) existing
interactive systems could be coded in a language that enforces
termination.  Only the loop that repeatedly applies f would have to be
coded in a less restrictive language.