Why type systems are interesting - part III: latent types
The "part II" thread was getting too long, so here beginneth part III. For ease of indexing, the prior two threads are:
This post is a response to Frank's recent post, "I say we shall have no mo' "latent types"..." (here's the same post in context). The first couple of points below are tangential, but after that comes my defense of the syntactic aspect of latent types that I've been discussing.Frank Atanassow wrote:
You are conflating dynamic loading of untyped code with dynamic loading of typed code. They are not the same thing, and untyped languages only support the first, and typed languages can easily accomodate dynamic loading of Univ code.In practice, typed languages are not usually used like this, probably because of convenience and practicality. See next point.
I find it very irritating that people continually bias their arguments for untyped languages in this fashion, as if typed languages need to "catch up" or something.Are there any typed languages for which highly dynamic IDEs exist, along the lines of those for Smalltalk or Self? If so, I want to play with them! If not, then what I was saying was not biased, since these are examples of "what current realistic implementations are capable of in terms of dynamic loading and so on." (Lauri Alanko's thesis seems relevant here.)
But this relates to the previous point: as long as DT languages ignore their type systemsUntyped languages don't have type systems.
I wrote "DT", you wrote "untyped". That's part of the stacked terminology deck here: I'm quite happy to agree that an untyped lambda calculus has no type system. But DT languages aren't untyped lambda calculi. A simple demonstration of this is the existence of soft type inferencers for languages like Scheme and Erlang.
Does the existence of these soft typers mean that Scheme and Erlang should be considered typed languages? Or are they untyped languages when you don't run the soft typer on their programs, and typed languages when you do? It makes much more sense to say that these languages have latent types, i.e. their programs have types which can be inferred by a soft typer. More importantly, and much more commonly, those types also inferred by the programmer.
Further, the situation is made even less black and white by the fact that an inferencer can't, without any hints, discover all the types - and I mean real, syntactic types - present in these programs. I'm not saying that all of the "program properties" which you referred to are types, but some of them are. An inferencer produces an approximation which can typically be improved by a programmer.
This is something else I find irritating, Anton. I spent many, many hours explaining exactly why and in what sense this is true,If you have explained in what sense "Untyped languages don't have type systems" is true, then either my points above must fit into your explanation somehow, or one of our positions is erroneous.
and I thought at last that people had started to grasp what a type is, what it is not,
If people have really grasped what a (syntactic) type is, then what I am saying should make sense to them -- that is, even DT programs contain latent type information, as evidenced by the fact that at least some of this information can be mechanically extracted. Further, this information is depended on by programmers when reasoning about their code.
My opening forum post in the prior thread was intended to made the case that type systems were interesting because of their utility when it comes to reasoning about code, and that this kind of reasoning takes place in DT languages as well as in static languages, which is why type systems are relevant even to DT programmers. I still consider that to be true, and I don't think any good evidence has been given to contradict it.
As a nice example of this in action, this LL1 post quotes a claim by Joe Armstrong, talking about a type-checking phase being applied to previously written Erlang programs: "The type system has uncovered no errors. The kernel libraries were written by Erlang 'experts' -- it seems that good programmers don't make type errors."
Joe ignored the fact that even good programmers do make type errors, but that these errors are ultimately caught, even if only at runtime, and corrected. The result of this process is that even DT programs can, and do, end up with consistent type schemes. Of course, to statically prove that, we have to do something like successfully run a type inferencer on the code. However, even if you fall back on some kind of Heisenberg-like effect, e.g. "type systems/schemes don't exist until you formally specify them", the fact remains that human programmers - aided by a debugging process - "somehow" end up creating valid type schemes. I quoted "somehow" because I don't think it's any mystery - they're reasoning about the program's types, albeit along with other program properties, to come up with working programs, which tend to have (or even must have) valid type schemes.
and what the relationship between typed and untyped languages is.
I'm actually not sure what your explanation is in this respect. We've seen that Univ isn't a complete explanation, and I don't think I've seen an alternative explanation of the relationship from you. In your defense, the usual type theory sources don't have much to say about this either. It's fine if you want to say that you prefer to stick to pure syntactic types, where you have formally specified type systems and languages and there's absolutely no ambiguity. It's also fine if you want to say that you're happy to restrict yourself to being able to embed DT programs in statically typed languages using a unitype. But as soon as you extend your claims beyond these very precisely-defined ones, and want to say anything about the nature of DT languages and their relationship to types, then what I've been talking about enters the picture.
Now you are diluting my message with your talk of "latent type systems."
I'm trying to discuss the relationship between syntactic types and DT languages. There obviously is a relationship, and to me it seems quite a bit deeper than most type theory explanations give it credit for. Traditional type theory doesn't seem to offer much to explain the abovementioned Erlang experience, for example.
If this dilutes your message, I suspect it's only because the message needs to be more clearly delineated along the lines I mentioned above, i.e. that you're only talking about types that are fully formally specified. However, you can't claim that types don't exist outside those boundaries, only that our formal descriptions of them are often incomplete, etc.
As far as I can tell, your notion of "latent type" only amounts to program properties which might be extractable with some blue-sky theorem prover, or more realistically a proof assistant being manually operated by a type theorist....or with a soft typing system assisted by hints from a programmer, which is much less blue-sky. But I'm not just talking about some theoretical future possibility: I'm saying that DT programs succeed, in part, by virtue of their programmers creating valid latent type schemes for them.
In particular, as a notion of "type system", latent type systems fail the "tractable" and "syntactic" conditions which you yourself quoted from Pierce.Soft typers seem to contradict this (although their developers might have something to say about tractability). In any case, Pierce characterizes his definition as "one plausible definition". Let's look at what else Pierce says:
Pierce: "this definition identifies type systems as tools for reasoning about programs"This applies to latent type systems: programmers use them for reasoning about their programs.
Pierce: "Another important element in the above definition is its emphasis on classification of terms -- syntactic phrases -- according to the properties of the values that they will compute when executed."As I've pointed out, the need to statically classify terms applies to DT programs as well as ST programs. It is impossible, in general, to reliably invoke operations without such classification.
Pierce: "A type system can be regarded as calculating a kind of static approximation to the run-time behaviors of the terms in a program."
The word "approximation" reminds us that not everything needs to be known statically. DT type schemes are certainly likely to be more approximate than ST ones - there are likely to be many more cases in which the exact operation being invoked is only known at runtime. But a programmer can only reliably perform operations with some knowledge of the properties of the values being operated on, even if it's "approximate" (e.g. expecting that an object accepts the "print" message). Do these properties always qualify as types? Presumably not - in some cases, they go well beyond what traditional type systems are capable of - but some of these properties do qualify as types.
Another way in which latent type systems mirror more traditional static type systems is that they're used to reject programs. However, the programmer has more discretion in this case than when rejection is performed mechanically. Rejection nevertheless does occur - there are many ways in which DT programs are designed to make sense from a type perspective, thus effectively rejecting alternative programs which make less sense. As I've previously pointed out, in some circles it's common practice to annotate functions with their type as a comment. Programmers constantly make design decisions which center around consistent usage of types.
I like Lauri Alanko's take on type systems, from his thesis referenced above, section 2.2:
Alanko: "A type system is a method for analyzing a program syntactically to prove the impossibility of certain erroneous conditions. It is based on types, syntactic structures that usually represent the sets of values which expressions can evaluate to. The type system works by assigning types to the expressions and variables of a program, and by checking that expressions are combined properly so that their types are compatible".
That entire description maps very well onto DT languages, with one change: "prove" usually becomes a weaker assurance, more like a theory of the program's types, which represents the best available knowledge at any given time, but may yet be falsified in future, requiring improvements to the theory. These activities are performed by the programmer, instead of mechanically, with assistance from runtime errors based on tagged values. These runtime errors are falsifications of the current theory, and their absence in the face of testing provides reasonable assurances as to the validity of the current theory of the program's types, among other things.
Physics vs. Mathematics
Based on the perspective in the previous paragraph, one can see DT programming as being more like physics, to ST programming's mathematics. Physicists are used to having theories that could be proved wrong at any time, by some previously untested special case. They even use theories that they know are wrong in some respect, that don't perfectly match observations. They put up with this because they have no alternative, because they are modelling "real" phenomena which have characteristics which can't simply be formalized away.
The areas which currently rely heavily on DT languages are rife with such characteristics, often having to do with complex interoperation between disparate systems, such as networks, databases, web servers, operating systems, and other programs. In these environments, the evolving-theory approach to development is often essential, and it's fairly natural that the type system aspect is simply fitted into this approach, even if theoretically better solutions exist.
Responding to one final comment of Frank's:
Instead of jumping on the type bandwagon, why not call your "latent types" "program properties"? Or, if you think they are different, please demonstrate how.This isn't about jumping on any bandwagon. If the above doesn't explain my position sufficiently clearly, or credibly, tell me what kind of demonstration is wanted, and I'll see what I can do, within reason.
Active forum topics
New forum topics