On Understanding Types, Data Abstraction, and Polymorphism

Cardelli and Wegner's On Understanding Types, Data Abstraction, and Polymorphism from 1985 is a treat. No wonder it has more than 2000 citations on Google Scholar.

It starts off with a simple functional language, and then adds universal and existential quantification. Universal quantification (∀) brings parametric polymorphism ("length returns the length of any list, whatever the type of its contents are"). Existential quantification (∃) lets you hide the details of a data type ("there exists some data type that implements a stack, but I'm not telling you more"). All of this is described in terms of a set-based description of types, which clears up a lot of issues.

It seems that this paper is the granddaddy of papers about polymorphism. It's expository style is unmatched.

P.S. I discovered this paper while skimming Adrian Moors' thesis Type Constructor Polymorphism for Scala: Theory and Practice. Its final chapter gives a great overview of where type systems are going.