What is Expressiveness in a Computer Language

[Chris Smith]

Chris F Clark <cfc at shell01.TheWorld.com> wrote:
> And to me the question is what kinds of types apply to these dynamic
> programs, where in fact you may have to solve the halting problem to
> know exactly when some statement is executed.

Yes, I believe (static) type systems will always end up approximating 
(conservatively) the possible behavior of programs in order to perform 
their verification.

> Or, perhaps we have static type checkers which can do
> computations of unbounded complexity.  However, I thought that one of
> the characteristics of type systems was that they did not allow
> unbounded complexity and weren't Turing Complete.

Honestly, I suspect you'd get disagreement within the field of type 
theory about this.  Certainly, there are plenty of researchers who have 
proposed type systems that potentially don't even terminate.  The 
consensus appears to be that they are worth studying within the field of 
type theory, but I note that Pierce still hasn't dropped the word 
"tractable" from his definition in his introductory text, despite 
acknowledging only a couple pages later that languages exist whose type 
systems are undecidable, and apparently co-authoring a paper on one of 
them.  The consensus seems to be that such systems are interesting if 
they terminate quickly for interesting cases (in which case, I suppose, 
you could hope to eventually be able to formalize what cases are 
interesting, and derive a truly tractable type system that checks that 
interesting subset).

Interestingly, Pierce gives ML as an example of a language whose type 
checker does not necesarily run in polynomial time (thus failing some 
concepts of "tractable") but that does just fine in practice.  I am just 
quoting here, so I don't know exactly how this is true.  Marshall 
mentioned template meta-programming in C++, which is definitely Turing-
complete.

-- 
Chris Smith - Lead Software Developer / Technical Trainer
MindIQ Corporation