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

[Matthias Blume]

Pascal Costanza <pc at p-cos.net> writes:

> Matthias Blume wrote:
>> Pascal Costanza <pc at p-cos.net> 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.
>>> Not quite. See http://en.wikipedia.org/wiki/ACL2
>> What do you mean "not quite"?  Of course, Patricia is absolutely
>> right.  Termination-guaranteeing languages are fundamentally less
>> expressive than Turing-complete languages.  ACL2 was not mentioned in
>> the newsgroup header.
>
> ACL2 is a subset of Common Lisp, and programs written in ACL2 are
> executable in Common Lisp. comp.lang.lisp is not only about Common
> Lisp, but even if it were, ACL2 would fit.

So what?

Patricia said "less expressive", you said "subset".  Where is the
contradiction?

Perhaps you could also bring up the subset of Common Lisp where the
only legal program has the form:

   nil

Obviously, this is a subset of Common Lisp and, therefore, fits
comp.lang.lisp.  Right?

Yes, if you restrict the language to make it less expressive, you can
guarantee termination.  Some restrictions that fit the bill already
exist.  IMHO, it is still wrong to say that "Lisp guaratees
termination", just because there is a subset of Lisp that does.

Matthias

PS: I'm not sure if this language guarantees termination, though.  :-)