Standard ML

Standard ML（SML），是一个函数式、指令式、模块化^[1]的通用的编程语言，具有编译时间类型检查和类型推论^[5]。它流行于编译器作者和编程语言研究者和自动定理证明研究者之中。

Standard ML

编程范型	多范型：函数式, 指令式, 模块化^[1]
语言家族	ML
发行时间	1983年，​40年前​（1983）^[2]
型態系統	类型推论, 静态, 强类型
文件扩展名	.sml
網站	Standard ML Family GitHub Project
主要實作產品
SML/NJ, MLton
衍生副語言
Concurrent ML, Dependent ML（英语：Dependent ML）, Alice（英语：Alice (programming language)）
啟發語言
ML, Hope, Pascal
影響語言
ATS（英语：ATS (programming language)）, Elm, F#, F*, Haskell, OCaml, Python^[3], Rust, Scala

Standard ML是ML的现代方言，ML是用于LCF（英语：Logic for Computable Functions）（可计算函数逻辑）定理证明计划的编程语言。Standard ML在广泛使用的语言之中与众不同，源于它具有正式规定《The Definition of Standard ML》 ^[4]，给出了语言的类型规则（英语：Type rule）和操作语义^[6]。

实现

存在很多SML实现，包括：

标准：

• Standard ML of New Jersey（缩写为SML/NJ），由普林斯顿大学和贝尔实验室在1986年开始联合开发的实现，是一个完全的编译器，具有关联的库、工具、交互式外壳和文档，还支持Concurrent ML^[7]。
• MLton，是一个全程序优化（英语：Interprocedural optimization）编译器，它产生相比其他ML实现非常快的代码^[8]。
• ML Kit^[9]，由爱丁堡大学的Mads Tofte（英语：Mads Tofte）等人在1989年发起开发^[10]，是一个非常紧密的基于了标准定义的实现，它集成了具有基于区域内存管理（英语：region-based memory management）的垃圾收集器，内存分配指令由编译器推论，可以停用垃圾收集器来支持实时应用。
• Poly/ML^[11]，由剑桥大学的David Matthews开发^[12]，是一个Standard ML的完全的实现，它产生快速代码并支持多核硬件（通过Posix线程）；它的运行时间系统，进行并行垃圾收集和不可变子结构的在线共享。
• HaMLet^[13]，由MPI-SWS（英语：Max Planck Institute for Software Systems）的Andreas Rossberg编写，是一个SML解释器，意图成为精确且便宜的标准定义参考实现。
• Moscow ML^[14]，是一个轻量级实现，基于了CAML Light运行时引擎。

派生：

• SML#^[15]，是日本东北大学电气通信研究所（英语：Research Institute of Electronic Communication）开发的SML家族新语言，提供了记录多态性和C语言互操作性。它是常规的本机编译器，名字的“#”号不暗示着要在.NET框架上运行。
• Alice（英语：Alice (programming language)），Alice ML是萨尔兰大学开发的基于Standard ML的函数式编程语言，它增加了惰性求值、并发性（多线程和通过远程过程调用的分布式计算）和约束编程特征。
• SOSML^[16]，是用TypeScript写的SML实现，可以直接运行在web浏览器内。它实现了大多数SML语言和选择的部份SML基本库。

研究：

• Isabelle/ML，剑桥大学的Larry Paulson（英语：Larry Paulson）开发的Isabelle，将并行Poly/ML集成入交互式定理证明器^[17]，它具有一个高端的IDE（基于了jEdit），用于官方Standard ML（SML'97）、Isabelle/ML方言和这个证明语言^[18]。开始于Isabelle2016，它还有一个源代码级的ML的调试器。
• CakeML^[19]，是一个基于了SML实质性子集的语言，它实现为x86-64机器码的REPL，带有正式验证的运行时间库和到汇编代码的转换。
• TILT^[20]，是一个完全验证了的SML编译器，它使用有类型的中间语言来优化代码和确保正确性，并可以编译成有类型的汇编语言（英语：Typed assembly language）。
• Poplog（英语：Poplog）系统实现一个版本的SML，还有POP-11（英语：POP-11）、可选的Common Lisp和Prolog，允许混合语言编程。

所有这些实现都是开源的并可自由的获得。其中多数用SML实现了自身。不再有任何商业SML实现。

使用SML的项目

证明辅助器HOL4（英语：HOL (proof assistant)）、Isabelle、LEGO（英语：LEGO (proof assistant)）和Twelf（英语：Twelf）是用Standard ML写成。它还用于编译器制作和集成电路设计比如ARM^[21]。

参见

• OCaml
• F#

引用

1. David MacQueen. . LFP '84 Proceedings of the 1984 ACM Symposium on LISP and functional programming. August 1984: 198–207 [2021-09-01]. （原始内容存档于2021-09-01）. 
   David Macqueen. . 1988 [2021-09-03]. （原始内容存档于2021-09-03）. 
2. Robin Milner. (PDF). 1983 [2021-09-02]. （原始内容 (PDF)存档于2021-11-06）. 
   Robin Milner, Robert Harper, David B. MacQueen. (PDF). 1986 [2021-09-02]. （原始内容 (PDF)存档于2021-09-02）.  School of Informatics Laboratory for Foundations of Computer Science, Edinburgh University.
3. itertools — Functions creating iterators for efficient looping — Python 3.7.1rc1 documentation. docs.python.org. [2020-04-25]. （原始内容于2020-06-14）. 
4. Milner, Robin; Tofte, Mads; Harper, Robert; MacQueen, David. (PDF). MIT Press. 1997 [2021-09-01]. ISBN 0-262-63181-4. （原始内容 (PDF)存档于2022-03-09）. 
5. Damas, Luis; Milner, Robin. (PDF). 9th Symposium on Principles of programming languages (POPL'82). ACM: 207–212. 1982 [2021-09-02]. ISBN 978-0-89791-065-1. doi:10.1145/582153.582176. （原始内容 (PDF)存档于2022-03-22）. 
   Damas, Luis. (PDF) (PhD论文). University of Edinburgh. 1985 [2021-09-02]. hdl:1842/13555. CST-33-85. （原始内容 (PDF)存档于2020-01-28）. 
6. Cardelli, Luca. (PDF). ACM Computing Surveys. March 1996, 28 (1): 263–264 [2021-09-01]. doi:10.1145/234313.234418. （原始内容 (PDF)存档于2020-11-09）. 
7. . [2020-04-25]. （原始内容存档于2020-05-01）. 
8. mlton.org. [2020-09-27]. （原始内容于2020-08-28）. 
9. ML Kit（页面存档备份，存于互联网档案馆）
10. Lars Birkedal, Nick Rothwell, Mads Tofte, David N. Turner. . 1993 [2021-10-19]. （原始内容存档于2021-09-13）. 
11. Poly/ML（页面存档备份，存于互联网档案馆）
12. David Matthews. . 1986 [2021-10-19]. （原始内容存档于2021-10-26）. 
13. HaMLet（页面存档备份，存于互联网档案馆）
14. . [2021-09-02]. （原始内容存档于2022-02-12）. 
15. SML#（页面存档备份，存于互联网档案馆）
16. SOSML（页面存档备份，存于互联网档案馆）
17. Isabelle（页面存档备份，存于互联网档案馆）
18. (PDF). [2021-09-01]. （原始内容 (PDF)存档于2021-09-01）. Isabelle/ML is best understood as a certain culture based on Standard ML. Thus it is not a new programming language, but a certain way to use SML at an advanced level within the Isabelle environment. This covers a variety of aspects that are geared towards an efficient and robust platform for applications of formal logic with fully foundational proof construction — according to the well-known LCF principle. There is specific infrastructure with library modules to address the needs of this difficult task. 
19. CakeML（页面存档备份，存于互联网档案馆）
20. TILT（页面存档备份，存于互联网档案馆）
21. Jade Alglave; Anthony C. J. Fox; Samin Ishtiaq; Magnus O. Myreen; Susmit Sarkar; Peter Sewell; Francesco Zappa Nardelli. (PDF). DAMP 2009: 13–24. [2021-08-31]. （原始内容 (PDF)存档于2020-09-19）. 

外部链接

• Standard ML Family GitHub Project（页面存档备份，存于互联网档案馆）
• Programming in Standard ML（页面存档备份，存于互联网档案馆）
• cmlib － A basic library of algorithms and data structures (a la NJlib) （页面存档备份，存于互联网档案馆）
• SML Help （页面存档备份，存于互联网档案馆）
• Awesome Standard ML （页面存档备份，存于互联网档案馆）
• Programming in Standard ML '97: An On-line Tutorial（页面存档备份，存于互联网档案馆）
• CSE341: Programming Languages（页面存档备份，存于互联网档案馆）, Dan Grossman, University of Washington.
• COMP 105 pages: Learning Standard ML （页面存档备份，存于互联网档案馆）