Standard ML
Standard ML（SML），是一個函數式、指令式、模塊化[1]的通用的程式語言，具有編譯時間類型檢查和類型推論[5]。它流行於編譯器作者和程式語言研究者和自動定理證明研究者之中。
| 編程範型 | 多范型：函數式, 指令式, 模塊化[1] |
|---|---|
| 語言家族 | ML |
| 面市時間 | 1983年[2] |
| 型態系統 | 類型推論, 靜態, 強類型 |
| 文件擴展名 | .sml |
| 網站 | Standard ML Family GitHub Project |
| 主要實作產品 | |
| SML/NJ, MLton | |
| 衍生副語言 | |
| Concurrent ML, Dependent ML, Alice | |
| 啟發語言 | |
| ML, Hope, Pascal | |
| 影響語言 | |
| ATS, Elm, F#, F*, Haskell, OCaml, Python[3], Rust, Scala | |
Standard ML是ML的現代方言，ML是用於LCF（可計算函數邏輯）定理證明計劃的程式語言。Standard ML在廣泛使用的語言之中與眾不同，源於它具有正式規定《The Definition of Standard ML》 [4]，給出了語言的類型規則和操作語義[6]。
實現
存在很多SML實現，包括：
標準：
- Standard ML of New Jersey（縮寫為SML/NJ），由普林斯頓大學和貝爾實驗室在1986年開始聯合開發的實現，是一個完全的編譯器，具有關聯的庫、工具、交互式外殼和文檔，還支持Concurrent ML[7]。
- MLton，是一個全程序優化編譯器，它產生相比其他ML實現非常快的代碼[8]。
- ML Kit[9]，由愛丁堡大學的Mads Tofte等人在1989年發起開發[10]，是一個非常緊密的基於了標準定義的實現，它集成了具有基於區域內存管理的垃圾收集器，內存分配指令由編譯器推論，可以停用垃圾收集器來支持實時應用。
- Poly/ML[11]，由劍橋大學的David Matthews開發[12]，是一個Standard ML的完全的實現，它產生快速代碼並支持多核硬體（通過Posix執行緒）；它的運行時間系統，進行並行垃圾收集和不可變子結構的在線共享。
- HaMLet[13]，由MPI-SWS的Andreas Rossberg編寫，是一個SML解釋器，意圖成為精確且便宜的標準定義參考實現。
- Moscow ML[14]，是一個輕量級實現，基於了CAML Light運行時引擎。
- LunarML，產生Lua/JavaScript代碼的Standard ML編譯器[15]。
派生：
- SML#[16]，是日本東北大學電氣通信研究所開發的SML家族新語言，提供了記錄多態性和C語言互操作性。它是常規的本機編譯器，名字的「#」號不暗示著要在.NET框架上運行。
- Alice，Alice ML是薩爾蘭大學開發的基於Standard ML的函數式程式語言，它增加了惰性求值、並發性（多執行緒和通過遠程過程調用的分布式計算）和約束編程特徵。
- SOSML[17]，是用TypeScript寫的SML實現，可以直接運行在web瀏覽器內。它實現了大多數SML語言和選擇的部份SML基本庫。
研究：
- Isabelle/ML，劍橋大學的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編譯器，它使用有類型的中間語言來優化代碼和確保正確性，並可以編譯成有類型的彙編語言。
- Poplog系統實現一個版本的SML，還有POP-11、可選的Common Lisp和Prolog，允許混合語言編程。
所有這些實現都是開源的並可自由的獲得。其中多數用SML實現了自身。不再有任何商業SML實現。
使用SML的項目
證明輔助器HOL4、Isabelle、LEGO和Twelf是用Standard ML寫成。它還用於編譯器製作和集成電路設計比如ARM[22]。
參見
引用
- ^ 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）. - ^ 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. - ^ itertools — Functions creating iterators for efficient looping — Python 3.7.1rc1 documentation. docs.python.org. [2020-04-25]. （原始內容存檔於2020-06-14）.
- ^ 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）.
- ^ 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）. - ^ 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）.
- ^ smlnj.org. [2020-04-25]. （原始內容存檔於2020-05-01）.
- ^ mlton.org. [2020-09-27]. （原始內容存檔於2020-08-28）.
- ^ ML Kit（頁面存檔備份，存於網際網路檔案館）
- ^ Lars Birkedal, Nick Rothwell, Mads Tofte, David N. Turner. The ML Kit, Version 1. 1993 [2021-10-19]. （原始內容存檔於2021-09-13）.
- ^ Poly/ML（頁面存檔備份，存於網際網路檔案館）
- ^ David Matthews. An Implementation of Standard ML in Poly. 1986 [2021-10-19]. （原始內容存檔於2021-10-26）.
- ^ HaMLet（頁面存檔備份，存於網際網路檔案館）
- ^ Moscow ML. [2021-09-02]. （原始內容存檔於2022-02-12）.
- ^ LunarML — The Standard ML compiler that produces Lua/JavaScript. [2024-02-23]. （原始內容存檔於2024-05-25）.
- ^ SML#（頁面存檔備份，存於網際網路檔案館）
- ^ SOSML（頁面存檔備份，存於網際網路檔案館）
- ^ Isabelle（頁面存檔備份，存於網際網路檔案館）
- ^ 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.
- ^ CakeML（頁面存檔備份，存於網際網路檔案館）
- ^ TILT（頁面存檔備份，存於網際網路檔案館）
- ^ 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）.
外部連結
- 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 （頁面存檔備份，存於網際網路檔案館）