Marshall wrote: > > Yes, an important question (IMHO the *more* important question > than the terminology) is what *programs* do we give up if we > wish to use static typing? I have never been able to pin this > one down at all.
It would depend on the type system, naturally. It isn't clear to me which programs we would have to give up, either. I don't have much experience in sophisticated typed languages. It is rather easy to find programs that baffle an unsophisticated typed language (C, C++, Java, etc.). Looking back in comp.lang.lisp, I see these examples: (defun noisy-apply (f arglist) (format t "I am now about to apply ~s to ~s" f arglist) (apply f arglist)) (defun blackhole (argument) (declare (ignore argument)) #'blackhole) But wait a sec. It seems that these were examples I invented in response to the same question from you! > > The real question is, are there some programs that we > can't write *at all* in a statically typed language, because > they'll *never* be typable? Certainly! As soon as you can reflect on the type system you can construct programs that type-check iff they fail to type-check. > > Perhaps, there is no such beast. Or, perhaps I just can't formulate > > it. 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. > > The C++ type system is Turing complete, although in practical terms > it limits how much processing power it will spend on types at > compile time. I think templates only have to expand to seven levels, so you are severely limited here. > > If you allow Turing Complete type systems, then I would say no--every > > bug can be reforumlated as a type error. If you require your type > > system to be less powerful, then some bugs must escape it. > > I don't think so. Even with a Turing complete type system, a program's > runtime behavior is still something different from its static behavior. > (This is the other side of the "types are not tags" issue--not only > is it the case that there are things static types can do that tags > can't, it is also the case that there are things tags can do that > static types can't.) I agree. The point of static checking is to *not* run the program. If the type system gets too complicated, it may be a de-facto interpreter. -- http://mail.python.org/mailman/listinfo/python-list
