Anton van Straaten <[EMAIL PROTECTED]> wrote: > The problem is that there are no useful sound definitions for the type > systems (in the static sense) of dynamically-typed languages. Yet, we > work with type-like static properties in those languages all the time, > as I've been describing.
I honestly don't find it very compelling that there are similarities between the kinds of reasoning that goes on in static type systems versus those used by programmers in dynamically typed languages. Rather, of course there are similarities. It would be shocking if there were not similarities. These similarities, though, have nothing to with the core nature of types. Basically, there are ways to reason about programs being correct. Static type systems describe their reasoning (which is always axiomatic in nature) by assigning "types" to expressions. Programmers in dynamically typed languages still care about the correctness of their programs, though, and they find ways to reason about their programs as well. That reasoning is not completely axiomatic, but we spend an entire lifetime applying this basic logical system, and it makes sense that programmers would try to reason from premises to conclusions in ways similar to a type system. Sometimes they may even ape other type systems with which they are familiar; but even a programmer who has never worked in a typed language would apply the same kind of logic as is used by type systems, because it's a form of logic with which basically all human beings are familiar and have practiced since the age of three (disclaimer: I am not a child psychologist). On the other hand, programmers don't restrict themselves to that kind of pure axiomatic logic (regardless of whether the language they are working in is typed). The also reason inductively -- in the informal sense -- and are satisfied with the resulting high probabilities. They generally apply intuitions about a problem statement that is almost surely not written clearly enough to be understood by a machine. And so forth. What makes static type systems interesting is not the fact that these logical processes of reasoning exist; it is the fact that they are formalized with definite axioms and rules of inference, performed entirely on the program before execution, and designed to be entirely evaluatable in finite time bounds according to some procedure or set of rules, so that a type system may be checked and the same conclusion reached regardless of who (or what) is doing the checking. All that, and they still reach interesting conclusions about programs. If informal reasoning about types doesn't meet these criteria (and it doesn't), then it simply doesn't make sense to call it a type system (I'm using the static terminology here). It may make sense to discuss some of the ways that programmer reasoning resembles types, if indeed there are resemblances beyond just that they use the same basic rules of logic. It may even make sense to try to identify a subset of programmer reasoning that even more resembles... or perhaps even is... a type system. It still doesn't make sense to call programmer reasoning in general a type system. In the same post here, you simultaneously suppose that there's something inherently informal about the type reasoning in dynamic languages; and then talk about the type system "in the static sense" of a dynamic language. How is this possibly consistent? > We know that we can easily take dynamically-typed program fragments and > assign them type schemes, and we can make sure that the type schemes > that we use in all our program fragments use the same type system. Again, it would be surprising if this were not true. If programmers do, in fact, tend to reason correctly about their programs, then one would expect that there are formal proofs that could be found that they are right. That doesn't make their programming in any way like a formal proof. I tend to think that a large number of true statements are provable, and that programmers are good enough to make a large number of statements true. Hence, I'd expect that it would be possible to find a large number of true, provable statements in any code, regardless of language. > So we actually have quite a bit of evidence about the presence of static > types in dynamically-typed programs. No. What we have is quite a bit of evidence about properties remaining true in dynamically typed programs, which could have been verified by static typing. > We're currently discussing something that so far has only been captured > fairly informally. If we restrict ourselves to only what we can say > about it formally, then the conversation was over before it began. I agree with that statement. However, I think the conversation regarding static typing is also over when you decide that the answer is to weaken static typing until the word applies to informal reasoning. If the goal isn't to reach a formal understanding, then the word "static type" shouldn't be used; and when that is the goal, it still shouldn't be applied to process that aren't formalized until they manage to become formalized. Hopefully, this isn't perceived as too picky. I've already conceded that we can use "type" in a way that's incompatible with all existing research literature. I would, however, like to retain some word with actually has that meaning. Otherwise, we are just going to be linguistically prevented from discussing it. -- Chris Smith - Lead Software Developer / Technical Trainer MindIQ Corporation -- http://mail.python.org/mailman/listinfo/python-list
