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

[Marshall]

Chris Uppal wrote:
> Pascal Costanza wrote:
>
> > Sorry, obviously I was far from being clear. ACL2 is not
> > Turing-complete. All iterations must be expressed in terms of
> > well-founded recursion.
>
> How expressive does that end up being for real problems ?   I mean obviously in
> some sense it's crippling, but how much of a restiction would that be for
> non-accademic programming.  Could I write an accountancy package in it, or an
> adventure games, or a webserver, with not too much more difficulty than in a
> similar language without that one aspect to its type system ?
>
> Hmm, come to think of it those all hae endless loops at the outer level, with
> the body of the loop being an event handler, so maybe only the handler should
> be required to guaranteed to terminate.

An example of a non-Turing-complete language (at least the core
language; the standard is getting huge) with guaranteed termination,
that is used everywhere and quite useful, is SQL.

I wouldn't want to write an accounting package in it; its abstraction
facilities are too weak. But the language is much more powerful
than it is usually given credit for.


Marshall