Paper! Milner Type Polymorphism

Paper Overview

The thrust of the paper is in its two theorems

• The semantic soundness theorem (section 3) says that IF a program is "well-typed", THEN evaluating that expression will not result in a type error at runtime.
• The syntactic soundness theorem (section 4) says that IF a certain algorithm (imaginatively named Algorithm W) can assign a type to an expression, THEN that expression is well-typed.

Putting them together, we see that any expression that Algorithm W can give a type to can be evaluated without runtime type errors.

The bulk of the paper is then concerned with the details of what type errors we are protecting against (which is defined by the semantics of the language in sections 3.1 and 3.2), what types actually are (sections 3.3 and 3.4), what it means for an expression to be well-typed (section 3.5), and the proofs of the two theorems (3.6 to the end of 4).

Section Headings

1. Introduction
2. Illustrations of the Type Discipline
3. A Simple Applicative Language and its Types

• The Semantic Soundness theorem

4. A Well-Typing Algorithm and its Correctness

• Algorithm W
• The Syntactic Soundness theorem
• Algorithm J

5. Types in Extended Languages

Section 3: The Semantic Soundness Theorem

Some possibly useful resources:

• Section 3 Cheat Sheet
• Semantic Soundness Theorem dissection. While studying the proof on page 364, I found myself continually having to refer to the definition of well-typed on page 362 and the semantic equation on page 358. So I saved myself approximately $372 in headache pills by making a PDF with six pages, one for each of the cases in the grammar.
• I also have various random study notes on the paper sitting in a Github repo.