HOPL IV
Sun 20 - Tue 22 June 2021
co-located with PLDI 2021
Tue 22 Jun 2021 13:30 - 14:45 at HOPL - Tuesday Early Afternoon Chair(s): Kim Bruce, Brent Hailpern

The ML family of languages evolved from the Meta Language (hence ML) of the LCF theorem proving system developed by Robin Milner and his research group at Edinburgh from 1974 through 1978. The basic framework of the language design was inspired by Landin’s ISWIM language from the mid 1960s, which was basically a sugared syntax for practical programming in Church’s lambda calculus (augmented with primitive values and operations). The LCF project added features to the ISWIM framework satisfy the requirements of a metalanguage for constructing proofs: a static type system to guarantee that programs that purport to produce \emph{theorems} in the object language (the LCF logic) actually produce logically valid theorems, and an exception mechanism for dealing with proof tactics that could fail. The language followed ISWIM in using strict evaluation and allowing impure side-effects in the form of variable assignments and exceptions.

LCF/ML soon generated interest as a potential general purpose language, and Luca Cardelli in 1980-81 produced the first independent implementation of ML as a free-standing language, in the process introducing some interesting language innovations in the areas of data types and declaration structures. The Hope language developed in Rod Burstall’s group at Edinburgh shortly after LCF/ML borrowed ideas from ML and developed some new features (algebraic data types and pattern matching, and a rudimentary module system) that could be easily adapted to ML. In the spring of 1983 Milner began an effort to integrate these new ideas into a new version of the language that would become the Standard ML (SML) Core language, and MacQueen proposed a preliminary module system. A series of design meetings over the next three years refined both the Core language and the module system, and parallel intensive work on a formal semantics led to the publication of the formal definition of the Standard ML language in 1990.

ML was initially implemented as an integrated component of the LCF theorem prover, with ML code being compiled to LISP, which was then interpreted. Cardelli’s stand-alone compiler was written in Pascal and generated VAX machine language. It became the basis for the Edinburgh ML system designed around a functional abstract machine (FAM), and during the Standard ML design period Edinburgh ML was gradually evolved into a prototype Standard ML compiler. Dave Matthews created an early Standard ML compiler based on his Poly language and compiler (1985), and in 1986 Appel and MacQueen began to develop an entirely new compiler, Standard ML of New Jersey, dedicated to producing highly optimized code. More recent implementations include Moscow ML, MLton, and the ML Kit.

By the mid 1990s significant experience with the Standard ML design had been accumulated through the work on the formal definition, multiple implementation efforts, and the development of reasonably large software systems written in SML, and a core group of designers felt it would be valuable to attempt a modest revision of the the language design, leading to the creation of Standard ML ’97 and the publication of the Definition of Standard ML (Revised). This revision simplified the Core type system in significant ways (notably the value restriction rule to control the interaction of polymorphism and mutable data). It also both simplified and enriched the module system, making signatures more expressive and providing for opaque signature matching.

The evolution of Standard ML has been stabilized (and constrained) by the published formal definitions, which had the beneficial effect of enabling multiple (largely) compatible implementations of the language. Meanwhile, other branches of the ML language family were developing independently, notably Caml and Objective Caml at INRIA, Moby at Chicago and AT&T Research, and Alice at Saarland University. These other branches have explored a wider design space, including hybrid designs that aim to encompass object-oriented programming. During the 90s some members of the ML community carried out extensive discussions about what a next generation ML would be like, centering on the question of whether ML should adopt ideas and features from object-oriented languages. Reppy and Fisher’s Moby language was one result of these discussions, representing the school of thought embracing object oriented programming. Current continuing work on successor ML'' pursues a more classical line of development.

This survey starts with background developments in the British school of programming language research in the 1960’s and 70’s (Strachey, Landin, Burstall, Milner). It then covers the original LCF/ML design (Milner, L. Morris, Newey, Wadsworth, Gordon) and Cardelli ML, before discussing the Standard ML design effort (1983 - 1986) and the formal definition (1986 - 1989). Further developments in the 1990s included the 1995 - 1997 revision, the ML 2000 discussions, and the completion of the Standard ML Basis library. We cover in detail important conceptual contributions of Standard ML, including polymorphic type inference, algebraic datatypes, and a functional module language. The implementation history of the language will also be covered. An extensive bibliography of SML-related literature will also be included.

#### Tue 22 JunDisplayed time zone: Eastern Time (US & Canada) change

 13:30 - 16:15 Tuesday Early AfternoonPapers at HOPL Chair(s): Kim Bruce Pomona College, Brent Hailpern IBM Research 13:3075mTalk The History of Standard MLPapersDavid MacQueen University of Chicago (Emeritus), Robert Harper Carnegie Mellon University, USA, John Reppy University of Chicago, USA DOI 15:1560mTalk Evolution of Emacs LispPapersStefan Monnier Université de Montréal, Michael Sperber Active Group GmbH DOI