imported>ExultantEditor 来自 2025年12月26日 (五) 16:36

2025-12-26T16:36:42Z

新页面

{{Infobox programming language
| name = Standard ML
| logo =
| paradigm = [[编程范式|多范型]]：[[函数式编程|函数式]], [[指令式编程|指令式]], [[模块化编程|模块化]]<ref name=“module”>{{cite journal|title=Modules for Standard ML|journal=LFP '84 Proceedings of the 1984 ACM Symposium on LISP and functional programming|pages=198–207|url=https://www.researchgate.net/publication/2477673_Modules_for_Standard_ML|author=David MacQueen|date=August 1984|access-date=2021-09-01|archive-date=2021-09-01|archive-url=https://web.archive.org/web/20210901131042/https://www.researchgate.net/publication/2477673_Modules_for_Standard_ML}}<br />{{cite web|title=An Implementation of Standard ML Modules|author=David Macqueen|year=1988|url=http://citeseerx.ist.psu.edu/viewdoc/download;jsessionid=9D69EB6BB01C953661AD5591A22D93B9?doi=10.1.1.48.6127&rep=rep1&type=pdf|access-date=2021-09-03|archive-date=2021-09-03|archive-url=https://web.archive.org/web/20210903012529/http://citeseerx.ist.psu.edu/viewdoc/download;jsessionid=9D69EB6BB01C953661AD5591A22D93B9?doi=10.1.1.48.6127&rep=rep1&type=pdf}}</ref>
| family = [[ML语言|ML]]
| year = {{Start date and age|1983|df=yes}}<ref>{{cite web|title=A Proposal for Standard ML|author=Robin Milner|year=1983|url=https://smlfamily.github.io/history/SML-proposal-11-83.pdf|access-date=2021-09-02|archive-date=2021-11-06|archive-url=https://web.archive.org/web/20211106091506/https://smlfamily.github.io/history/SML-proposal-11-83.pdf}}<br />{{cite web|title=Standard ML: Report ECS-LFCS-86-2|author=Robin Milner, Robert Harper, David B. MacQueen|year=1986|url=https://www.pure.ed.ac.uk/ws/portalfiles/portal/16547288/Standard_ML_ECS_LFCS_86_2.pdf|access-date=2021-09-02|archive-date=2021-09-02|archive-url=https://web.archive.org/web/20210902153857/https://www.pure.ed.ac.uk/ws/portalfiles/portal/16547288/Standard_ML_ECS_LFCS_86_2.pdf}} School of Informatics Laboratory for Foundations of Computer Science, Edinburgh University.</ref>
| designer =
| latest release version = Standard ML '97<ref name="def"/>
| latest release date = {{Start date and age|1997|df=yes}}
| typing = [[类型推论]], [[类型系统|静态]], [[类型系统|强类型]]
| implementations = [[新泽西Standard ML|SML/NJ]], [[MLton]]
| dialects = [[Concurrent ML]], {{le|Dependent ML}}, {{le|Alice (编程语言)|Alice (programming language)|Alice}}
| influenced_by = [[ML语言|ML]], [[Hope (编程语言)|Hope]], [[Pascal (程式语言)|Pascal]]
| influenced = {{le|ATS (编程语言)|ATS (programming language)|ATS}}, [[Elm (编程语言)|Elm]], [[F♯|F#]], [[F*]], [[Haskell]], [[OCaml]], [[Python]]<ref>{{cite web|url=https://docs.python.org/3/library/itertools.html|title=itertools — Functions creating iterators for efficient looping — Python 3.7.1rc1 documentation|website=docs.python.org|accessdate=2020-04-25|archive-date=2020-06-14|archive-url=https://web.archive.org/web/20200614153629/https://docs.python.org/3/library/itertools.html|dead-url=no}}</ref>, [[Rust (编程语言)|Rust]], [[Scala]]
| file_ext = .sml
| website = [https://smlfamily.github.io/ Standard ML Family GitHub Project]
}}
'''Standard ML'''（'''SML'''），是一个[[函数式编程|函数式]]、[[指令式编程|指令式]]、[[模块化编程|模块化]]<ref name=“module” />的[[通用编程语言|通用]]的[[编程语言]]，具有[[类型系统|编译时间类型检查]]和[[类型推论]]<ref name="Damas">{{cite conference | last1 = Damas | first1 = Luis | author-link2 = Robin Milner | last2 = Milner | first2 = Robin | date = 1982 | title = Principal type-schemes for functional programs | conference = 9th Symposium on Principles of programming languages (POPL'82) | pages = 207–212 | publisher = ACM | url = http://web.cs.wpi.edu/~cs4536/c12/milner-damas_principal_types.pdf | isbn = 978-0-89791-065-1 | doi = 10.1145/582153.582176 | access-date = 2021-09-02 | archive-date = 2022-03-22 | archive-url = https://web.archive.org/web/20220322134254/http://web.cs.wpi.edu/~cs4536/c12/milner-damas_principal_types.pdf }}<br />{{cite thesis | first = Luis | last = Damas | date = 1985 | title = Type Assignment in Programming Languages | url = https://prl.ccs.neu.edu/img/d-thesis-1984.pdf | degree = PhD | publisher = University of Edinburgh | id = CST-33-85 | hdl = 1842/13555 | access-date = 2021-09-02 | archive-date = 2020-01-28 | archive-url = https://web.archive.org/web/20200128232639/http://prl.ccs.neu.edu/img/d-thesis-1984.pdf }}</ref>。它流行于[[编译器]]作者和[[程式语言理论|编程语言研究]]者和[[自动定理证明]]研究者之中。

Standard ML是[[ML语言|ML]]的现代方言，ML是用于{{le|可计算函数逻辑|Logic for Computable Functions|LCF}}（可计算函数逻辑）定理证明计划的编程语言。Standard ML在广泛使用的语言之中与众不同，源于它具有正式规定《The Definition of Standard ML》
<ref name="def">{{cite web
| last1 = Milner
| first1 = Robin
| last2 = Tofte
| first2 = Mads
| last3 = Harper
| first3 = Robert
| last4 = MacQueen
| first4 = David
| title = The Definition of Standard ML (Revised)
| url = https://smlfamily.github.io/sml97-defn.pdf
| publisher = MIT Press
| year = 1997
| isbn = 0-262-63181-4
| access-date = 2021-09-01
| archive-date = 2022-03-09
| archive-url = https://web.archive.org/web/20220309034143/https://smlfamily.github.io/sml97-defn.pdf
}}</ref>，给出了语言的{{le|类型规则|Type rule}}和[[操作语义]]<ref>{{cite journal |first=Luca |last=Cardelli |url=http://www.cs.colorado.edu/~bec/courses/csci5535/reading/cardelli-typesystems.pdf |title=Type Systems |journal=ACM Computing Surveys |date=March 1996 |volume=28 |issue=1 |pages=263–264 |doi=10.1145/234313.234418 |access-date=2021-09-01 |archive-date=2020-11-09 |archive-url=https://web.archive.org/web/20201109220414/https://www.cs.colorado.edu/~bec/courses/csci5535/reading/cardelli-typesystems.pdf }}</ref>。

==实现==

存在很多SML实现，包括：

'''标准'''：
* [[新泽西Standard ML|Standard ML of New Jersey]]（缩写为SML/NJ），由[[普林斯顿大学]]和[[贝尔实验室]]在1986年开始联合开发的实现，是一个完全的编译器，具有关联的库、工具、交互式外壳和文档，还支持[[Concurrent ML]]<ref>{{Cite web |url=http://www.smlnj.org/ |title=smlnj.org |accessdate=2020-04-25 |archive-date=2020-05-01 |archive-url=https://web.archive.org/web/20200501115826/http://www.smlnj.org/ |dead-url=yes }}</ref>。
* [[MLton]]，是一个{{le|过程间优化|Interprocedural optimization|全程序优化}}编译器，它产生相比其他ML实现非常快的代码<ref>{{Cite web |url=http://www.mlton.org/ |title=mlton.org |accessdate=2020-09-27 |archive-date=2020-08-28 |archive-url=https://web.archive.org/web/20200828042838/http://mlton.org/ |dead-url=no }}</ref>。
* ML Kit<ref>[http://elsman.com/mlkit/ ML Kit]{{Wayback|url=http://elsman.com/mlkit/ |date=20181128041300 }}</ref>，由[[爱丁堡大学]]的{{le|Mads Tofte}}等人在1989年发起开发<ref>{{cite web|title=The ML Kit, Version 1|author=Lars Birkedal, Nick Rothwell, Mads Tofte, David N. Turner|year=1993|url=http://www.cs.cmu.edu/afs/cs/user/birkedal/pub/kit.ps.gz|access-date=2021-10-19|archive-date=2021-09-13|archive-url=https://web.archive.org/web/20210913210520/http://www.cs.cmu.edu/afs/cs/user/birkedal/pub/kit.ps.gz}}</ref>，是一个非常紧密的基于了标准定义的实现，它集成了具有{{le|基于区域内存管理|region-based memory management}}的垃圾收集器，内存分配指令由编译器推论，可以停用垃圾收集器来支持实时应用。
* Poly/ML<ref>[http://www.polyml.org/ Poly/ML]{{Wayback|url=http://www.polyml.org/ |date=20200627155901 }}</ref>，由[[剑桥大学]]的David Matthews开发<ref>{{cite web|author=David Matthews|title=An Implementation of Standard ML in Poly|url=http://citeseerx.ist.psu.edu/viewdoc/download;jsessionid=A7ADF150EB892580DB649F721D2A34D3?doi=10.1.1.34.7412&rep=rep1&type=pdf|year=1986|access-date=2021-10-19|archive-date=2021-10-26|archive-url=https://web.archive.org/web/20211026142801/http://citeseerx.ist.psu.edu/viewdoc/download;jsessionid%3DA7ADF150EB892580DB649F721D2A34D3%3Fdoi%3D10.1.1.34.7412%26rep%3Drep1%26type%3Dpdf}}</ref>，是一个Standard ML的完全的实现，它产生快速代码并支持多核硬件（通过Posix线程）；它的运行时间系统，进行并行垃圾收集和不可变子结构的在线共享。
* HaMLet<ref>[http://www.mpi-sws.org/~rossberg/hamlet/ HaMLet]{{Wayback|url=http://www.mpi-sws.org/~rossberg/hamlet/ |date=20161014055807 }}</ref>，由{{le|马克斯·普朗克软件系统研究所|Max Planck Institute for Software Systems|MPI-SWS}}的Andreas Rossberg编写，是一个SML解释器，意图成为精确且无障碍的标准定义参考实现。
* Moscow ML<ref>{{Cite web |url=https://mosml.org/ |title=Moscow ML |access-date=2021-09-02 |archive-date=2022-02-12 |archive-url=https://web.archive.org/web/20220212082404/https://mosml.org/ }}</ref>，是一个轻量级实现，基于了[[Caml|CAML Light]]运行时引擎。
*LunarML，产生[[Lua]]/[[JavaScript]]代码的Standard ML编译器<ref>{{cite web|url=https://github.com/minoki/LunarML|title=LunarML — The Standard ML compiler that produces Lua/JavaScript|access-date=2024-02-23|archive-date=2024-05-25|archive-url=https://web.archive.org/web/20240525011457/https://github.com/minoki/LunarML|dead-url=no}}</ref>。
'''派生'''：
* SML#<ref>[http://www.pllab.riec.tohoku.ac.jp/smlsharp/ SML#]{{Wayback|url=http://www.pllab.riec.tohoku.ac.jp/smlsharp/ |date=20200608121802 }}</ref>，是日本[[东北大学 (日本)|东北大学]]{{le|电气通信研究所|Research Institute of Electronic Communication}}开发的SML家族新语言，提供了记录多态性和C语言互操作性。它是常规的本机编译器，名字的“#”号不暗示着要在.NET框架上运行。
* {{le|Alice (编程语言)|Alice (programming language)|Alice}}，Alice ML是[[萨尔兰大学]]开发的基于Standard ML的函数式编程语言，它增加了[[惰性求值]]、[[并发性]]（[[线程|多线程]]和通过[[远程过程调用]]的[[分布式计算]]）和[[约束编程]]特征。
* SOSML<ref>[https://github.com/SOSML/SOSML SOSML]{{Wayback|url=https://github.com/SOSML/SOSML |date=20200912182745 }}</ref>，是用[[TypeScript]]写的SML实现，可以直接运行在web浏览器内。它实现了大多数SML语言和选择的部份SML基本库。
'''研究'''：
* Isabelle/ML，[[剑桥大学]]的{{le|Larry Paulson}}开发的[[Isabelle]]，将并行Poly/ML集成入交互式定理证明器<ref>[http://isabelle.in.tum.de Isabelle]{{Wayback|url=http://isabelle.in.tum.de/ |date=20200830080049 }}</ref>，它具有一个高端的IDE（基于了[[jEdit]]），用于官方Standard ML（SML'97）、Isabelle/ML方言和这个证明语言<ref>{{cite web|url=https://isabelle.in.tum.de/dist/Isabelle2021/doc/implementation.pdf|title=The Isabelle/Isar Implementation|quote=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.|access-date=2021-09-01|archive-date=2021-09-01|archive-url=https://web.archive.org/web/20210901125610/https://isabelle.in.tum.de/dist/Isabelle2021/doc/implementation.pdf}}</ref>。开始于Isabelle2016，它还有一个源代码级的ML的调试器。
* CakeML<ref>[https://cakeml.org/ CakeML]{{Wayback|url=https://cakeml.org/ |date=20200914221734 }}</ref>，是一个基于了SML实质性子集的语言，它实现为x86-64机器码的[[读取﹣求值﹣输出循环|REPL]]，带有正式验证的运行时间库和到汇编代码的转换。
* TILT<ref>[https://github.com/RobertHarper/TILT-Compiler TILT]{{Wayback|url=https://github.com/RobertHarper/TILT-Compiler |date=20180611034059 }}</ref>，是一个完全验证了的SML编译器，它使用有类型的中间语言来优化代码和确保正确性，并可以编译成{{le|有类型的汇编语言|Typed assembly language}}。
* {{le|Poplog|Poplog}}系统实现一个版本的SML，还有{{le|POP-11|POP-11}}、可选的[[Common Lisp]]和[[Prolog]]，允许混合语言编程。
所有这些实现都是[[开源软件|开源]]的并可自由的获得。其中多数用SML实现了自身。不再有任何商业SML实现。

==使用SML的项目==
证明辅助器{{le|HOL|HOL (proof assistant)|HOL4}}、[[Isabelle]]、{{le|LEGO (证明辅助器)|LEGO (proof assistant)|LEGO}}和{{le|Twelf}}是用Standard ML写成。它还用于[[编译器]]制作和[[集成电路设计]]比如[[ARM架构|ARM]]<ref>{{cite conference|author1=Jade Alglave|author2=Anthony C. J. Fox|author3=Samin Ishtiaq|author4=Magnus O. Myreen|author5=Susmit Sarkar|author6=Peter Sewell|author7=Francesco Zappa Nardelli|title=The Semantics of Power and ARM Multiprocessor Machine Code|conference=DAMP 2009|pages=13–24|url=http://www0.cs.ucl.ac.uk/staff/j.alglave/papers/damp09.pdf|access-date=2021-08-31|archive-date=2020-09-19|archive-url=https://web.archive.org/web/20200919000247/http://www0.cs.ucl.ac.uk/staff/j.alglave/papers/damp09.pdf}}</ref>。

==参见==
* [[OCaml]]
* [[F♯|F#]]

==引用==

{{reflist|2}}

==外部链接==
* [http://sml-family.org Standard ML Family GitHub Project]{{Wayback|url=http://sml-family.org/ |date=20200220023435 }}
* [https://www.cs.cmu.edu/~rwh/isml/book.pdf Programming in Standard ML]{{Wayback|url=https://www.cs.cmu.edu/~rwh/isml/book.pdf |date=20200215062548 }}
* [https://github.com/standardml/cmlib cmlib － A basic library of algorithms and data structures (a la NJlib)] {{Wayback|url=https://github.com/standardml/cmlib |date=20220502085911 }}
* [https://smlhelp.github.io/book/ SML Help] {{Wayback|url=https://smlhelp.github.io/book/ |date=20210915034530 }}
* [https://github.com/i4ki/awesome-sml Awesome Standard ML] {{Wayback|url=https://github.com/i4ki/awesome-sml |date=20211113135129 }}
* [http://www.dcs.ed.ac.uk/home/stg/NOTES/notes.html Programming in Standard ML '97: An On-line Tutorial]{{Wayback|url=http://www.dcs.ed.ac.uk/home/stg/NOTES/notes.html |date=20090522130025 }}
* [http://courses.cs.washington.edu/courses/cse341/13sp/ CSE341: Programming Languages]{{Wayback|url=http://courses.cs.washington.edu/courses/cse341/13sp/ |date=20131001123612 }}, Dan Grossman, University of Washington.
* [https://www.cs.tufts.edu/comp/105-2020f/readings/ml.html COMP 105 pages: Learning Standard ML] {{Wayback|url=https://www.cs.tufts.edu/comp/105-2020f/readings/ml.html |date=20211028183847 }}

{{程序设计语言}}
[[Category:ML語言家族]]
[[Category:函数式编程语言]]
[[Category:1990年建立的程式語言]]

Standard ML - 版本历史

imported>ExultantEditor 来自 2025年12月26日 (五) 16:36