David Hopwood wrote: > Joe Marshall wrote: > > > > The point is that there exists (by construction) programs that can > > never be statically checked. > > I don't think you've shown that. I would like to see a more explicit > construction of a dynamically typed [*] program with a given specification, > where it is not possible to write a statically typed program that meets > the same specification using the same algorithms.
I think we're at cross-purposes here. It is trivial to create a static type system that has a `universal type' and defers all the required type narrowing to runtime. In effect, we've `turned off' the static typing (because everything trivially type checks at compile time). However, a sufficiently powerful type system must be incomplete or inconsistent (by Godel). A type system proves theorems about a program. If the type system is rich enough, then there are unprovable, yet true theorems. That is, programs that are type-safe but do not type check. A type system that could reflect on itself is easily powerful enough to qualify. > AFAIK, it is *always* possible to construct such a statically typed > program in a type system that supports typerec or gradual typing. The > informal construction you give above doesn't contradict that, because > it depends on reflecting on a [static] type system, and in a dynamically > typed program there is no type system to reflect on. A static type system is usually used for universal proofs: For all runtime values of such and such... Dynamic checks usually provide existential refutations: This particular value isn't a string. It may be the case that there is no universal proof, yet no existential refutation. > > Note that I'm not claiming that you can check any desirable property of > a program (that would contradict Rice's Theorem), only that you can > express any dynamically typed program in a statically typed language -- > with static checks where possible and dynamic checks where necessary. Sure. And I'm not saying that you cannot express these programs in a static language, but rather that there exist programs that have desirable properties (that run without error and produce the right answer) but that the desirable properties cannot be statically checked. The real question is how common these programs are, and what sort of desirable properties are we trying to check. -- http://mail.python.org/mailman/listinfo/python-list
