On Wed, Jul 9, 2014 at 10:06 PM, Jonathan S. Shapiro <[email protected]> wrote: > Since the Tofte-Talpin region system also pushes you to semi-unification, > we'll at least end up with a set of deficiencies that manifest in a > consistent way in different parts of the type system. I think it would feel > awkward if region type inference tended to fail for qualitatively different > reasons than (e.g.) polymorphic recursion. It makes it much harder to get > any intuitive handle on what's going on.
Type inference doesn't have to be intuitive. Try it without annotations, if it doesn't work or doesn't do what you want, add annotations. In practice, Coq and Agda have great type inference, even though inference for dependent typing cannot be remotely complete. Compared to Java, Coq hardly needs any annotations, and that's with a harder inference problem. In theory, Coq's type inference is a mess; I don't know how it works in general, and I occasionally run into bugs. But in practice, it was easy to get used to. I don't notice a big difference in convenience between Coq and OCaml. And everything I read suggests that Agda and Idris do inference even better than Coq. > Type inference is a thing that sits on several different kinds of sharp > edges all at once. I'm tempted to say that we should just require top-level > procedure types to be annotated. The problem with that is that humans turn > out to be pretty bad at discovering complete types when the types start > getting complicated, and we have a bunch of interacting typing problems > going on at once in our type system in ways that other languages have never > explored. If by "complete types" you mean principal or minimal types, well I don't think the notion makes much sense as the type system gets stronger. In a strong type system, types are almost (or exactly) like specifications. It's possible to overspecify your program, making it less convenient to use because of the unnecessary detail of its type, and painting yourself into a corner by over-relying on its accidental properties. With strong types, choosing the right type is an act of design, and will in general require human intelligence. An easily-specified computer program hasn't a chance. So humans turn out to be pretty bad at choosing good types at first? That's because it's hard! Type inference won't magically solve the problem. In my opinion, the closest thing to a solution is for the type system to make sense to the programmer. The type system should be a tool for the programmer to think with. Artificial tweaks to improve type inference can actually make this worse. I find OCaml's polymorphic variant types to be very unintuitive; a lot of the details seem rigged just to make inference work. Even if you would like to avoid types as strong as specs, I don't see why a nice neat situation regarding type inference is so important. If type inference is too hard to have a beautiful general solution, so be it. What really seems important is that the type inference not be inexcusably stupid, like in Java, C#, C, C++... _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
