Years of endless debates about static type annotations regurgitating the same information over again have led me to shy awayfrom them in recent years. I've done pretty well, yet here I am in the gravity field of another one. I'm not sure how long this will last but for this day, I am somewhat interested in continuing.
PJE writes in a comment...
Um, just because a given use case can be accomplished without a given tool, doesn't mean the tool is useless, or isn't useful for that use case. If that were true, we'd never use anything but machine code.I have not found any useful scenarios where I want static type annotations. There's not much more to say than that. I'd like to hear of scenarios others have found useful so I can compare them to my own.
Meanwhile, I notice you haven't responded to the point that solid integration with statically typed languages often requires type annotation; e.g. jythonc's use of special patterns in docstrings. Integration with other languages, documentation, and runtime introspection/adaptation are my use cases for type annotation.I'm not sure what you mean by "solid" integration. I have done production-quality integration between "agile" languages like Lisp, Smalltalk, and Python with "rigid" languages like Pascal, C, C++.
There are situations where the more rigid languages have required, say, a 32-bit integer or a specifically formatted sequence of values (i.e. "struct" or "record"). "Agile" languages tend to provide integers that are not limited by the word size of the underlying hardware. In scenarios like this then, on the agile side of the integration a check is necessary that the integer will fit in the rigid size of 32-bits and so on. Likewise a conversion is necessary to actually format the scalar data and structured data into the kind expected on the rigid side.
I would not call these expressions "static type annotations" in the agile language though. Rather they are hoops I'd not have to jump through as much if the rigid language were more agile. The language systems I have used that I can recall have tended to allow me a way to express these in the agile language itself rather than in a comment or doc string, but that's a minor point.
Languages like Java and C# are less rigid and given their capabilities for reflection, integration with more agile languages tend to be more automatic. And so Jython and Python.Net among others tend to do most of the conversion automatically without special annotations or coding.
Corner cases require more programmer attention but that's also a minor point. They could agree on a common model for data exchange such as is done in CORBA and it's descendent WS-xxx. Doing integration via CORBA using Smalltalk is so easy I believe had more programmers been working this way the WS-xxx fiasco would never have been. Rather improvements to CORBA's relationship with HTTP would have been getting all the intention. These are market force issues, not software.
Another source of feedback on this is the Inter-Language Unification work done at Xerox. Related to CORBA but more focused on integration aspects and RPC, where CORBA was beginning to branch out into a variety of distributed programming models.
I don't see how type inference helps with either documentation or introspection, either. If it's pure "duck typing", how is the system going to infer that I want an IAtomicStream, say, versus an IRawStream, if the two have the same methods? Duck typing isn't sufficient to distinguish different *semantics* of a type/interface, only its method signature -- and that is not sufficient for documentation!If you need an
IAtomicStream on the rigid side then there
is probably enough information to infer that from the code on the
agile side. If the rigid specification is ambiguous (well, then it's
not really a "specification" is it?)... then, yes, you need to have
some kind of an expression on the agile side to disambiguate.
The point is, this is a burden rather than a feature. Why would I *want* to work at this level of detail?
A good bit of information on the power of inference for agile languages can be found in the implementation of the Stalin Scheme compiler, see "Flow-Directed Lightweight Closure Conversion" by Jeffrey Mark Siskind.
Documentation needs to present the semantics of the interface, so that if you are implementing that interface yourself, you know what semantics to implement.The documentation I want to see is (1) executable examples or (2) technical memos that augment executable examples. Period.
Likewise, for introspection, I don't see how an implicit signature helps. Let's say I want to create an XML schema for a document format that can contain messages that get converted to method calls on some object. If each of those methods uses a different set of methods on their arguments, I'm going to end up defining new types for each method, which might be okay for the computer to process, but for a human being it's going to be a mess to understand.I am not sure what this example is about. I agree there are integration scenarios where something like an XML Scheme is required to specify the kinds of messages that can be exchanged between language-independent processes. That does not in any way imply that static type annotations are a benefit to the languages I use to implement the independent processes.
Type inference, IMO, is just type checking. It doesn't seem to me to be useful for anything else -- and like you, I'm not interested in type checking! (I suppose it could be used for optimization in some cases, but only if you can statically prove a concrete type - not just an operation signature.)Type inference is better than type annotation. The real benefit I see is in getting even more capable agile modeling and inferencing tools by extrapolating from recent work in model checking. Simple, even compound, type checks are uninteresting. We do need a lot of help with concurrent state machines however. Tools that can tell me more about *real* behavior problems rather than simple type checks should be getting all this attention.
Now, perhaps I could be wrong, and there is some other way to accomplish these use cases that's just as clean. If so, I'd sure like to see them. I personally don't see that any of my uses for type annotation *can* be satisfied by inference; there's just not enough information. Heck, I don't see how a *human* could do the inference in the absence of added documentation, let alone a computer. It would be little more than blind guessing.I think I see one use case here... how to integrate languages that have different data models. I agree system integration requires some kind of agreement on specifying data integration. I'm not sure what else I am seeing here.
OK. I am getting tired of writing about type checking. I think we're in agreement on this use case of language-independent data integration.