Marshall wrote: > Chris F Clark wrote: > >>I'm particularly interested if something unsound (and perhaps >>ambiguous) could be called a type system. I definitely consider such >>things type systems. > > > I don't understand. You are saying you prefer to investigate the > unsound over the sound?
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. If you want to talk about those properties as though they were types, one of the options is what Chris Clark described when he wrote "I reason about my program using types which I can (at least partially) formalize, but for which there is no sound axiomatic system." >>However, I like my definitions very general and >>vague. Your writing suggests the opposite preference. > > > Again, I cannot understand this. In a technical realm, vagueness > is the opposite of understanding. To me, it sounds like you are > saying that you prefer not to understand the field you work in. The issue as I see it is simply that if we're going to work with dynamically-typed programs at all, our choices are limited at present, when it comes to formal models that capture our informal static reasoning about those programs. In statically-typed languages, this reasoning is mostly captured by the type system, but it has no formal description for dynamically-typed languages. >>To me if >>something works in an analogous way to how a known type system, I tend >>to consider it a "type system". That probably isn't going to be at >>all satisfactory to someone wanting a more rigorous definition. > > > Analogies are one thing; definitions are another. A formal definition is problematic, precisely because we're dealing with something that to a large extent is deliberately unformalized. But as Chris Clark pointed out, "these types are locally sound, i.e. I can prove properties that hold for regions of my programs." We don't have to rely entirely on analogies, and this isn't something that's entirely fuzzy. There are ways to relate it to formal type theory. >>Of >>course, to my mind, the rigorous definitions are just an attempt to >>capture something that is already known informally and put it on a >>more rational foundation. > > > If something is informal and non-rational, it cannot be said to > be "known." As much as I love the view down into that abyss, we're nowhere near being in such bad shape. 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. We know that we can assign type schemes to entire dynamically-typed programs, and we can even automate this process, although not without some practical disadvantages. So we actually have quite a bit of evidence about the presence of static types in dynamically-typed programs. Besides, we should be careful not to forget that our formal methods are incredibly weak compared to the power of our intelligence. If that were not the case, there would be no advantage to possessing intelligence, or implementing AIs. We are capable of reasoning outside of fully formal frameworks. The only way in which we are able to develop formal systems is by starting with the informal. 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. Anton -- http://mail.python.org/mailman/listinfo/python-list
