Anton van Straaten wrote: > Vesa Karvonen wrote: > > > > This static vs dynamic type thing reminds me of one article written by > > Bjarne Stroustrup where he notes that "Object-Oriented" has become a > > synonym for "good". More precisely, it seems to me that both camps > > (static & dynamic) think that "typed" is a synonym for having > > "well-defined semantics" or being "safe" and therefore feel the need > > to be able to speak of their language as "typed" whether or not it > > makes sense. > > I reject this comparison. There's much more to it than that.
I agree that there's more to it than that. I also agree, however, that Vesa's observation is true, and is a big part of the reason why it's difficult to discuss this topic. I don't recall who said what at this point, but earlier today someone else posted -- in this same thread -- the idea that static type "advocates" want to classify some languages as untyped in order to put them in the same category as assembly language programming. That's something I've never seen, and I think it's far from the goal of pretty much anyone; but clearly, *someone* was concerned about it. I don't know if much can be done to clarify this rhetorical problem, but it does exist. The *other* bit that's been brought up in this thread is that the word "type" is just familiar and comfortable for programmers working in dynamically typed languages, and that they don't want to change their vocabulary. The *third* thing that's brought up is that there is a (to me, somewhat vague) conception going around that the two really ARE varieties of the same thing. I'd like to pin this down more, and I hope we get there, but for the time being I believe that this impression is incorrect. At the very least, I haven't seen a good way to state any kind of common definition that withstands scrutiny. There is always an intuitive word involved somewhere which serves as an escape hatch for the author to retain some ability to make a judgement call, and that of course sabotages the definition. So far, that word has varied through all of "type", "type error", "verify", and perhaps others... but I've never seen anything that allows someone to identify some universal concept of typing (or even the phrase "dynamic typing" in the first place) in a way that doesn't appeal to intuition. > The point > is that the reasoning which programmers perform when working with an > program in a latently-typed language bears many close similiarities to > the purpose and behavior of type systems. Undoubtedly, some programmers sometimes perform reasoning about their programs which could also be performed by a static type system. This is fairly natural, since static type systems specifically perform tractable analyses of programs (Pierce even uses the word "tractable" in the definition of a type system), and human beings are often (though not always) best-served by trying to solve tractable problems as well. > There are reasons to connect > it to type theory, and if you can't see those reasons, you need to be > more explicit about why. Let me pipe up, then, as saying that I can't see those reasons; or at least, if I am indeed seeing the same reasons that everyone else is, then I am unconvinced by them that there's any kind of rigorous connection at all. > I'm suggesting that if a language classifies and tags values in a way > that supports the programmer in static reasoning about the behavior of > terms, that calling it "untyped" does not capture the entire picture, > even if it's technically accurate in a restricted sense (i.e. in the > sense that terms don't have static types that are known within the > language). It is, nevertheless, quite appropriate to call the language "untyped" if I am considering static type systems. I seriously doubt that this usage in any way misleads anyone into assuming the absence of any mental processes on the part of the programmer. I hope you agree. If not, then I think you significantly underestimate a large category of people. > The first point I was making is that *automated* checking has very > little to do with anything, and conflating static types with automated > checking tends to lead to a lot of confusion on both sides of the > static/dynamic fence. I couldn't disagree more. Rather, when you're talking about static types (or just "types" in most research literature that I've seen), then the realm of discussion is specifically defined to be the very set of errors that are automatically caught and flagged by the language translator. I suppose that it is possible to have an unimplemented type system, but it would be unimplemented only because someone hasn't felt the need nor gotten around to it. Being implementABLE is a crucial part of the definition of a static type system. I am beginning to suspect that you're make the converse of the error I made earlier in the thread. That is, you may be saying things regarding the psychological processes of programmers and such that make sense when discussing dynamic types, and in any case I haven't seen any kind of definition of dynamic types that is more acceptable yet; but it's completely irrelevant to static types. Static types are not fuzzy -- if they were fuzzy, they would cease to be static types -- and they are not a phenomenon of psychology. To try to redefine static types in this way not only ignores the very widely accepted basis of entire field of existing literature, but also leads to false ideas such as that there is some specific definable set of problems that type systems are meant to solve. Skipping ahead a bit... > I agree, to make the comparison perfect, you'd need to define a type > system. But that's been done in various cases. I don't think that has been done, in the case of dynamic types. It has been done for static types, but much of what you're saying here is in contradiction to the definition of a type system in that sense of the word. > The problem we're dealing with in this case is that anything that's not > formally defined is essentially claimed to not exist. I see it as quite reasonable when there's an effort by several participants in this thread to either imply or say outright that static type systems and dynamic type systems are variations of something generally called a "type system", and given that static type systems are quite formally defined, that we'd want to see a formal definition for a dynamic type system before accepting the proposition that they are of a kind with each other. So far, all the attempts I've seen to define a dynamic type system seem to reduce to just saying that there is a well- defined semantics for the language. I believe that's unacceptable for several reasons, but the most significant of them is this. It's not reasonable to ask anyone to accept that static type systems gain their essential "type system-ness" from the idea of having well-defined semantics. From the perspective of a statically typed language, this looks like a group of people getting together and deciding that the real "essence" of what it means to be a type system is... and then naming something that's so completely non- essential that we don't generally even mention it in lists of the benefits of static types, because we have already assumed that it's true of all languages except C, C++, and assembly language. -- Chris Smith - Lead Software Developer / Technical Trainer MindIQ Corporation -- http://mail.python.org/mailman/listinfo/python-list
