Lambda the Ultimate

If you check out the slide presentation discussed previously, you will see that this is a well-known trade-off in type system design.

To quote: "The more interesting your types get, the less fun it is to write them down!"

I don't really agree with comments like "visually in the source code, if nothing else". I used to be enamoured with ML's type inference and lack of explicit type annotations, but these days I'm not so much.

The basic problem is that in a non-trivial project, code is there to be read as much as it is to be written. In order to understand a program you typically need to know the types of things. The type inference algorithm for Hindley-Milner is hard (doubly exponential and provably can't be improved upon I think?), and you're basically forcing the reader to run that in their head (this is mitigated by a good IDE or prompt, but they still need to take the trouble to look up the type). Explicit type annotations don't take up that much room and have significant readability advantages, at the expense of putting a small burden of commenting on the writer.

I guess this is dual to the old "Why write unit tests to check these things when the type system can prove it for you?": "Why write comments to explain this aspect of the code when the type annotations can do it for you?"

And of course if you move to more complicated type systems, like dependently typed ones or ML-sub, the situation with type inference gets even worse.

If you'll pardon the somewhat glib response, I don't think we have verbosity problem. I think we have a verbosity *solution* to the lack of readability problem. ;-)

I just don't think that type inference is very viable for type systems in which the types are less disjoint than in Hindley-Milner. Dynamic dispatch and overloading particularly hurt it.

Let's take the classic stupid example. Camera and Gun types.

Each has a function shoot.

I define a function bangBang(x) { shoot(x); shoot(x) }

What should the type of bangBang be?

The compiler could create a type class or kind combining Camera and Gun, say 'shootable', but why should it? They're really not at all related. They just happen to have a method name in common, and littering the world with an abundance of unneeded type classes is hardly cutting down on verbosity.

It's pretty easy to come up with other similar examples.

Of course, type inference is still possible for a largeish subset of the language. But it's not going to solve the verbosity problem because the areas with the increased verbosity that worries you are exactly the areas the type inference is no longer going to work in. Further this means that the look of the code is going to be awfully inconsistent, with type declarations being present or not seemingly at random.

A better place for type inference is probably entirely in the tool support. Types which can be inferred are inserted for you automatically in the function definitions (I don't just mean displayed - they automatically get inserted as part of the code). Type annotations which can't simply be inferred will give you a pretty red underline saying "I can't infer this type. Please tell me what it is".

On an idle note, I've just had a really cool idea. Why doesn't the IDE colour code variables based on their type? That would help readability matters a lot and definitely allow one to see at a glance what type something was, even if its type declaration was many lines back. :-) (Only half in jest).

That is basically the core of my comment, yes. Given a good display mechanism for automatic type inference (ideally one that elegantly integrates with the case where you do need the explicit type annotations, which is why I suggested the system adding them to the code directly), I would withdraw all objections to type inference and consider it an awesome tool I would dearly love to have. :-)