I recently uncovered a free computer science textbook which is not as well-known as it should be, called Programming Languages: Application and Interpretation by Shriram Krishnamurthi. One of the gems inside was a very lucid explanation of type systems and type inference.

I have been working recently on trying to explain the rather ad-hoc type inference algorithm I use in the Cat language in the form of a technical report. During this process I uncovered what I consider to be the best description of basic Hindley-Milner (HM) type inference in the book Programming Languages: Application and Interpretation by Shriram Krishnamurti, sometimes referred to as the PLAI. Type-inference is explained in Chapter 30

Other papers that I have found very helpful and accessible in learning about type-inference are:

• HMF: Simple type inference for first-class polymorphism by Daan Leijen(http://research.microsoft.com/users/daan/download/papers/hmf-tr.pdf)

• Basic Polymorphic Type-Checking by Luca Cardelli
  (http://research.microsoft.com/users/luca/Papers/BasicTypechecking.pdf)

I hope more language implementors will consider seriously the advantages of including type-checking in their languages (and optimizers), and explore the different ways that we can extend HM type-inference to make it even more powerful.