Andreas Rossberg wrote: > > ... And the reason is that "type" has a > well-established use in theory. It is not just my "assumption", it is > established practice since 80 or so years.
Wouldn't it be fair to say it goes back a least to Principia Mathematica, 1910? > So far, this discussion has > not revealed the existence of any formal work that would provide a > theory of "dynamic types" in the sense it is used to characterise > "dynamically typed" languages. Indeed, the idea I am starting to get is that much of what is going on in the dynamic/latent/untyped/whatever world is simply informal, conceptual-level static analysis. The use of the runtime system is a formal assistant to this informal analysis. In other words, formal existential quantification is used as hint to help do informal universal quantification. Now, given that explanation, the formal analysis looks better. But that's not the whole story. We also have the fact that the informal analysis gets to run on the human brain, while the static analysis has to run on a lousy microprocessor with many orders of magnitude less processing power. We have the fact that the formal static analysis is of limited power. We have the fact that historically, static languages have forbidden the use of the formal existential method preferred by the DT crowd until *after* the static analysis has passed, thus defeating their purpose. And probably still more things that I don't appreciate yet. So I'll now throw around some terms (in an attempt to look smart :-) and say, late binding, impredicativity. Marshal -- http://mail.python.org/mailman/listinfo/python-list