跳至內容

「ML語言」:修訂間差異

出自Taiwan Tongues 台語維基
TaiwanTonguesApiRobot留言 | 貢獻
從 JSON 檔案批量匯入
 
(無差異)

於 2025年8月23日 (六) 00:06 的最新修訂

MLMetaLanguage:元語言), 是一个函數式、指令式的通用的程式語言,伊講的佇使用多態的 Hindley–Milner 類型推論。ML 會當自動的指定多數表達式的類型,無要求顯式的類型標註,而且會當確保類型安全,已經正式證明矣有良好類型的 ML 程序袂致使運行時間類型錯誤。

ML 提供了對函數實際參數的模式匹配、糞埽回收、指令式編程、傳值的調用佮柯里化。伊予大量的用佇咧程式語言研究內底,並且是全面規定了和使用形式語義驗證了的少數語言之一。伊的類型佮模式匹配予伊非常適合併而且定定用佇其他的形式語言進行操作,譬如講咧編譯器構造、自動化定理證明佮形式驗證中。

歷史

佇一九七空年代早期,ML 由愛丁堡大學的羅賓 ・ 米爾納佮別人研製出來,用於在 LCF 定理證明器中開發證明策略。LCF 的語言是「PPλ」,伊是一階邏輯演算有類型的多態 λ 演算的結合,以 ML 做元語言。ML 的語法對 ISWIM 佮擴展實現 PAL 得著啟發,LCF ML 運行佇咧 DEC 鋪十 / TOPS 鋪十主機的 Stanford LISP 一孵六下。

佇一九八O年,Luca Cardelli 佇愛丁堡大學的 VAX / VMS 系統上開發矣 ML 編譯器,伊予人叫做「VAX ML」,以區別於 LCF 版本的「DEC 鋪十 ML」。 VAX ML 的編譯器佮運行的時間系統二者,攏是用 Pascal 書寫佇建立佇「函數抽象的機器」(FAM)之上。佇咧一九八二年,愛丁堡大學的 Kevin Mitchell,用 VAX ML 重寫矣 VAX ML 編譯器,隨即 John Scott 和 Alan Mycroft 加入去開發,佇咧閣進行一系列重寫改進了後,新的編譯器予人號做「Edinburgh ML」。

佇一九八一年,INRIA 的 Gérard Huet,共上蓋起初的 LCF ML 適配著 Multics 系統的 Maclisp 落,並且增加編譯器。這个實現予人講是 INRIA 內部文檔「ML 手冊」之中,伊予開發者自稱做「Le \ _ ML」。 劍橋大學的 Lawrence Paulson 用伊開發矣基於 Franz Lisp 的 Cambridge LCF,行抑若劍橋大學的 Michael J . C . Gordon 閣用伊開發矣基於 Common Lisp 的頭一版的 HOL。

佇一九八三年,Robin Milner 由兩个動機驅使開始重新設計 ML。其實是愛丁堡大學的 Rod Burstall 佮其實小組佇咧規定頂懸的工課,具體化做規定語言 CLEAR,和表達會當執行規定的函數式語言 HOPE。這項工課佮 ML 有關係的是兩方面成果:首先,HOPE 有優雅的編程特徵,特別是模式匹配,佮子句式函數定義;其次,是使用伊咧接口中的簽名,進行規定的模塊化構造的想法。其二是 Luca Cardelli 佇咧 VAX ML 上的工課,通過增加號名的記錄佮可變類型,展出來矣 ML 中數據類型的品目。

佇咧一九八四年,貝爾實驗室的 David MacQueen 提出著 Standard ML 的模塊系統的設計。佇咧 Standard ML 的繼續設計期間,Edinburgh ML 去予漸漸進的修改,充當矣 Standard ML 的近似原型實現。佇一九八六年,普林斯頓大學的 Andrew Appel 佮貝爾實驗室的 David MacQueen,以 Edinburgh Standard ML 做起步開發環境,開始矣專注射生成高質量機器代碼的 Standard ML of New Jersey 的活跳跳。

佇一九九O年,Robin Milner、Mads Tofte 和 Robert Harper 制定的 Standard ML 的正式的規定《The Definition of Standard ML》終其尾完成;佇一九九七年,這个標準規定是增補 David MacQueen 為作者並進行了修訂。佇一九八九年,Mads Tofte、Nick Rothwell 和 David N . Turner 佇愛丁堡大學開始開發 ML Kit 編譯器,為著強調度清楚有夠懸效,將標準定義直接轉譯做一組 Standard ML 模塊;佇一九九二年佮一九九三年期間,主要通過愛丁堡大學的 Nick Rothwell 佮哥本哈根大學計算機科學系(DIKU)的 Lars Birkedal 的工課,ML Kit 頭一版完成並開源發行。

佇一九八七年,INRIA 的 Ascánder Suárez,基於巴黎第七大學的 Guy Cousineau 的「範圍抽象機器」(CAM), 利用 Le Lisp 的運行時間系統重新實現矣 Le \ _ ML,並正式號名 Caml。佇一九九O年佮一九九一年,INRIA 的 Xavier Leroy 是用來的 C 實現的字節碼解說器,利用 Damien Doligez 提供的內存管理系統重新實現矣 Caml,並講的其實 Caml Light。佇一九九五年,Xavier Leroy 閣增加機器代碼編譯器佮高層模塊系統,這个版本嘛叫做是「Caml Special Light」。 佇咧一九九六年,INRIA 的 Didier Rémy 和 Jérôme Vouillon,向 Caml Special Light 增加物件導向特徵,對而且形成矣 OCaml。

今仔日 ML 家族的兩个主要的方言是 Standard ML 和 OCaml。ML 的實力真濟予人用佇語言設計佮操作,譬如講建構編譯器、分析器、定理證明器,但是伊做為通用語言嘛予人用佇生物信息佮財務系統等等領域。ML 確立了靜態類型函數式編程范型,對佇咧程式語言歷史上占有顯愛地位,伊的思想佇咧影響足濟的語言,比如講 Haskell、Nemerle、ATS 和 Elm。

解說佮編譯

ML 代碼片真容易通過共錄入到「頂層」來研習,伊嘛叫做讀取 ﹣ 求值 ﹣ 輸出循環抑是 REPL。這是列印結果抑是定義的表達式的推論類型的交互式會話。足濟的 SML 實現提供交互式 REPL,比如講 SML / NJ:

會當咧提示符仔 `-` 後鍵入代碼。譬如講計算 ` 一 + 二 * 三 ` :

頂層推論這个表達式的類型 ` int ` 並且共出結果 ` 七 `。若輸入無完全是列印第二提示符 `=`,這个時陣定定會當用 ` ; ` 終結輸入。` it ` 是予無指定變量的表達式的標準變量。輸入 control-C 會當回解說器頂層,輸入 control-D 會當退出解說器。

下跤是 hello , world ! 的程序代碼佇咧 SML / NJ 解說器下執行的結果:

佮使用 MLton 編譯器進行編譯執行的例:

核心語言

和尚純函數式編程語言,ML 是兼具一寡指令式特徵的函數式編程語言。ML 的特徵包括講:傳值調用的求值策略,頭等函數,帶有糞埽收集的自動內存管理,參數多態,靜態類型,類型推論,代數據類型,模式匹配佮異常處理。無仝 Haskell,ML 佮大多數程式語言平平使用佮早求值。

用 ML 書寫的程序構成自要被求值的表達式,毋是語句抑是命令,就算一寡表達式倒轉來一个平凡的 ` unit ` 並且干焦其副作用而且求值。以下章節介紹採用 Standard ML 的語法佮語義。

函數

袂輸所有的函數式的語言仝款,ML 的關鍵特徵是函數,伊予人用佇咧進行抽象。譬如講階乘函數用純 ML 會當表達為:

遮將階乘描述做遞歸函數,有一个單一的終止基礎狀況。伊類似佇數學教科書見著的階乘描述。多數 ML 代碼咧設施佮語法頂懸類似數學。

憑藉類型推論編譯器能推導出,` fac ` 接受整數 ` 零 ` 成做實際的參數,則形式參數 ` n ` 嘛是整數類型 ` int `,而且 ` fac 零 ` 的結果是整數 ` 一 `,則函數 ` fac ` 的結果嘛是整數類型。函數 ` fac ` 接受一个整數的形式參數閣倒轉來一个整數結果,伊做一个整體對而有著「對整數到整數的函數」類型 ` int-> int `。函數佮其形式參數的 " 類型 " 猶閣會當用類型標註(annotation)來講,使用 ` E  : t ` 表示法,伊會當讀做表達式 ` E ` 有類型 ` t `,伊是可選嘛會當忽略的。使用類型標準註,這比如講這字會當重寫為下:

這个函數猶閣靠模式匹配,這是 ML 語言的重要部份。注意函數形式參數毋免佇圓括號內但愛用空格來分隔。做一个函數的實際參數是 ` 零 `,伊共回回整數 ` 一 `。對所有其他的狀況,試看覓仔第二途。彼是一个遞歸,而且再次執行這個函數直到達到基礎的狀況。伊會當使用 ` case ` 表達式重寫為:

遮 ` case ` 介入模式佮對應表達式的序列。伊閣會當重寫做將標識符仔縛定甲 lambda 函數:

遮的關鍵字 ` val ` 介入了標識符合著值的縛定,` fn ` 介入了匿名函數的定義,伊會當用佇咧 ` fun ` 的位置頂懸,毋過使用 `=> ` 算符而非 `=`。縛定到遞歸的匿名函數需要使用 ` rec ` 關鍵字來指示。

通過將主要的工課寫入尾遞歸咱風格的內部迵天代函數,對語言編譯抑是解說系統進行的尾調用優化,這个函數會當增進性能,伊的調用棧毋免隨函數調用數目來做比例的增加長。著這个函數會當採用向內部函數增加額外的「累加器」形式參數 ` acc ` 來實現:

` let ` 表達式的值是佇咧 ` in ` 和 ` end ` 之間表達式的值。這个遞歸函數的實現無保證會當終止,因為負數實際參數會致使遞歸調用的不窮降鏈條件。閣較勇健的實現會佇咧遞歸前檢查實際參數為非負數,並且佇有問題的狀況,即 ` n ` 是負數的時陣,啟用異常處理:

類型

有一寡基本的類型會當做是「內建」的,因為𪜶是咧 Standard ML 標準基本庫內底預先定義的,並且語言為𪜶提供文字的表示法,比如講 ` 三十四 ` 是整數,而且 ` " 三十四 " ` 是字符合。一寡上蓋捷用的基本的類型是:

  • ` int ` 整數,比如講 ` 三 ` 抑是 ` ~ 十二 `。注意波浪號 ~ 表示負號。
  • ` real ` 浮點數,比如講 ` 四配二 ` 抑是 ` ~ 六桱四 `。Standard ML 無隱含的提升整數做浮點數,因此表達式 ` 二 + 五鋪六七 ` 是無效的。
  • ` string ` 字符串,比如講 ` " this is a string " ` 抑是 ` " " `(空串)。
  • ` char ` 字符,比如講 ` # " y " ` 抑是 ` # " \ n " `(換行符)。
  • ` bool ` 布爾值,伊是欲按怎 ` true ` 欲按怎 ` false `。產生 ` bool ` 值的有較算符 `=`、` < > `、` > `、` >=`、` < `、` <=`,邏輯函數 ` not ` 佮行短路求值的中綴算符 ` andalso `、` orelse `。

包括上述基本類型的各種類型會當用多種方式組合。一種方式是元組,伊是值的有序集合,比如表達式 ` ( 一 , 二 ) ` 的類型是 ` int * int `,而且 ` ( " foo " , false ) ` 的類型是 ` string * bool `。會用得使用 ` # 一 ( " foo " , false ) ` 這款的語法來提元組的指定次序的成員。

有零元組 ` ( ) `,伊的類型指示為 ` unit `。但是無一箍組,抑是講佇咧例 ` ( 一 ) ` 和 ` 一 ` 之間無分別,攏有類型 ` int `。元組會當1875套,` ( 一 , 二 , 三 ) ` 無仝 ` ( ( 一 , 二 ) , 三 ) ` 和 ` ( 一 , ( 二 , 三 ) ) ` 二者。前者的類型是 ` int * int * int `,其他兩个的類型分別是 ` ( int * int ) * int ` 和 ` int * ( int * int ) `。

組合值的另外一種方式是記錄。記錄足成元組的,除了伊的成員是有名的毋是假的,比如講 ` { a=五曉空 , b=" five " } ` 有類型 ` { a  : real , b  : string } `,這佮類型仝類型 ` { b  : string , a  : real } `。會用得使用 ` # a { a=五曉空 , b=" five " } ` 這款的語法來選取記錄的指定名的欄位。Standard ML 中的函數隻接受一个值作為參數,毋是參數的一个列表,會當使用上述元組模式匹配來實際上傳達多個參數。函數閣會當倒轉來一个元組。比如講:

遮第一段創建了兩个類型是 ` int * int-> int ` 的函數 ` sum ` 和 ` average `。第二段創建中綴算子 ` averaged _ with `,紲落來定義伊是類型 ` int * int-> int ` 的函數。最後的 ` int _ pair ` 函數的類型是 ` int-> int * int `。

下列函數是多態類型的一个例:

編譯器無法度推論出的 ` pair ` 的特殊化去的類型,伊會當是 ` int-> int * int `、` real-> real * real ` 甚至講 ` ( int * real-> string )-> ( int * real-> string ) * ( int * real-> string ) `。佇咧 Standard ML 中,伊會當簡單指定做多態類型 `'a->'a *'a `,遮的 `'a `(讀作「alpha」)是一个類型變量,指示任何可能的類型。咧寫定義下,` pair 三 ` 和 ` pair " x " ` 攏是有良好定義的,分別產生 ` ( 三 , 三 ) ` 和 ` ( " x " , " x " ) `。

SML 標準基本庫包括了重載標識符:` + `、`-`、` * `、` div `、` mod `、` / `、` ~ `、` abs `、` < `、` > `、` <=`、` >=`。標準基本庫提供多態的函數:` ! `、` :=`、` o `、` before `、` ignore `。妝娗的算符會使有對伊上低 ` 零 ` 到上懸 ` 九 ` 的任何運算符優先級。標準基本庫提供了如下內建中綴著規定:

等式類型

算符 `=` 和 ` < > ` 分別被定義為多態的等式佮不等式。`=` 伊確定兩个值是毋是相等,有類型 `a *a-> bool `。這意味著伊的兩个運算數著愛有仝款的類型,這个型著愛是等式類型(` eqtype `)。 欲講基本的類型內底除了 ` real ` 以外,` int `、` real `、` string `、` char ` 和 ` bool ` 攏是等式類型。

比如講:` 三=三 `、` " 三 "=" 三 " `、` # " 三 "=# " 三 " ` 和 ` true=true `,攏是有效的表達式並求值為 ` true `;而且 ` 三=四 ` 是有效表達式並求值為 ` false `,` 三-c零=三-c零 ` 是無效的表達式被編譯器拒絕。這是因為 IEEE 浮點數等式拍破去 ML 中對等式的一寡要求。特別是 ` nan ` 無等於家己,所以關係毋是自反的。

元組佮記錄類型是等式類型,彼當陣而且干焦做伊的逐个成員類型是等式類型;比如講 ` int * string `、` { b  : bool , c  : char } ` 和 ` unit ` 是等式類型,而且 ` int * real ` 和 ` { x  : real } ` 毋是呢。函數類型永遠毋是等式類型,因為一般這情況下無可能確定兩个函數敢是等價。

類型聲明

類型聲明抑是同義詞(synonym)使用 ` type ` 關鍵字來定義。下跤是予佇咧平面當中的點的類型聲明,計算兩點間距離,佮通過海倫公式計算予定角點的三角形的面積的函數。

數據類型

Standard ML 提供了對代數據類型(ADT)的強力支持。一个 ML 數據類型會當被當做是元組的無交並(積之佮)。 數據類型使用 ` datatype ` 關鍵字來定義,比如講:

這个數據類型聲明建立一个全新的數據類型 ` int _ or _ string `,閣有做伙的新構造子(一種特殊函數抑是值)` INT `、` STRING ` 和 ` NEITHER `;每一个這種類型的值攏是愛按怎 ` INT ` 有一个整數,欲按怎 ` STRING ` 有一个字符串,欲按怎 ` NEITHER `。寫為下按呢:

遮上尾一个聲明通過模式匹配,將變量 ` j ` 縛定甲變量 ` i ` 所縛定的整數 ` 三 `。` val 模式=表現出色 ` 是縛定的一般形式,伊是良好定義的,若是唯一模式佮表達有仝款的類型。

數據類型會當是多態的:

這个數據類型聲明建立一个新的類型 `'a pair ` 家族,比如講 ` int pair `,` string pair ` 等咧。

數據類型會當是遞歸的:

這个數據類型聲明建立一个新的類型 ` int _ list `,這个型的每一个值是欲按怎 ` EMPTY `(空列表), 欲按怎是一个整數和另外一个 ` int _ list ` 的接合。

通過 ` datatype ` 創建的類型是等式類型,如果伊的所有變體,抑若無參數的空構造子,若是有等式類型參數的構造子,並且佇多態類型的情況下所有類型參數也攏是等式類型。遞歸類型佇咧有可能的情形下是等式類型,抑若無就毋是。

列表

基礎庫提供的複雜數據類型之一是列表 ` list `。伊是一个遞歸的、多態的數據類型,會當等價的定義為:

遮的 ` : : ` 是中綴著算符,比如講 ` 三   : : 四   : : 五   : : nil ` 是三个整數的列表。列表是 ML 程序當中上捷用的數據類型之一,語言閣為生做列表提供了特殊表示法 ` [三 , 四 , 五] `。

` real list ` 當然毋是等式類型。但是無 ` int list ` 袂當是等式類型的理由,所以伊就是等式類型。注意類型變量無仝就是無仝的列表類型,比如講 ` ( nil  : int list )=( nil  : char list ) ` 是無效的,因為兩个表達式有無仝的類型,就算講𪜶有仝款值。猶毋過 ` nil=nil ` 和 ` ( nil  : int list )=nil ` 攏是有效的。

基本庫 ` rev ` 函數「反轉」一个列表中的元素。伊的類型是 `'a list->'a list `,就是講伊會當接受伊的元素有任何類型的列表,閣倒轉去仝類型的列表。閣較準確實講,伊倒轉來其元素比較予定列表是反轉次序的一个新列表,比如講將 ` [" a " , " b " , " c "] ` 炤做 ` [" c " , " b " , " a "] `。著算符 ` @ ` 表示兩个列表的串接。

` rev ` 和 ` @ ` 一般被實現做基本庫函數 ` revAppend ` 的簡單應用:

模式匹配

Standard ML 的數據類型會當輕易的定義佮用於編程,佇足大的程度上是由伊的模式匹配,猶閣有多數 Standard ML 實現的模式散赤盡性檢查佮模式趁錢檢查。

模式匹配會當佇語法頂懸去予二空變的量縛定之中,比如講:

第一啦 ` val ` 縛定了四个變量 ` m `、` n `、` r ` 和 ` s `;第二个 ` val ` 縛定一个變量 ` url `;第三个 ` val ` 縛定三个變量 ` port `、` addr ` 和 ` name `,第四个叫分層模式,縛定三个變量 ` x `、` fst ` 和 ` snd `。

模式匹配會當佇語法頂懸去予人入去函數定義內底,比如講:

次序佇模式匹配內底是誠緊的:模式按文本次序來依次進行匹配。佇咧特定計算中,使用下劃線 ` _ `,來省略無需要伊的值的子成員,這嘛叫做通配符(wildcard)模式。咱所講的「子句形式」風格的函數定義,遮的模式綴咧明明了後出來,只是形式的一種語法糖:

模式散盡性檢查會確保數據類型的每一个情形攏已經顧及著。 若是有落勾去,著愛產生警告。 若是模式有咧趁錢,也會致使一个編譯時間警告。

高階函數

函數會當接受函數作為實際參數,比如講:

函數會當產生函數作為返回值,比如講:

函數會當同時接受和產生函數,譬如講複合函數:

基本庫的函數 ` List . map `,是佇咧 Standard ML 上捷用的 Curry 化高階函數,伊佇概念頂懸會當定義為:

佇基本庫中將函數複合定義為多態中算符 ` ( f o g ) `,` map ` 和 ` fold ` 高階函數有較高效率的實現。

異常

異常會當使用 ` raise ` 關鍵字發起,閣通過模式匹配 ` handle ` 構造來處理:

遮的 ` ^ ` 是字符串接算符。會當利用異常系統來實現非局部退出,譬如講這个函數所採用技術:

異常 ` Zero ` 佇咧 ` 零 ` 狀況下發起,控制對函數 ` p ` 中做伙出離。

引用

初初的去化基礎庫閣以引用的形式提供了會當變的存儲。引用 ` ref ` 會當佇某一種意義上予人認為是如下按呢定義的:

閣定義矣內起的 ` :=` 函數來修改引用的內容,和 ` ! ` 函數來檢索引用的內容。階乘函數會當使用引用定義做指令式風格:

遮使用圓括號著以 ` ; ` 分隔的表達式進行矣順序複合。

會當變類型 `'a ref ` 是等式類型,就算講伊的成員類型毋是。兩个引用予人叫做是相等的,如果𪜶若標識仝款的「` ref ` 單元」,就是講相仝的著 ` ref ` 構造子調用生成的仝一个指針。所以 ` ( ref 一 )=( ref 一 ) ` 和 ` ( ref 一垺零 )=( ref 一垺零 ) ` 攏是有效的,並且攏求值為 ` false `,因為著算兩个引用拄好指向矣仝款的值,引用家己的是分立的,逐个攏會當獨立於其他而改變。

模塊語言

模塊是 ML 用佇咧構造大型的項目佮庫的系統。

模塊

一个模塊構成自一个簽名(signature)文件佮一个抑是幾个仔結構文件。簽名文件指定愛實現的 API(就親像 C 語言頭文件抑是 Java 承口文件)。 結構實現這个簽名(就親像 C 語言源文件抑是 Java 類文件)。 解說器通過 ` use ` 命令導入𪜶。ML 的標準庫予人實現做這種方式的模塊。

比如講,下列定義一个算術簽名:

和這个簽名使用有理數的實現:

下底是這个結構的簡單用例:

Standard ML 只允准通過簽名函數同實現進行交互,比如講袂當直接過這个代碼內底會當 ` Rat ` 來建立數據對象。結構塊對外部隱藏所有實現細節。遮的 ` : ` 叫做透明歸屬(ascription), 會當通過所縛定的變量見著這結構的數據內容,佮之相對的是 ` : > `,伊叫做無透明歸屬,此結構的數據內容對外完全無可見。比如講頂懸用例有結果:` val c=Rat ( 四 , 三 )   : Rational . t `,若改做無透明歸屬是有結果:` val c=-  : Rational . t `。

愛用有理數做實際上的數值計算,需要處理分數形式中分母快速增加予溢出整數類型的大細範圍等等的問題。

函子

函子接受指定簽名的一个結構作為參數,閣倒轉來一个結構作為結果,下跤示例的函子能佇咧 ` ARITH ` 簽名的結構頂懸算徙振動平均:

和這个函子的簡單用例:

這用例承上節示例,` Rational ` 結構採用矣透明歸屬,有結果若是:` val d=( [Rat ( 四 , 五 ) , Rat ( 二 , 三 )] , 二 , Rat ( 十一 , 十五 ) )   : MLR . t `。如果伊改做無透明歸屬,對應結果為著:` val d=( [-,-] , 二 ,-)   : MLR . t `。

示例代碼

伊比例閣較好用 Standard ML 的語法佮語義。

素數

下跤是求素數的試除法實現:

基本庫 ` find ` 和 ` exists ` 函數佇咧不存在符合條件元素的時會遍歷規个列表, 遮採用著特殊化的 ` existsDivisor `,用以後續的元素攏無滿足條件的時陣隨結束運算。

下跤是埃拉托斯特尼篩法實現:

遮是基於列表的篩法實現符合埃拉托斯特尼的原初算法。篩法猶閣有數組的直觀實現。 下跤是其解釋器下命令行運行實例:

漢明數

正規數是形若 $ \ 二 ^ { i } \ cdot 三 ^ { j } \ cdot 五 ^ { k } \ $ 的整數,對非負整數 $ \ i \ $、$ \ j \ $ 和 $ \ k $,伊是會當整除 $ \ 六十 ^ { \ max ( \ lceil i \ , / 二 \ rceil , j , k ) } \ $ 的數。計算升序的正規數的算法經由戴克斯特拉會當時行,理察 ・ 漢明上頭仔提出這个問題,故這个問題予人號做「漢明問題」,這个數列嘛予人號做漢明數。Dijkstra 計算遮的數的想法如下:

  • 漢明數的序列開始於數 ` 一 `。
  • 愛加入序列內底有啥物意思形式:` 二 h , 三 h , 五 h `,遮的 ` h ` 是序列已有的任意的漢明數。
  • 所以,會當生做上頭仔干焦一个 ` 一 ` 的序列 ` H `,並且做這个歸併序列 ` 二 H , 三 H , 五 H `,並且以這樣推。

示例漢明數程序代碼,一般就用來展示,確實計算只要時行的純函數式編程方式。

產生指定範圍內的漢明數需要多輪運算,後壁每輪中的三个列表元素乘積運算中攏有可能產生超出這个範圍的結果,𪜶無需要出現佇後續的運算中。 基本庫 ` mapPartial ` 函數佮伊所映射的函數,通過因為 ` Option ` 結構的 ` SOME ` 和 ` NONE ` 構造子的協定,會當將所映射函數認為無符合條件的元素抑是結果排除,伊會遍歷規个列表。 因為這算法採用升序列表,這搭遮共改寫做 ` mapPrefix ` 函數,用來佇咧特定條件不滿足條件就隨結束。下面是漢明數程序佇咧解說器下命令行運行實例:

續體傳遞風格實例

下面是續體傳遞風格(CPS)的高階函數 foldr 和 map 的實現,佮達成一个整數列表的合計函數的簡單用例:

對著輸入 ` [e 一 , e 二 , . . . , en] `,` sum ` 函數等價於函數複合 ` ( fn x=> x ) o ( fn x=> e 一 + x ) o ( fn x=> e 二 + x ) o . . . o ( fn x=> en + x ) `,伊應用佇咧 ` 零 ` 會上得著 ` ( e 一 + ( e 二 + ( . . . + ( en + 零 ) . . . ) ) ) `。

SML / NJ 支持頭等等的對象的續體。頭等等體對一門語言來講是會當完全控制指令執行次序的能力。𪜶會當用來跳轉來產生著當前函數調用的彼个函數,或者是跳轉來到這進前已經退出矣的函數。頭等等體保存了程序執行狀態,伊無保存程序數據,干焦保存執行上下文。

排序算法

排序算法關注算複雜度,特別是時間複雜度,基本庫函數的實現細節嘛愛考慮在內,譬如講串接函數 ` @ `,伊予人實現做 ` fun l 一 @ l 二=revAppend ( rev l 一 , l 二 ) `,除非必需的狀況避免使用遍歷規个列表的 ` rev ` 和 ` length ` 函數。 通過較佇遮的排序算法的周知過程式編程語言譬如講 C 語言的實現,會當體察著這个 ML 佇咧控制流程佮列表資料結構頂懸的相關限制,佮之相適應的採用尾遞歸的特色函數式編程風格。

插入去排序

下面是簡單的插入去排序算法的尾遞歸佮遮的價數的普通遞歸實現:

插入排序算法是穩定的自適應排序,伊佇輸入列表較正序的時陣會當最佳,佇咧輸入列表較趨勢的時陣會當上䆀,因此佇咧算法實現中,需要 ` insert ` 函數所插入列表保持做反序,佇咧插入去攏完成了後 ` rev ` 函數才閣反倒轉來正序。佇預期輸入數據時到隨機化或者是預知伊經過了反轉的狀況之下,會當採用保持愛插入去列表為正序的變體插入去排序算法實現,伊佇輸入列表較趨勢的時陣會當最佳,佇輸入列表較正序的時陣會當上䆀,伊比自適應實現少作一擺全列表反轉。 採用 ` foldr ` 函數會當相應的保持愛插入去列表為正序,因為 ` fun foldr f b l=foldl f b ( rev l ) `,伊等仝款對反轉過的列表應用變體插入去排序。

希爾排序

希爾排序算法是對插入去排序的改進,保持家己適應性,放棄了穩定性。 下面是希爾排序的實現:

遮有採用的間隔序列是 OEIS A 十二點空八千八百七十,即 $ \ { \ begin { smallmatrix } \ left \ lceil { \ frac { 一 } { 五 } } \ left ( 九 \ cdot \ left ( { \ frac { 九 } { 四 } } \ right ) ^ { k 影一 } 扳四 \ right ) \ right \ rceil \ end { smallmatrix } } \ $,伊是喬田尚之在一九九二年提出的。這个序列用遞推公式表示為:` hk=⌈h'k⌉ `,遮的 ` h'k=二嬸二五·h'k 影一 + 一 ` 而且 ` h'一=一 `。假定一个列表的長度 ` s ` 佇序列兩个元素之間,即 ` hk 影一 < hk ≤ s < hk + 一 `,若是 ` hk ≤ $ { \ tfrac { n } { m } } $·s `,遮的 ` n ≤ m `,是選擇初間隔做 ` hk `,抑無來做 ` hk 影一 `。佇這个保值之下,對無仝長度 ` s ` 的列表佮對應的初期隔 ` h `,伊每一个列表的遮的初初的時陣列表的平均長度 ` $ { \ tfrac { s } { h } } $ `,約佇咧 ` $ { \ tfrac { m } { n } } $ ≤ $ { \ tfrac { s } { h } } $ < $ { \ tfrac { 九 } { 四 } } $·$ { \ tfrac { m } { n } } $ ` 範圍內底。間隔序列閣會當採用 OEIS A 十石空二千五百四十九,伊是 Marcin Ciura 佇二空空一年通過實驗得著的。

快速排序

下跤是快速排序算法的自頂向下實現:

基本庫 ` partition ` 函數實現對快速排序來講有無必要的反轉, 遮採用著伊的簡省改寫。佇咧 ML 中快速排序應該愛採用自底向上實現:

歸併排序

下跤是歸併排序算法的自底向上法實現:

考慮輸入列表 ` [x 一 , . . . , xi , a 零 , . . . , a 九 , xj , . . . , xn] `,遮佇咧 ` xi ` 和 ` xj ` 之間的 ` 十 ` 個 ` a `,具有仝款的值並且需要保持其下標表示的次序,遮的 ` xi > a ` 並且 ` xj < a `,並且佇這个區段前後的元素總數攏會當予 ` 三 ` 整除,伊予人分解做子列表的列表 ` [Xm , . . . , [ xj , a 八 , a 九] , [a 五 , a 六 , a 七] , [a 二 , a 三 , a 四] , [a 零 , a 一 , xi] , . . . , X 一 ] `,遮有 ` m=n div 三 `;假定這 ` 四 ` 有含有 ` a ` 的子列表兩兩歸併,佇歸併正序子列表的歸併條件 ` x < y ` 落,通好著 ` [X 一 , . . . , [ xi , a 四 , . . . , a 零] , [a 九 , . . . , a 五 , xj] , . . . , Xk ] `;繼續推捒落去,佇咧歸併反序子列表的歸併條件 ` x > y ` 落,通好著 ` [Xh , . . . , [ xj , a 零 , . . . , a 九 , xi] , . . . , X 一 ] `。會當看出這種歸併操作會當保證排序算法的穩定性,即具有仝款值的元素之間的仝款對次序保持無變。

分初的子列表採用插入去排序,閣會當進一步來增加其大細。歸併排序嘛有自頂向下實現。

堆排序

下面是堆排序的是因為數組的實現:

佇數組實現中,` siftdown ` 函數融合了插入佮篩選功能,伊首先佇暫時位佇堆頂的欲插入的元素,佮對堆頂節點左右仔堆的兩堆頂元素中篩選出的彼个元素,二者內底選擇出佗一个適合作堆頂元素;若是欲插入元素適合,是以伊為新堆頂元素結束規个過程,若無以篩選出元素是新堆頂元素,閣自頂向下跤逐級處理提供新堆頂元素的子堆,欲插元素暫時共做其堆頂元素閣著伊繼續進行 ` siftdown `;` siftdown ` 只要到位有某一个堆底,就插入去欲插入去的元素結束規个過程。

咧提頂元素生做結果列表的時陣,先提走堆頂元素的內容,閣挽掉去最後的堆底元素將伊的內容暫時囥佇堆頂,這時陣爾大細嘛相應減一下,隨後的 ` siftdown ` 函數,揀出新的堆頂元素,閣共原底最後堆底元素插入去堆中。

佇咧 ` heapify ` 函數來起造堆的時陣,首先自列表中央將元素分做前後兩組,後組中的元素予人看做是干焦一个元素堆,然後自後向頭前處理前組的元素,這陣伊的左右子節點已經是已經有的堆或者是空縫,佇咧其上進行 ` siftdown `,毋過合做一个新堆。做規堆原仔會使採用 ` siftup ` 函數來實現,伊自第二个元素開始對前往後逐个處理列表元素,其實頭前是已經有的堆,共這个新元素自堆底向頂頭插入去這个堆內底。

疊排序算法嘛會當使用兩箍樹資料結構來實現二叉堆:

兩箍樹實現袂使直接訪問堆底元素,對袂好勢對挽伊規堆的大細減一。遮的 ` insert ` 函數,佇原堆頂元素佮欲插入元素內底選擇適合者做新的堆頂元素,將落選的另外一个元素作為新的愛插入元素,插入去到保持這个平衡的彼个樹仔內底。遮的 ` extract ` 函數隻篩選袂插入,伊就共大細減一下。

遮的 ` insert ` 和 ` extract ` 函數嘛會當直接轉寫做等價的尾遞歸形式,佮列表攏無仝,只要樹頭尾會當保持真好的平衡,採用尾遞歸形式就無傷大的必要性。 佇兩箍樹仔實現,嘛會使採用 ` siftdown ` 函數來初初來建造堆,毋免佇節點中保存關於樹仔狀態的統計信息。

基數排序

下跤是針對非負整數的基數排序算法的實現:

遮採用的基數是 ` 二 ` 的 ` 三 ` 次冪 ` 八 `,代碼所使用的列表元組大細佮基數大細成正比,運算量佮列表中元素的總數佮上大數的位數的乘積做正比。

隨機數生成

編寫排序算法進行測試除了使用簡單的數列, 測試用列表閣會使使用線性仝餘隨機數函數來生做:

語言解說器

定義佮處理一个小型表達式語言是誠對容易:

共這段代碼錄入文件比如講 ` expr-lang . sml `,並佇咧命令行下執行 ` sml expr-lang . sml `,會當用如此下佇咧正確類型的和無正確類型上運行的例,測試這个新的語言:

注釋佮附錄代碼

參見

  • Standard ML 佮伊的實現:
  • SML / NJ,由普林斯頓大學佮貝爾實驗室聯合開發的實現,伊具有並發編程擴展 Concurrent ML。
  • MLton,嚴格遵循標準定義的強力的全程序優化編譯器。
  • HaMLet,由馬克斯 ・ 普朗克軟體系統研究所(MPI-SWS)的 Andreas Rossberg 編寫,是一个 SML 解說器,意圖成做精確閣合宜接近的標準定義參考實現。
  • OCaml,由法國國家信息佮自動化研究所(INRIA)維護,是一个「工業強度」的 ML 方言,演化自上早用來實現 Coq 定理證明器的 Caml。
  • Alice,由薩爾蘭大學設計的 Alice ML,是因為 Standard ML 的函數式程式語言,擴展矣嘿並且發、分佈式佮約束式編程的豐富支持。
  • ATS,由波士頓大學的 Hongwei Xi 佮卡內基 ・ 梅隆大學的 Frank Pfenning 提出的 Dependent ML 發展而來,伊向 ML 擴展依賴類型。
  • F #,由微軟仔研究院(MSR)開發,是一个是對 OCaml 的一个以 . NET 為目標的程式的語言。
  • F \ *,由 MSR 和 INRIA 主導開發,是一个是對 ML 的依賴類型函數式程式語言。
  • Futhark,由哥本哈根大學計算機科學系(DIKU)開發,是屬於 ML 閣有家族的一个函數式、數據並行、陣列程式語言。
  • Ur,由麻省理工學院的 Adam Chlipala 開發,是語法的 Standard ML 的專門用佇咧 web 開發的一个函數式程式語言。
  • CM-Lex 和 CM-Yacc,是由卡內基 ・ 梅隆大學的 Karl Crary 開發,是用著 Standard ML、OCaml 和 Haskell 的詞法分析器佮語法解析器。
  • Amulet,是一个類 ML 的函數式程式語言,其編譯器輸出 Lua 文件。
  • Alpaca,是一个受 ML 啟發的運行佇 Erlang 虛擬機頂的函數式程式語言。

延伸閱讀

  • Robin Milner , Mads Tofte , Robert Harper . The Definition of Standard ML ( PDF ) . MIT Press . 一千九百九十 [二千空二十一孵三孵一] .(原始的內容 ( PDF ) 存檔佇二千空二十一孵一鼻十四).
  • Robin Milner , Mads Tofte , Robert Harper , David MacQueen . The Definition of Standard ML , Revised ( PDF ) . MIT Press . 一千九百九十七 [二千空二十一孵三孵一] . ISBN 空九二百六十二四六五三千一百八十一孵四 .(原始的內容 ( PDF ) 存檔佇二千空二十二孵三鋪九).
  • Robin Milner , Mads Tofte . Commentary on Standard ML . MIT Press . 一千九百九十一 [二千空二十一孵八孵三十一] . ISBN 九百七十八追空九二百六十二孵六鼻三千一百三十七刣二 .(原始內容存檔佇兩千空二十一分八刣三十一).
  • Emden R . Gansner , John H . Reppy . The Standard ML Basis Library ( PDF ) . Cambridge University Press . 兩千空四 [二千空二十一孵九九十七] .(原始的內容 ( PDF ) 存檔佇二千空二十二抹一曝二十九).
  • Mads Tofte . Four Lectures on Standard ML ( PDF ) . University of Edinburgh . 一千九百八十九 [二千空二十一孵九九四] .(原始的內容 ( PDF ) 存檔佇二千空二十二孵一鼻二十八).   Code examples in lectures . [二千空二十一孵九九十一] . 原始內容存檔佇兩千空一十六五四四配二 .
  • Mads Tofte . Essentials of Standard ML Modules . DIKU . 九百九十六 [二千空二十一孵九九四] .(原始內容存檔佇兩千空二十一抹九九分四).   The SML code ( uuencoded compressed tar ) . [二千空二十一孵九九十八] . 原始內容存檔佇兩千空五鋪三鋪七 .
  • Mads Tofte . Tips for Computer Scientists on Standard ML ( Revised ) ( PDF ) . ITU . 二千空九 [二千空二十一孵九九四] .(原始的內容 ( PDF ) 存檔佇二千空二十一石十一石二十七).   Examples . [二千空二十二孵一孵三] . 原始內容存檔佇兩千空一十七撨九尻川十五 .
  • Robert Harper . Programming in Standard ML ( PDF ) . Carnegie Mellon University . 二千空一十一 [二千空二十一孵二二十七] .(原始的內容 ( PDF ) 存檔佇二千空二十五二孵十五).   Examples . [二千空二十一孵九九十二] .(原始內容存檔佇兩千空二十一抹九九十二).
  • Michael J . C . Gordon . Introduction to Functional Programming . Cambridge University . 九百九十六 [二千空二十一孵九九十一] .(原始內容存檔佇兩千空二十一抹四鋪十一).   Lecture notes . [二千空二十一孵九九十一] .(原始內容存檔佇兩千空六抹六鋪二十三).
  • Lawrence Paulson . ML for the Working Programmer , 二 nd Edition . Cambridge University Press . 九百九十六 [二千空二十一孵八孵三十一] . ISBN 空抹五百二十一鋪五五百六千五百四十三-X .(原始內容存檔佇兩千空二十二謼二孵二十四).   Sample programs . [二千空二十一孵九九十二] .(原始內容存檔佇兩千空二十二孵一鋪十九).
  • David MacQueen . Should ML be Object-Oriented ? ( PDF ) . 兩千空二 [二千空二十一孵九九十] .(原始的內容 ( PDF ) 存檔佇二千空二十一石十二十九).
  • David MacQueen , Robert Harper , John Reppy . The History of Standard ML . 二千空二十 [二千空二十一孵八孵三十一] .(原始內容存檔佇兩千空二十一謼十二孵一).
  • Andrew W . Appel . Compiling with Continuations . Cambridge University Press . 一千九百九十二 [二千空二十二孵一孵三] .(原始內容存檔佇兩千空二十二孵一孵三).
  • Andrew W . Appel . Modern Compiler Implementation in ML . Cambridge University Press . 一千九百九十八 [二千空二十二孵一孵十二] .(原始內容存檔佇兩千空二十二岫一謼十二).   Tiger compiler modules for programming exercises . [二千空二十一孵九九十二] .(原始內容存檔佇兩千空二十二抹五鋪六).
  • Jeffrey D . Ullman . Elements of ML Programming , ML 九十七喔 Edition . Prentice-Hall . 一千九百九十八 [二千空二十一孵十二孵三十] . ISBN 空知十三五七十九九五空三百八十七七五一 .(原始內容存檔佇兩千空二十二岫三鋪十二).   Programs from the text . [二千空二十二孵一孵一] .(原始內容存檔佇兩千空二十二抹二鋪十四).
  • Anthony L . Shipman . Unix System Programming with Standard ML ( PDF ) . 兩千空一 [二千空二十一孵九九一] .(原始的內容 ( PDF ) 存檔佇二千空二十一孵一鼻二十一).

引用

外部連結

  • Andreas Rossberg . Standard ML and Objective Caml , Side by Side . 二千空一十一 [二千空二十一孵八孵三十一] .(原始內容存檔佇兩千空二十一謼十二孵三十).
  • Adam Chlipala . Comparing Objective Caml and Standard ML . 二千空二十 [二千空二十一孵八孵三十一] .(原始內容存檔佇咧二千空二十一鋪十二鋪十六).
  • SML Help
  • cmlib