> There are two sources of such information: the static context (e.g., in Scheme, which variables are in scope) and the dynamic environment (e.g., again in Sche

> There are two sources of such information: the static context (e.g., in Scheme, which variables are in scope) and the dynamic environment (e.g., again in Scheme, the type of an object, and, in Python, pretty much everything). The static context grows whenever you bind variables in the program text (e.g., when you define a procedure). The dynamic environment grows when the control flow reaches such binders (e.g., when it enters a called procedure). Heh, I intended that as a rhetorical question, but I admit that wasn't clear from my post, and this is a very thorough answer. :) > For example, if you create an empty mutable list object, dynamic analysis can't tell you what its element type is supposed to be, until you actually start inserting elements into it. That's a limitation of most implementations of mutable list objects in dynamically typed languages, but there's nothing preventing a dynamic language from having a mutable list that enforces a single type in a list at runtime starting from the construction of the list. In Python it would not be difficult to implement an `IntegerList` class which enforces that all its elements are integers, for example. Yes, we can't determine at compile time that the following is a type error: a = IntegerList() a.append('Hello, world') But we can report on that at runtime (remember, I'm talking about the quality of type errors, not when they occur). Further, one can imagine a hypothetical dynamic language where we parameterize types, too: a = List<Integer>() a.append('Hello, world') Of course this could be implemented statically, but it could be implemented dynamically, the difference being that the type error would be reported at runtime instead of compile time. The reason, I think, that this isn't done is that once you get to the point where you're putting type parameters like this, you've lost most of the benefits of a dynamic type system, and would gain more from seeing your errors at compile time. > > A type system that gathers lots of type information is equivalent to a strongly-typed language IMHO > This isn't true. C++'s type system gathers a lot of type information, yet C++ isn't “strongly typed” (assuming that term means anything at all) by any stretch of the term. You're right, I can't imagine what brain fart caused me to say what I said there. /shrug > Rather than “strongly-typed”, a more useful term is “sound”. A type system is sound when it actually protects the language's basic abstractions. For example, Standard ML has a sound type system, and there's a formal proof of this fact. Java's type system is actually unsound, but it makes up for this deficiency by inserting runtime checks to turn wrong operations (e.g., invalid downcasts) into runtime exceptions (just like in Python!). C++'s type system is also unsound, and performing wrong operations is simply undefined behavior. "Soundness" is a mathematically defined concept, but a very binary one (it's sound or it isn't). "Strength" is a different concept which admittedly isn't an objective measure. But I think we can agree on it as a subjective measure for comparing some things. For example, I do think there's a real phenomenon described that we can agree on when I say that Python is more strongly-typed than JavaScript, and Java is more strongly-typed than C, and I think you'd agree with me on these comparisons, even though none of these languages are soundly typed. Sound typing corresponds to a very strong type system. :)