How we got here
The genesis of enlightened programming languages
What we’re talking about
- ML - OCaml / SML
- lambda calculus (LC). Church.
Automated Theorem Proving
- Theorem provers and Martin-Löf.
- 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.
- 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.
- 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.
- the rise of the lazy functional PLs such as Hope, Miranda and LazyML. Some folks, faces and places.
- Haskell, one of the few times a design by committee worked (someone should study that and learn how they did it).
- Type classes. Wadler.
- A generalisation of eqtype variables from Standard ML.
- 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
- 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.
- See http://steshaw.org/how-we-got-here/resources.html
- A curated resource for the interested student.
- Includes key papers & books.
- Links to programming languages. Haskell, ML, proof assistants,
- less well-known research PLs such as ATS, Ur/Web, F*.