I thought about this in the context of reading Anton's latest post to me, but I'm just throwing out an idea. It's certainly too fuzzy in my mind at the moment to consider it in any way developed. I'm sure it's just as problematic, if not more so, as any existing accounts of dynamic types. Here it is, anyway, just because it's a different way of seeing things.
(I'll first point out here, because it's about to become significant, that contrary to what's been said several times, static type systems assign types to expressions rather than variables.) First of all, it's been pointed out several times that static typing assumes a static program, and that it becomes difficult to describe if the program itself is being modified as it is evaluated. The interesting thing that occurred to me earlier today is that for languages that are reducible to the lambda calculus at least, ALL programs are from some perspective self-modifying. Specifically, no single expression is ever evaluated more than once. When a statement is evaluated several times, that simply means that there is actually a more complex statement that, when it is evaluated, writes a new statement, which consists of a copy of itself, plus something else. Thus it makes little sense, from that perspective, to worry about the possibility that an expression might have a different type each time it's evaluated, and therefore violate static typing. It is never evaluated more than once. What if I were to describe a dynamically typed system as one in which expressions have types just as they do in a static type system, but in which programs are seen as self-modifying? Rather than limiting forms of recursion for well-typed programs to, say, the standard fixed-point operator and then assigning some special-purpose rule for it, we simply admit that the program is being modified as it is run. Type inference (and therefore checking) would need to be performed incrementally. When they do, the results of evaluating everything up to this point will have changed the type environment, providing more information than was previously known. The type environment for assigning types to an expression could still be treated statically at the time that the expression first comes into existence; but it would be different then from what it was at the beginning of the program. Of course, this is only a formal description of the meaning, and not a description of any kind of a reasonable implementation. However, this initially appears, on the surface, to take us some distance toward unifying dynamic types and static types. At least two interesting correlations just sort of "fall out". First, Marshall has observed (and I agree) that static and dynamic types form not different ways of looking at verifying correctness, but rather different forms of programming in the first place. It appears to be encouraging, then, that this perspective classifies static and dynamic types based on how we define the program rather than how we define the type checking. Second, type theory is sometimes concerned with the distinction between structural and nominal types and various hybrids. We've concerned ourself a good bit in this thread with exactly what kinds of "tags" or other runtime type notations are acceptable for defining a dynamically typed language. In this view, Smalltalk (or some simplification thereof wherein doesNotUnderstand is considered an error handling mechanism rather than a first-class part of the language semantics) would represent the dynamic version of structural types, whereas type "tagging" systems with a user-declared finite set of type tags would be the dynamic equivalent to nominal types. Just like in type theory, dynamic type systems can also have hybrids between structural and nominal types. Obviously, that has a lot of problems... some of the same ones that I've been complaining about. However, it has some interesting characteristics as well. If an expression is assumed to be different each time it is encountered, then type the type of "one" expression is easy to evaluate in the initial environment in which it occurs (for some well-defined order of evaluation). Now, to Anton's response, with admittedly rather liberal skimming (sorry!) to avoid my staying up all night thinking about this. Anton wrote: > It's obviously going to be difficult to formally pin down something that > is fundamentally informal. It's fundamentally informal because if > reasoning about the static properties of terms in DT languages were > formalized, it would essentially be something like a formal type system. We may be talking past each other, then, but I'm not particularly interested in the informal aspects of what makes up a type. I agree that formalizing the notion appears quite difficult, especially if my conjecture above were to become part of it. > However, there are some pretty concrete things we can look at. One of > them, which as I've mentioned elsewhere is part of what led me to my > position, is to look at what a soft type inferencer does. It takes a > program in a dynamically typed language, and infers a static type scheme > for it (obviously, it also defines an appropriate type system for the > language.) This has been done in both Scheme and Erlang, for example. > How do you account for such a feat in the absence of something like > latent types? There are undoubtedly any number of typing relations and systems of rules which can be assigned to any program in a dynamically typed language. I think the more interesting question is how these type inference systems choose between the limitless possibilities in a way that tends to be acceptable. I suspect that they do it by assuming certain kinds of type systems, and then finding them. I doubt they are going to find a type system in some language until the basics of that system have been fed to the software as something to look for. I'd be delighted to discover that I'm wrong. If nothing else, it would mean that applying these programs to significant amounts of Scheme and Erlang software would become an invaluable tool for doing research in type theory. > > Undoubtedly, some programmers sometimes perform reasoning about their > > programs which could also be performed by a static type system. > > I think that's a severe understatement. Yes, I agree. I did not intend the connotations that ended up there. In fact, I'd say that something like 90% (and yes, I just grabbed that number out of thin air) of reasoning performed by programmers about their programs could be performed by a static type system. > BTW, I notice you didn't answer any of the significant questions which I > posed to Vesa. So let me pose one directly to you: how should I rewrite > the first sentence in the preceding paragraph to avoid appealing to an > admittedly informal notion of type? I'll try to answer your question. My answer is that I wouldn't try. I would, instead, merely point out that the notion of type is informal, and that it is not necessarily even meaningful. The two possibilities that concern me are that either reasoning with types in this informal sense is just a word, which gets arbitrarily applied to some things but not others such that distinctions are made that have no real value, and that any sufficient definition of type-based reasoning is going to be broad enough to cover most reasoning that programmers ever do, once we start applying enough rigor to try to distinguish between what counts as a type and what doesn't. The fact that programmers think about types is not disputed; my concern is that the types we think about may not meaningfully exist. > Note, also, that I'm using the word > in the sense of static properties, not in the sense of tagged values. In the static sense of types, as I just wrote to Chris Uppal, I can then definitively assert at least the second of the two possibilities above. Every possible property of program execution is a type once the problem of how to statically check it has been solved. > For now, I'll stand on what I've written above. When I see if or how > that doesn't convince you, I can go further. To be clear, I am certainly convinced that people talk and think about types and also about other things regarding their programs which they do not call types. I am concerned only with how accurate it is to make that distinction, on something other than psychological grounds. If we are addressing different problems, then so be it. If however, you believe there is a type/non-type distinction that can be built on some logical foundation, then I'd love to hash it out. > > It is, nevertheless, quite appropriate to call the language "untyped" if > > I am considering static type systems. > > I agree that in the narrow context of considering to what extent a > dynamically typed language has a formal static type system, you can call > it untyped. OK. > However, what that essentially says is that formal type > theory doesn't have the tools to deal with that language, and you can't > go much further than that. As long as that's what you mean by untyped, > I'm OK with it. I can see that in a sense... yes, if a specific program has certain properties, then it may be possible to extend the proof-generator (i.e., the type checker) to be able to prove those properties. However, I remain inconvinced that the same is true of the LANGUAGE. Comments in this thread indicate to me that even if I could write a type-checker that checks correctness in a general-purpose programming language, and that language was Scheme, there would be Scheme programmers who would prefer not to use my Scheme+Types language because it would pester them until they got everything perfect before they could run their code, and Scheme would remain a separate dynamically typed (i.e., from a type theory perspective, untyped) language despite my having achieved all of the wildest dreams of the field of type theory. In that sense, I don't consider this a limitation of type theory. (Two notes: first, I don't actually believe that this is possible, since the descriptions people would give for "correct" are nowhere near so formal as the type theory that would try to check them; and second, I am not so sure that I'd want to use this new language either, for anything except applications in which bugs are truly life-threatening.) > Think of it like this: the more ambitious a language's type system is, > the fewer uncaptured static properties remain in the code of programs in > that language. However, there are plenty of languages with rather weak > static type systems. In those cases, code has more static properties > that aren't captured by the type system. Yes, I agree with this. > I'm pointing out that in many > of these cases, those properties resemble types, to the point that it > can make sense to think of them and reason about them as such, applying > the same sort of reasoning that an automated type inferencer applies. It often makes sense to apply the same sort of reasoning as would be involved in static type inference. I also agree that there are properties called types, which are frequently the same properties caught by commonly occurring type systems, and which enough developers already think of under the word "type" to make it worth trying to change that EXCEPT when there is an explicit discussion going on that touches on type theory. In that latter case, though, we need to be very careful about defining some group of things as not-types across the scope of all possible type systems. There are no such things a priori, and even when you take into account the common requirement that a type system is tractable, the set of things that are not-type because it's provably impossible to check them in polynomial time is smaller than the intuitive sense of that word. Essentially, this use of "type" becomes problematic when it is used to draw conclusions about the scope, nature, purpose, etc. of static types. This answers a good number of the following concerns. > > 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. > > A complete formal definition of what I'm talking about may be impossible > in principle, because if you could completely formally define it, you'd > have a static type system. That may not actually be the case. Lots of things may be formally defined that would nevertheless be different from a static type system. For example, if someone did provide a rigorous definition of some category of type errors that could be recognized by some defined process as such, then the set of language features that detect and react to these errors could be defined as a type system. Chris Uppal just posted such a thing in a different part of this thread, and I'm unsure at this point whether it works or not. The problem with earlier attempts to define type errors in this thread is that they either tend to include all possible errors, or are distinguished by some nebulously defined condition such as being commonly thought of in some way by some set of human beings. > If that makes you throw up your hands, then all you're saying is that > you're unwilling to deal with a very real phenomenon that has obvious > connections to type theory, examples of which I've given above. That's > your choice, but at the same time, you have to give up exclusive claim > to any variation of the word "type". I really think it's been a while since I claimed any such thing... and even at the beginning, I only meant to challenge that use of type in comparing static and dynamic type systems. I am not so sure, though, about these obvious connections to type theory. Those connections may be, for example, some combination of the following rather uninteresting phenomena: 1. Type theory got the word "type" from somewhere a century ago, and the word has continued to be used in its original sense as well, and it just happens that despite the divergence of these uses, there remains some common ground between the two different meanings. or, 2. Many programmers approach type theory from the perspective of having some intuitive definition of a type in mind, and they tend to mix it in with a few of the ideas of type theory in their minds, and then go off and use the word in other contexts. > Terms are used in a context, and it's perfectly reasonable to call > something a "latent type" or even a "dynamic type" in a certain context > and point out connections between those terms and their cousins (or if > you insist, their completely unrelated namesakes) static types. Yes, I agree. I'm yet to be convinced that they are completely unrelated namesakes. I am actually trying to reconstruct such a thing. The problem is that, knowing how "type" is used in the static sense, I am forced to reject attempts that share only basic superficial similarities and yet miss the main point. > > 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. > > The definition of static type system is not in question. However, > realistically, as I pointed out above, you have to acknowledge that type > systems exist in, and are inextricably connected to, a larger, less > formal context. No, but it certainly seems that the reason behind calling them a "type system" is being placed very much in doubt. Simply saying static type system is horribly wrong, and I do it only to avoid inventing words wholesale... but I greatly regret the implication that it means "a type system, which happens to be static." In some senses, this is akin to describing a boat as "a floating platform". That may be somewhat accurate as a rough definition for someone who is familiar with platforms but not with boats. It's a terrible failure, though, in that it implies that being a platform is the important bit; where actually the important bit is that it floats! In fact, it may turn out that boats have very little to do with common platforms... for example, while some boats (barges) have many of the same properties that platforms do, there are whole other classes of boats, which are considerably more powerful than barges, that end up looking very little like a platform at all. If you press hard enough, I can be forced to admit that there is some kind of connection between platforms and floating platforms, because after all one has to stand on something while using a boat, right? Well, the important part of the phrase "static type" isn't "type" but "static." Without even having to undertake the dead-end task of deciding who's got the right to the word "type", let's assume that I should really be saying some other word, like boat. However, that word doesn't really exist, so I am stuck with "static type". I just have to be very careful about explaining that what I mean by type is completely different from what others mean by type. There is some overlap, which potentially arises from one of the uninteresting sources I've listed above, or maybe... just maybe... arises from some actual similarity that we haven't identified yet. But we still haven't identified it. This is very much the situation I see ourselves in. I very much want to agree with everyone's right to use the word "type", but then people keep saying things that seem to me to be clear misunderstandings that the important part is the "static", not the "type". When qualification is not needed Fundamentally, the important aspect of types, in the static sense, is that they are used in a formal, syntactic, tractable method for proving the absence of program behaviors. Even if it turns out that, in practice, all type systems contain mechanisms for solving a certain rigorously definable class of problems, that will not be part of the definition of types, when the word is used in the static sense. So we can search for a more formal similarity, or we can agree that it's incidentally true that they sometimes solve the same problems but also agree that it's pointless and misleading to ever talk about a "type system" without clarifying the usage either explicitly or by context. It remains incorrect to relax the degree of formality and talk about static types in an intuitive and undefinable way, because than they lose the entire property of being types at all. At that point, it's best to drop "static", which is not true anyway, and switch over to the other set of terminology where it makes sense to call them types. > There's a sense in which one can say that yes, the informal types I'm > referring to have an interesting degree of overlap with static types; > and also that static types do, loosely speaking, have the "purpose" of > formalizing the informal properties I'm talking about. Static types have the property of proving ANY properties of a program that may be proven. Certainly, research is pragmatically restricted to specific problems that are (1) useful and (2) solvable. Aside from that, I can't imagine any competent language designer building a type system, but rejecting some useful and solvable feature for the sole reason that he or she doesn't think of it as solving a type error. > But I hardly see why such an informal characterization should bother > you. It doesn't affect the definition of static type. I hope I've explained how it does affect the definition of a static type. > This is based on the assumption that all we're talking about is > "well-defined semantics". Indeed. My statement there will not apply if we find some formal definition of a dynamic type system that doesn't reduce to well-defined semantics once you remove the intuitive bits from it. -- Chris Smith - Lead Software Developer / Technical Trainer MindIQ Corporation -- http://mail.python.org/mailman/listinfo/python-list