Genesis of ML as a tactics language for the LCF theorem prover.
Mention some of the people and places such as Robin Milner and University of Edinburgh.
Lisp
Perhaps mention of lisp as a simple external syntax for the LC. This is were lisp remains in the past. Essentially it’s light goes out.
CAML
The first implementation of CAML in Lisp. Mention some early INRIA researchers such a Gérard Huet.
ML and SML
The work on ML/SML. One of the researchers went from the US -> Scotland or the other way around. Find that guy and mention him :).
Modules in SML and OCaml. Perhaps mention applicative v generative module systems and the similarity with Haskell’s type classes. Mention modular type classes by Dreyer, Harper and Chakravarty.
Lazy MLs
the rise of the lazy functional PLs such as Hope, Miranda and LazyML. Some folks, faces and places.
Haskell
Haskell, one of the few times a design by committee worked (someone should study that and learn how they did it).
Type Classes
Type classes. Wadler.
A generalisation of eqtype variables from Standard ML.
Proof Assistants
Verified software and dependent types.
Languages such as Agda, Coq, Idris.
These influence the Glorious dialect of Haskell available in GHC.
Here, we’re full-circle back to theorem provers :D
Further Resources
Key references
How to make ad-hoc polymorphism less ad hoc. Philip Wadler and Stephen Blott. 16’th Symposium on Principles of Programming Languages, ACM Press, Austin, Texas, January 1989.