Chris F Clark <[EMAIL PROTECTED]> 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 -- http://mail.python.org/mailman/listinfo/python-list
