In comp.lang.functional Anton van Straaten <[EMAIL PROTECTED]> 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. > Let me add another complex subtlety, then: the above description misses > an important point, which is that *automated* type checking is not the > whole story. I.e. that compile time/runtime distinction is a kind of > red herring. I agree. I think that instead of "statically typed" we should say "typed" and instead of "(dynamically|latently) typed" we should say "untyped". > In a statically-checked language, people tend to confuse automated > static checking with the existence of types, because they're thinking in > a strictly formal sense: they're restricting their world view to what > they see "within" the language. That is not unreasonable. You see, you can't have types unless you have a type system. Types without a type system are like answers without questions - it just doesn't make any sense. > Then they look at programs in a dynamically-checked language, and see > checks happening at runtime, and they assume that this means that the > program is "untyped". Not in my experience. Either a *language* specifies a type system or not. There is little room for confusion. Well, at least unless you equate "typing" with being "well-defined" or "safe" and go to great lengths to convince yourself that your program has "latent types" even without specifying a type system. > It's certainly close enough to say that the *language* is untyped. Indeed. Either a language has a type system and is typed or has no type system and is untyped. I see very little room for confusion here. In my experience, the people who confuse these things are people from the dynamic/latent camp who wish to see types everywhere because they confuse typing with safety or having well-defined semantics. > But a program as seen by the programmer has types: the programmer > performs (static) type inference when reasoning about the program, and > debugs those inferences when debugging the program, finally ending up > with a program which has a perfectly good type scheme. It's may be > messy compared to say an HM type scheme, and it's usually not proved to > be perfect, but that again is an orthogonal issue. There is a huge hole in your argument above. Types really do not make sense without a type system. To claim that a program has a type scheme, you must first specify the type system. Otherwise it just doesn't make any sense. > Mathematicians operated for thousands of years without automated > checking of proofs, so you can't argue that because a > dynamically-checked program hasn't had its type scheme proved correct, > that it somehow doesn't have types. That would be a bit like arguing > that we didn't have Math until automated theorem provers came along. No - not at all. First of all, mathematics has matured quite a bit since the early days. I'm sure you've heard of the axiomatic method. However, what you are missing is that to prove that your program has types, you first need to specify a type system. Similarly, to prove something in math you start by specifying [fill in the rest]. > 1. "Untyped" is really quite a misleading term, unless you're talking > about something like the untyped lambda calculus. That, I will agree, > can reasonably be called untyped. Untyped is not misleading. "Typed" is not a synonym for "safe" or "having well-defined semantics". > So, will y'all just switch from using "dynamically typed" to "latently > typed" I won't (use "latently typed"). At least not without further qualification. -Vesa Karvonen -- http://mail.python.org/mailman/listinfo/python-list