This is a follow-up to Milner’s introduction of the type inference algorithm known as Hindley-Milner or Algorithm W. Here they provide a sketch of a proof that it infers “principal” types which are the most general possible types. (This proof was given by Hindley over a decade earlier, but apparently Milner nor the any of the reviewers knew about it.) It’s the sort of paper that wastes no ink on pesky prose explanations of the nice compact formulas, which is great for the trees, but really annoying when any of those formulas contain typos. If you’re not already familiar with the subject matter, you might spend an awful lot of time trying to figure out whether they really meant theta-sub-one when they wrote theta-sub-two.