Chris Smith wrote: > What makes static type systems interesting is not the fact that these > logical processes of reasoning exist; it is the fact that they are > formalized with definite axioms and rules of inference, performed > entirely on the program before execution, and designed to be entirely > evaluatable in finite time bounds according to some procedure or set of > rules, so that a type system may be checked and the same conclusion > reached regardless of who (or what) is doing the checking. All that, > and they still reach interesting conclusions about programs.
There's only one issue mentioned there that needs to be negotiated w.r.t. latent types: the requirement that they are "performed entirely on the program before execution". More below. > If > informal reasoning about types doesn't meet these criteria (and it > doesn't), then it simply doesn't make sense to call it a type system > (I'm using the static terminology here). It may make sense to discuss > some of the ways that programmer reasoning resembles types, if indeed > there are resemblances beyond just that they use the same basic rules of > logic. It may even make sense to try to identify a subset of programmer > reasoning that even more resembles... or perhaps even is... a type > system. It still doesn't make sense to call programmer reasoning in > general a type system. I'm not trying to call programmer reasoning in general a type system. I'd certainly agree that a programmer muddling his way through the development of a program, perhaps using a debugger to find all his problems empirically, may not be reasoning about anything that's sufficiently close to types to call them that. But "latent" means what it implies: someone who is more aware of types can do better at developing the latent types. As a starting point, let's assume we're dealing with a disciplined programmer who (following the instructions found in books such as the one at htdp.org) reasons about types, writes them in his comments, and perhaps includes assertions (or contracts in the sense of "Contracts for Higher Order Functions[1]), to help check his types at runtime (and I'm talking about real type-checking, not just tag checking). When such a programmer writes a type signature as a comment associated with a function definition, in many cases he's making a claim that's provable in principle about the inputs and outputs of that function. For example, if the type in question is "int -> int", then the provable claim is that given an int, the function cannot return anything other than an int. Voila, assuming we can actually prove our claim, then we've satisfied the requirement in Pierce's definition of type system, i.e. "proving the absence of certain program behaviors by classifying phrases according to the kinds of values they compute." The fact that the proof in question may not be automatically verified is no more relevant than the fact that so many proofs in mathematics have not been automatically verified. Besides, if the proof turns out to be wrong, we at least have an automated mechanism for finding witnesses to the error: runtime tag checks will generate an error. Such detection is not guaranteed, but again, "proof" does not imply "automation". What I've just described walks like a type and talks like a type, or at least it appears to do so according to Pierce's definition. We can classify many terms in a given dynamically-typed program on this basis (although some languages may be better at supporting this than others). So, on what grounds do you reject this as not being an example of a type, or at the very least, something which has clear and obvious connections to formal types, as opposed to simply being arbitrary programmer reasoning? Is it the lack of a formalized type system, perhaps? I assume you recognize that it's not difficult to define such a system. Regarding errors, we haven't proved that the function in question can never be called with something other than an int, but we haven't claimed to prove that, so there's no problem there. I've already described how errors in our proofs can be detected. Another possible objection is that I'm talking about local cases, and not making any claims about extending it to an entire program (other than to observe that it can be done). But let's take this a step at a time: considered in isolation, if we can assign types to terms at the local level in a program, do you agree that these are really types, in the type theory sense? If you were to agree, then we could move on to looking at what it means to have many local situations in which we have fairly well-defined types, which may all be defined within a common type system. As an initial next step, we could simply rely on the good old universal type everywhere else in the program - it ought to be possible to make the program well-typed in that case, it would just mean that the provable properties would be nowhere near as pervasive as with a traditional statically-typed program. But the point is we would now have put our types into a formal context. > In the same post here, you simultaneously suppose that there's something > inherently informal about the type reasoning in dynamic languages; and > then talk about the type system "in the static sense" of a dynamic > language. How is this possibly consistent? The point about inherent informality is just that if you fully formalize a static type system for a dynamic language, such that entire programs can be statically typed, you're likely to end up with a static type system with the same disadvantages that the dynamic language was trying to avoid. However, that doesn't preclude type system being defined which can be used to reason locally about dynamic programs. Some people actually do this, albeit informally. >>So we actually have quite a bit of evidence about the presence of static >>types in dynamically-typed programs. > > > No. What we have is quite a bit of evidence about properties remaining > true in dynamically typed programs, which could have been verified by > static typing. Using my example above, at least some of those properties would have been verified by manual static typing. So those properties, at least, seem to be types, at least w.r.t. the local fragment they're proved within. >>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. > > > I agree with that statement. However, I think the conversation > regarding static typing is also over when you decide that the answer is > to weaken static typing until the word applies to informal reasoning. > If the goal isn't to reach a formal understanding, then the word "static > type" shouldn't be used Well, I'm trying to use the term "latent type", as a way to avoid the ambiguity of "type" alone, to distinguish it from "static type", and to get away from the obvious problems with "dynamic type". But I'm much less interested in the term itself than in the issues surrounding dealing with "real" types in dynamically-checked programs - if someone had a better term, I'd be all in favor of it. > and when that is the goal, it still shouldn't > be applied to process that aren't formalized until they manage to become > formalized. This comes back to the phrase I highlighted at the beginning of this message: "performed entirely on the program before execution". Formalizing local reasoning about types is pretty trivial, in many cases. It's just that there are other cases where that's less straightforward. So when well-typed program fragments are considered as part of a larger untyped program, you're suggesting that this so radically changes the picture, that we can no longer distinguish the types we identified as being anything beyond programmer reasoning in general? All the hard work we did figuring out the types, writing them down, writing assertions for them, and testing the program to look for violations evaporates into the epistemological black hole that exists outside the boundaries of formal type theory? > Hopefully, this isn't perceived as too picky. I've already conceded > that we can use "type" in a way that's incompatible with all existing > research literature. Not *all* research literature. There's literature on various notions of dynamic type. > I would, however, like to retain some word with > actually has that meaning. Otherwise, we are just going to be > linguistically prevented from discussing it. For now, you're probably stuck with "static type". But I think it was never likely to be the case that type theory would succeed in absconding with the only technically valid use of the English word "type". Although not for want of trying! Besides, I think it's worth considering why Bertrand Russell used the term "types" in the first place. His work had deliberate connections to the real world. Type theory in computer science unavoidably has similar connections. You could switch to calling it Zoltar Theory, and you'd still have to deal with the fact that a zoltar would have numerous connections to the English word "type". In CS, we don't have the luxury of using the classic mathematician's excuse when confronted with inconvenient philosophical issues, of claiming that type theory is just a formal symbolic game, with no meaning outside the formalism. Anton [1] http://people.cs.uchicago.edu/~robby/pubs/papers/ho-contracts-techreport.pdf -- http://mail.python.org/mailman/listinfo/python-list
