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

[David Hopwood]

Matthias Blume wrote:
> 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.  [...]
>>>>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.

This is absolutely consistent with what I said. While f could be coded in
a system that *required* termination, the outer loop could not.

As I mentioned in a follow-up, event loop languages such as E enforce this
program structure, which would almost or entirely eliminate the need for
annotations in a type system that proves termination of some subprograms.

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