On Sun, Jul 13, 2014 at 9:45 AM, Jonathan S. Shapiro <[email protected]> wrote:
> Systems programmers are pretty smart. They *can* learn just about > anything that solves a problem for them. This certainly includes type > systems. But the key words are "that solves a problem for them". Before > they are going to commit the effort to learn something like this, they need > to see a clear benefit to some immediate problem they are facing. Given > such a benefit, they will then ask how much investment of time and energy > is needed to learn that new thing. Then and only then will they learn the > new thing. > Being a (mostly) systems programmer and knowing many of them, I'd say this is a good characterization. I think of systems programmers as Local optimizers with a capital "L", as in "Best value for the resulting product to humanity given Local time and what is proved to be true about tools at hand". One reason that inference is so important is that it allows those > programmers to approach type system issues incrementally and as needed. > When inference is incomplete - which is what makes you need to fiddle the > type annotations - it stops being a way to ease in to the language and > starts becoming an obstacle in its own right. > IMO, this discussion is missing the elephant in the room, that one of the big-undesirable properties of both dynamic-typing and inference-typing, is the lack of human-readable coherent symbolic type documentation in the code. Anytime I look at code with my eyes and don't understand what it does, it's becoming an obstacle in it's own right. Yes, static typing systems encourage overconstrained programs! However, dynamic and inference systems encourage under-named typing ontologies! There is real value in Aristotelian Ontology. For example, I like the idea of anonymous structures (where the declaration requires field-names). However, I avoid and dislike tuples in all their forms (including LISP/Scheme), because they introduce too much under-named data and ad-hoc "order dependent contract" between different places in the code. Do you see the issue? How do you hope to address it? ----- I think there is more middle ground between the "people who want type-names for clarity" and the "people who want more flexible and stronger software" than we're exploring. It might be interesting to see a global inference engine used to provide *warnings* about uses of over-constrained types. Of course for this to be useful, we'd also need to change the static-type system itself to remove some classic encouragements of over-and-under constraint. Such as : (1) implicitly making all implementation types interface types -- This would help achieve type-contracts which are less constrained, but still well named (2) add a lightweight "colored-type" construct, which injects a subtype constraint into otherwise identical (and possibly final) structural types. In a way, this is a generalization of the enum concept to any type, as enums could be thought of as colored-ints. A Vector3#worldspace type would not be implicitly convertible to Vector3#objectspace but being otherwise identical. This would effectively make every argument parametric in "type color", allowing the type system to help us find more errors. The inference engine would be inferring the validity of type-color interactions. (does this exist in PL somewhere?) That's just an on-the-spot brainstorm, so I don't know if it leads anywhere. However, my main point is that if you give me a perfect interference system which can handle any type relationship automagically, I won't choose it unless I can cause it to be an error not to specify a typename in most place -- because those type names are the documentation which makes the code readable.
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
