Remove ads
Standard ML（SML），是一個函數式、指令式、模塊化[1]的通用的程式語言，具有編譯時間類型檢查和類型推論[5]。它流行於編譯器作者和程式語言研究者和自動定理證明研究者之中。
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實現。
Remove ads
證明輔助器HOL4、Isabelle、LEGO和Twelf是用Standard ML寫成。它還用於編譯器製作和集成電路設計比如ARM[22]。
Wikiwand in your browser!
Seamless Wikipedia browsing. On steroids.
Every time you click a link to Wikipedia, Wiktionary or Wikiquote in your browser's search results, it will show the modern Wikiwand interface.
Wikiwand extension is a five stars, simple, with minimum permission required to keep your browsing private, safe and transparent.
Remove ads