Vesa Karvonen wrote: > 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.
I reject this comparison. There's much more to it than that. 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. This isn't an attempt to jump on any bandwagons, it's an attempt to characterize what is actually happening in real programs and with real programmers. I'm relating that activity to type systems because that is what it most closely relates to. Usually, formal type theory ignores such things, because of course what's in the programmer's head is outside the domain of the formal definition of an untyped language. But all that means is that formal type theory can't account for the entirety of what's happening in the case of programs in untyped languages. Unless you can provide some alternate theory of the subject that's better than what I'm offering, it's not sufficient to complain "but that goes beyond (static/syntactic) type theory". Yes, it goes beyond traditional type theory, because it's addressing with something which traditional type theory doesn't address. 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. > I agree. I think that instead of "statically typed" we should say > "typed" and instead of "(dynamically|latently) typed" we should say > "untyped". The problem with "untyped" is that there are obvious differences in typing behavior between the untyped lambda calculus and, say, a language like Scheme (and many others). Like all latently-typed languages, Scheme includes, in the language, mechanisms to tag values in a way that supports checks which help the programmer to ensure that the program's behavior matches the latent type scheme that the programmer has in mind. See my other recent reply to Marshall for a more detailed explanation of what I mean. 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). Let me come at this from another direction: what do you call the classifications into number, string, vector etc. that a language like Scheme does? And when someone writes a program which includes the following lines, how would you characterize the contents of the comment: ; third : integer -> integer (define (third n) (quotient n 3)) In my experience, answering these questions without using the word "type" results in a lot of silliness. And if you do use "type", then you're going to have to adjust the rest of your position significantly. >>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. 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. But as to your point, latently typed languages have informal type systems. Show me a latently typed language or program, and I can tell you a lot about its type system or type scheme. Soft type inferencers demonstrate this by actually defining a type system and inferring type schemes for programs. That's a challenging thing for an automated tool to do, but programmers routinely perform the same sort of activity on an informal basis. >>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. Again, the type system is informal. What you're essentially saying is that only things that are formally defined make sense. But you can't wish dynamically-checked languages out of existence. So again, how would you characterize these issues in dynamically-checked languages? Saying that it's just a matter of well-defined semantics doesn't do anything to address the details of what's going on. I'm asking for a more specific account than that. >>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]. I agree, to make the comparison perfect, you'd need to define a type system. But that's been done in various cases. So is your complaint simply that most programmers are working with informal type systems? I've already stipulated that. However, I think that you want to suggest that those programmers are not working with type systems at all. This reminds me of a comedy skit which parodied the transparency of Superman's secret identity: Clark Kent is standing in front of Lois Lane and removes his glasses for some reason. Lois looks confused and says "where did Clark go?" Clark quickly puts his glasses back on, and Lois breathes a sigh of relief, "Oh, there you are, Clark". The problem we're dealing with in this case is that anything that's not formally defined is essentially claimed to not exist. It's lucky that this isn't really the case, otherwise much of the world around us would vanish in a puff of formalist skepticism. We're discussing systems that operate on an informal basis: in this case, the reasoning about the classification of values which flow through terms in a dynamically-checked language. If you can produce a useful formal model of those systems that doesn't omit significant information, that's great, and I'm all ears. However, claiming that e.g. using a universal type is a complete model what's happening misses the point: it doesn't account at all for the reasoning process I've just described. >>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". Again, your two suggested replacements don't come close to capturing what I'm talking about. Without better alternatives, "type" is the closest appropriate term. I'm qualifying it with the term "latent", precisely to indicate that I'm not talking about formally-defined types. I'm open to alternative terminology or ways of characterizing this, but they need to address issues that exist outside the boundaries of formal type systems, so simply applying terms from formal type theory is not usually sufficient. >>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. This and my other recent post give a fair amount of qualification, so let me know if you need anything else to be convinced. :) But to be fair, I'll start using "untyped" if you can come up with a satisfactory answer to the two questions I asked above, just before I used the word "silliness". Anton -- http://mail.python.org/mailman/listinfo/python-list