For faster navigation, this Iframe is preloading the Wikiwand page for Standard ML.

Standard ML

维基百科,自由的百科全书

Standard ML
编程范型多范型函数式, 指令式, 模块化[1]
语言家族ML
发行时间1983年,​39年前​(1983[2]
稳定版本
Standard ML '97[3]
(1997年,​25年前​(1997
型态系统类型推论, 静态, 强类型
文件扩展名.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[4], Rust, Scala

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

Standard ML是ML的现代方言,ML是用于LCF英语Logic for Computable Functions(可计算函数逻辑)定理证明计划的编程语言。Standard ML在广泛使用的语言之中与众不同,源于它具有正式规定《The Definition of Standard ML》 [3],给出了语言的类型规则英语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运行时引擎。

派生

研究

  • 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 LispProlog,允许混合语言编程。

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

使用SML的项目

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

参见

引用

  1. ^ 1.0 1.1 David MacQueen. Modules for Standard ML. 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. An Implementation of Standard ML Modules. 1988 [2021-09-03]. (原始内容存档于2021-09-03). 
  2. ^ Robin Milner. A Proposal for Standard ML (PDF). 1983 [2021-09-02]. (原始内容 (PDF)存档于2021-11-06). 
    Robin Milner, Robert Harper, David B. MacQueen. Standard ML: Report ECS-LFCS-86-2 (PDF). 1986 [2021-09-02]. (原始内容 (PDF)存档于2021-09-02).  School of Informatics Laboratory for Foundations of Computer Science, Edinburgh University.
  3. ^ 3.0 3.1 Milner, Robin; Tofte, Mads; Harper, Robert; MacQueen, David. The Definition of Standard ML (Revised) (PDF). MIT Press. 1997 [2021-09-01]. ISBN 0-262-63181-4. (原始内容 (PDF)存档于2022-03-09). 
  4. ^ itertools — Functions creating iterators for efficient looping — Python 3.7.1rc1 documentation. docs.python.org. [2020-04-25]. (原始内容存档于2020-06-14). 
  5. ^ Damas, Luis; Milner, Robin. Principal type-schemes for functional programs (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. Type Assignment in Programming Languages (PDF) (PhD论文). University of Edinburgh. 1985 [2021-09-02]. hdl:1842/13555. CST-33-85. (原始内容 (PDF)存档于2020-01-28). 
  6. ^ Cardelli, Luca. Type Systems (PDF). ACM Computing Surveys. March 1996, 28 (1): 263–264 [2021-09-01]. doi:10.1145/234313.234418. (原始内容 (PDF)存档于2020-11-09). 
  7. ^ smlnj.org. [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. The ML Kit, Version 1. 1993 [2021-10-19]. (原始内容存档于2021-09-13). 
  11. ^ Poly/ML页面存档备份,存于互联网档案馆
  12. ^ David Matthews. An Implementation of Standard ML in Poly. 1986 [2021-10-19]. (原始内容存档于2021-10-26). 
  13. ^ HaMLet页面存档备份,存于互联网档案馆
  14. ^ Moscow ML. [2021-09-02]. (原始内容存档于2022-02-12). 
  15. ^ SML#页面存档备份,存于互联网档案馆
  16. ^ SOSML页面存档备份,存于互联网档案馆
  17. ^ Isabelle页面存档备份,存于互联网档案馆
  18. ^ The Isabelle/Isar Implementation (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. The Semantics of Power and ARM Multiprocessor Machine Code (PDF). DAMP 2009: 13–24. [2021-08-31]. (原始内容 (PDF)存档于2020-09-19). 

外部链接

{{bottomLinkPreText}} {{bottomLinkText}}
Standard ML
Listen to this article

This browser is not supported by Wikiwand :(
Wikiwand requires a browser with modern capabilities in order to provide you with the best reading experience.
Please download and use one of the following browsers:

This article was just edited, click to reload
This article has been deleted on Wikipedia (Why?)

Back to homepage

Please click Add in the dialog above
Please click Allow in the top-left corner,
then click Install Now in the dialog
Please click Open in the download dialog,
then click Install
Please click the "Downloads" icon in the Safari toolbar, open the first download in the list,
then click Install
{{::$root.activation.text}}

Install Wikiwand

Install on Chrome Install on Firefox
Don't forget to rate us

Tell your friends about Wikiwand!

Gmail Facebook Twitter Link

Enjoying Wikiwand?

Tell your friends and spread the love:
Share on Gmail Share on Facebook Share on Twitter Share on Buffer

Our magic isn't perfect

You can help our automatic cover photo selection by reporting an unsuitable photo.

This photo is visually disturbing This photo is not a good choice

Thank you for helping!


Your input will affect cover photo selection, along with input from other users.