The history of Standard ML
Autor: | Robert Harper, John Reppy, David MacQueen |
---|---|
Rok vydání: | 2020 |
Předmět: |
Parametric polymorphism
Functional programming Syntax (programming languages) Computer science Programming language Semantics (computer science) 010102 general mathematics Type inference 020207 software engineering 02 engineering and technology Standard ML Variety (linguistics) computer.software_genre 01 natural sciences Operational semantics 0202 electrical engineering electronic engineering information engineering 0101 mathematics Safety Risk Reliability and Quality computer Software computer.programming_language |
Zdroj: | Proceedings of the ACM on Programming Languages. 4:1-100 |
ISSN: | 2475-1421 |
DOI: | 10.1145/3386336 |
Popis: | The ML family of strict functional languages, which includes F#, OCaml, and Standard ML, evolved from the Meta Language of the LCF theorem proving system developed by Robin Milner and his research group at the University of Edinburgh in the 1970s. This paper focuses on the history of Standard ML, which plays a central role in this family of languages, as it was the first to include the complete set of features that we now associate with the name “ML” (i.e., polymorphic type inference, datatypes with pattern matching, modules, exceptions, and mutable state). Standard ML, and the ML family of languages, have had enormous influence on the world of programming language design and theory. ML is the foremost exemplar of a functional programming language with strict evaluation (call-by-value) and static typing. The use of parametric polymorphism in its type system, together with the automatic inference of such types, has influenced a wide variety of modern languages (where polymorphism is often referred to as generics ). It has popularized the idea of datatypes with associated case analysis by pattern matching. The module system of Standard ML extends the notion of type-level parameterization to large-scale programming with the notion of parametric modules, or functors . Standard ML also set a precedent by being a language whose design included a formal definition with an associated metatheory of mathematical proofs (such as soundness of the type system). A formal definition was one of the explicit goals from the beginning of the project. While some previous languages had rigorous definitions, these definitions were not integral to the design process, and the formal part was limited to the language syntax and possibly dynamic semantics or static semantics, but not both. The paper covers the early history of ML, the subsequent efforts to define a standard ML language, and the development of its major features and its formal definition. We also review the impact that the language had on programming-language research. |
Databáze: | OpenAIRE |
Externí odkaz: |