Standard ML

Standard MLSML),是一個函數式指令式模塊化[1]通用程式語言,具有編譯時間類型檢查類型推論[5]。它流行於編譯器作者和程式語言研究者和自動定理證明研究者之中。

Standard ML
編程範型多范型函數式, 指令式, 模塊化[1]
語言家族ML
面市時間1983年,​41年前​(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實現,包括:

標準

派生

研究

  • Isabelle/ML,劍橋大學Larry Paulson英語Larry Paulson開發的Isabelle,將並行Poly/ML集成入交互式定理證明器[18],它具有一個高端的IDE(基於了jEdit),用於官方Standard ML(SML'97)、Isabelle/ML方言和這個證明語言[19]。開始於Isabelle2016,它還有一個原始碼級的ML的調試器。
  • CakeML[20],是一個基於了SML實質性子集的語言,它實現為x86-64機器碼的REPL,帶有正式驗證的運行時間庫和到彙編代碼的轉換。
  • TILT[21],是一個完全驗證了的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[22]

參見

引用

  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. ^ itertools — Functions creating iterators for efficient looping — Python 3.7.1rc1 documentation. docs.python.org. [2020-04-25]. (原始內容存檔於2020-06-14). 
  4. ^ 4.0 4.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). 
  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. ^ LunarML — The Standard ML compiler that produces Lua/JavaScript. [2024-02-23]. (原始內容存檔於2024-05-25). 
  16. ^ SML#頁面存檔備份,存於網際網路檔案館
  17. ^ SOSML頁面存檔備份,存於網際網路檔案館
  18. ^ Isabelle頁面存檔備份,存於網際網路檔案館
  19. ^ 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. 
  20. ^ CakeML頁面存檔備份,存於網際網路檔案館
  21. ^ TILT頁面存檔備份,存於網際網路檔案館
  22. ^ 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). 

外部連結