Conor McBride revolutionizes type inference

The Hindley-Milner let-rule operates on the basis that if we keep on restricting our ambitions for the expressiveness of the types we want for our programs, we reach the point where types are stupid enough that even computers can guess them. What happens if we reverse the information flow? Ambition for type expressivity can become rewarding if it increases the computer's ability to guess the *program*. This possibility has not escaped notice, thus far, but neither has it taken hold as the key to a language design. Fortunately, Milner's idea to ensure necessary coincidences by unification works perfectly well when the information flow is turned around. So let us (and our languages) be mindful about what we already know and open to new possibilities. I'll try to put my finger on some blind spots and some faulty learning, the better to blunder more effectively.

Video: http://youtu.be/ad4BVmPni7A
Slides: http://staff.computing.dundee.ac.uk/frantisekfarka/tiap/slides/Conor_McBride_-_Type_Inference_needs_Revolution.pdf

How can I upvote you?