fbpx
维基百科

ML语言

MLMeta Language:元语言),是一个函数式指令式通用编程语言,它著称于使用了多态Hindley–Milner类型推论[8]。ML能自动的指定多数表达式英语Expression (computer science)类型,不要求显式的类型标注,而且能够确保类型安全,已经正式证明了有良好类型的ML程序不会导致运行时间类型错误[8]

ML
编程范型多范型函数式指令式
設計者罗宾·米尔纳爱丁堡大学其他人
发行时间1973年,​49年前​(1973
穩定版本
Standard ML '97
(1997年,​25年前​(1997
型態系統类型推论静态类型强类型
衍生副語言
Standard ML, OCaml
啟發語言
ISWIM[1]PAL[2]POP-2[1],GEDANKEN[1]
影響語言
ClojureCoqCyclone英语Cyclone (programming language)C++Elm[3]Futhark[4]F#F*HaskellIdris、Lazy ML[5]MirandaNemerle[6]OCamlOpa英语Opa (programming language)RustScalaStandard MLUr[7]

ML提供了对函数实际参数的模式匹配垃圾回收指令式编程传值调用柯里化。它被大量的用于编程语言研究之中,并且是全面规定了的和使用形式语义验证了的少数语言之一。它的类型和模式匹配使得它非常适合并且经常用于在其他形式语言上进行操作,比如在编译器构造自动化定理证明形式验证中。

历史

1970年代早期,ML由爱丁堡大学罗宾·米尔纳及他人研制出来[1],用于在LCF英语Logic for Computable Functions定理证明器中开发证明策略[9]。LCF的语言是“PPλ”,它是一阶逻辑演算与有类型的多态λ演算的结合,以ML作为元语言。ML的语法从ISWIM及其扩展实现PAL得到了启发[2]LCF英语Logic for Computable Functions ML运行在DEC-10/TOPS-10主机Stanford LISP 1.6下[10]

在1980年,Luca Cardelli英语Luca Cardelli于爱丁堡大学的VAX/VMS系统上开发了ML编译器,它被称为“VAX ML”[11],以区别于LCF版本的“DEC-10 ML”[12]。VAX ML的编译器和运行时间系统二者,都是用Pascal书写而建立在“函数抽象机器”(FAM)之上[13]。在1982年,爱丁堡大学的Kevin Mitchell,用VAX ML重写了VAX ML编译器,随即John Scott和Alan Mycroft英语Alan Mycroft加入了开发,在又进行一系列重写改进之后,新的编译器被称为“Edinburgh ML”[14]

在1981年,INRIAGérard Huet英语Gérard Huet,将最初的LCF ML适配到Multics系统的Maclisp下,并且增加了编译器[15]。这个实现被描述于INRIA内部文档“ML手册”之中[16],它被开发者自称为“Le_ML”[17]剑桥大学Lawrence Paulson英语Lawrence Paulson用它开发了基于Franz Lisp的Cambridge LCF[18],进而剑桥大学Michael J. C. Gordon英语Michael J. C. Gordon又用它开发了基于Common Lisp的第一版的HOL英语HOL (proof assistant)[19]

在1983年,Robin Milner由两个动机驱使开始重新设计ML[20]。其一是爱丁堡大学Rod Burstall英语Rod Burstall及其小组在规定上的工作,具体化为规定语言CLEAR[21],和表达可执行规定的函数式语言HOPE[22]。这项工作与ML有关的是两方面成果:首先,HOPE拥有优雅的编程特征,特别是模式匹配[23],和子句式函数定义[24];其次,是使用在接口中的签名,进行规定的模块化构造的想法。其二是Luca Cardelli英语Luca Cardelli在VAX ML上的工作,通过增加命名记录和可变类型,扩展了ML中数据类型的品目[25]

在1984年,贝尔实验室的David MacQueen提出了对Standard ML模块系统的设计[26]。在Standard ML的持续设计期间[27],Edinburgh ML被渐进的修改,充当了Standard ML的近似原型实现[28]。在1986年,普林斯顿大学Andrew Appel英语Andrew Appel贝尔实验室的David MacQueen,以Edinburgh Standard ML作为起步开发环境[29],开始了专注于生成高质量机器代码的Standard ML of New Jersey的活跃开发[30]

在1990年,Robin MilnerMads Tofte英语Mads TofteRobert Harper英语Robert Harper (computer scientist)制定的Standard ML的正式规定《The Definition of Standard ML》最终完成[31];在1997年,这个标准规定增补了David MacQueen为作者并进行了修订[32]。在1989年,Mads Tofte英语Mads Tofte、Nick Rothwell和David N. Turner于爱丁堡大学开始开发ML Kit编译器,为了强调清晰性而非高效,将标准定义直接转译成一组Standard ML模块;在1992年和1993年期间,主要通过爱丁堡大学的Nick Rothwell和哥本哈根大学计算机科学系英语UCPH Department of Computer Science(DIKU)的Lars Birkedal的工作[33],ML Kit第一版完成并开源发行[34]

在1987年,INRIA的Ascánder Suárez,基于巴黎第七大学Guy Cousineau法语Guy Cousineau的“范畴抽象机器英语Categorical abstract machine”(CAM)[35],利用Le Lisp的运行时间系统重新实现了Le_ML,并正式命名为Caml[15]。在1990年和1991年,INRIAXavier Leroy英语Xavier Leroy基于用C实现的字节码解释器[36],利用Damien Doligez英语Damien Doligez提供的内存管理系统重新实现了Caml,并称其为Caml Light[37]。在1995年,Xavier Leroy又增加了机器代码编译器和高层模块系统[38],这个版本也称为“Caml Special Light”。在1996年,INRIA的Didier Rémy和Jérôme Vouillon,向Caml Special Light增加了面向对象特征[39],从而形成了OCaml[40]

今天ML家族的两个主要的方言是Standard MLOCaml。ML的实力大多被用于语言设计和操作,比如建构编译器、分析器、定理证明器,但是它作为通用语言也被用于生物信息和财务系统等领域。ML确立了静态类型函数式编程范型,从而在编程语言历史上占有显要地位,它的思想在影响了众多的语言,例如HaskellNemerle[6]ATS英语ATS (programming language)Elm[3]

解释与编译

ML代码片段很容易通过将其录入到“顶层”来研习,它也叫作读取﹣求值﹣输出循环或REPL。这是打印结果或定义的表达式的推论类型的交互式会话。很多SML实现提供交互式REPL,比如SML/NJ

$ sml Standard ML of New Jersey v110.79 [built: Sat Oct 26 12:27:04 2019] - 

可以在提示符-后键入代码。例如计算1 + 2 * 3:

- 1 + 2 * 3; val it = 7 : int 

顶层推论这个表达式的类型为int并给出结果7。如果输入不完全则打印第二提示符=,这时经常可以用;终结输入。it是给未指定变量的表达式的标准变量。输入control-C可返回解释器顶层,输入control-D可退出解释器。

下面是hello, world!的程序代码在SML/NJ解释器下执行的结果:

- val _ = print "Hello, world!\n"; Hello, world! 

和使用MLton编译器进行编译执行的例子:

$ echo 'print "Hello, world!\n";' > hello-world.sml $ mlton hello-world.sml $ ./hello-world Hello, world! 

核心语言

不同于纯函数式编程语言,ML是兼具一些指令式特征的函数式编程语言。ML的特征包括:传值调用的求值策略头等函数,带有垃圾收集的自动内存管理参数多态静态类型类型推论代数数据类型模式匹配异常处理。不同于Haskell,ML与大多数编程语言一样使用及早求值

用ML书写的程序构成自要被求值的表达式英语Expression (computer science),而非语句或命令,尽管一些表达式返回一个平凡的unit值并且只为其副作用而求值。以下章节介绍采用Standard ML的语法和语义。

函数

就像所有的函数式语言一样,ML的关键特征是函数,它被用于进行抽象。例如阶乘函数用纯ML可表达为:

fun fac 0 = 1 | fac n = n * fac (n - 1) 

这里将阶乘描述为递归函数,具有一个单一的终止基础情况。它类似于在数学教科书见到的阶乘描述。多数ML代码在设施和语法上类似于数学。

凭借类型推论编译器能推导出,fac接受整数0作为实际参数,则形式参数n也是整数类型int,而fac 0的结果是整数1,则函数fac的结果也是整数类型。函数fac接受一个整数的形式参数并返回一个整数结果,它作为一个整体从而有着“从整数到整数的函数”类型int -> int。函数及其形式参数的"类型"还可以用类型标注(annotation)来描述,使用E : t表示法,它可以被读作表达式E有类型t,它是可选也可忽略的。使用类型标注,这个例子可重写为如下:

fun fac 0 = 1 | fac (n : int) : int = n * fac (n - 1) 

这个函数还依赖于模式匹配,这是ML语言的重要部份。注意函数形式参数不必须在圆括号内但要用空格分隔。当一个函数的实际参数是0,它将返回整数1。对于所有其他情况,尝试第二行。这是一个递归,并且再次执行这个函数直到达到基础情况。它可以使用case表达式重写为:

fun fac n = case n of 0 => 1 | n => n * fac (n - 1) 

这里case介入了模式和对应表达式的序列。它还可以重写为将标识符绑定到lambda函数

val rec fac = fn 0 => 1 | n => n * fac (n - 1) 

这里的关键字val介入了标识符到值的绑定,fn介入了匿名函数的定义,它可以用在fun的位置上,但使用=>算符而非=。绑定到递归的匿名函数需要使用rec关键字来指示。

通过将主要工作写入尾递归风格的内部迭代函数,借助于语言编译或解释系统进行的尾调用优化,这个函数可以得以增进性能,它的调用栈不需要随函数调用数目而成比例的增长。对这个函数可以采用向内部函数增加额外的“累加器”形式参数acc来实现:

fun fact n = let fun fac (0, acc) = acc | fac (n, acc) = fac (n - 1, n * acc) in fac (n, 1) end 

let表达式的值是在inend之间表达式的值。这个递归函数的实现不保证能够终止,因为负数实际参数会导致递归调用的无穷降链条件。更健壮的实现会在递归前检查实际参数为非负数,并在有问题的情况,即n是负数的时候,启用异常处理

fun fact n = let fun fac (0, acc) = acc | fac (n, acc) = fac (n - 1, n * acc) in if (n < 0) then raise Fail "negative argument" else fac (n, 1) end 

类型

有一些基本类型可以当作是“内建”的,因为它们是在Standard ML标准基本库中预先定义的,并且语言为它们提供文字英语Literal (computer programming)表示法,比如34是整数,而"34"是字符串。一些最常用的基本类型是:

  • int 整数,比如3~12。注意波浪号~表示负号。
  • real浮点数,比如4.2~6.4。Standard ML不隐含的提升整数为浮点数,因此表达式2 + 5.67 是无效的。
  • string字符串,比如"this is a string"""(空串)。
  • char字符,比如#"y"#"\n"(换行符)。
  • bool布尔值,它是要么true要么false。产生bool值的有比较算符=<>>>=<<=,逻辑函数not短路求值的中缀算符andalsoorelse

包括上述基本类型的各种类型可以用多种方式组合。一种方式是元组,它是值的有序集合,比如表达式(1, 2)的类型是int * int,而("foo", false)的类型是string * bool。可以使用#1 ("foo", false)这样的语法来提取元组的指定次序的成员。

有0元组(),它的类型指示为unit。但是没有1元组,或者说在例子(1)1之间没有区别,都有类型int。元组可以嵌套,(1, 2, 3)不同于((1, 2), 3)(1, (2, 3))二者。前者的类型是int * int * int,其他两个的类型分别是(int * int) * intint * (int * int)

组合值的另一种方式是记录。记录很像元组,除了它的成员是有名字的而非有次序的,例如{a = 5.0, b = "five"}有类型{a : real, b : string},这同于类型{b : string, a : real}。可以使用#a {a = 5.0, b = "five"}这样的语法来选取记录的指定名字的字段。

Standard ML中的函数只接受一个值作为参数,而不是参数的一个列表,可以使用上述元组模式匹配来实际上传递多个参数。函数还可以返回一个元组。例如:

fun sum (a, b) = a + b fun average pair = sum pair div 2 infix averaged_with fun a averaged_with b = average (a, b) val c = 3 averaged_with 7 fun int_pair (n : int) = (n, n) 

这里第一段创建了两个类型是int * int -> int的函数sumaverage。第二段创建中缀算子averaged_with,接着定义它为类型int * int -> int的函数。最后的int_pair函数的类型是int -> int * int

下列函数是多态类型的一个例子:

fun pair x = (x, x) 

编译器无法推论出的pair的特殊化了的类型,它可以是int -> int * intreal -> real * real甚至是(int * real -> string) -> (int * real -> string) * (int * real -> string)。在Standard ML中,它可以简单指定为多态类型'a -> 'a * 'a,这里的'a(读作“alpha”)是一个类型变量,指示任何可能的类型。在上述定义下,pair 3pair "x"都是有良好定义的,分别产生(3, 3)("x", "x")

SML标准基本库包括了重载标识符+-*divmod/~abs<><=>=。标准基本库提供了多态函数:!:=obeforeignore。中缀运算符可以有从缺省最低0到最高9的任何运算符优先级。标准基本库提供了如下内建中缀规定:

infix 7 * / div mod infix 6 + - ^ infixr 5 :: @ infix 4 = <> > >= < <= infix 3 := o infix 0 before 

等式类型

算符=<>分别被定义为多态的等式和不等式。=它确定两个值是否相等,有着类型''a * ''a -> bool。这意味着它的两个运算数必须有相同的类型,这个类型必须是等式类型(eqtype)。上述基本类型中除了real之外,intrealstringcharbool都是等式类型。

例如:3 = 3"3" = "3"#"3" = #"3"true = true,都是有效的表达式并求值为true;而3 = 4是有效表达式并求值为false3.0 = 3.0是无效表达式而被编译器拒绝。这是因为IEEE浮点数等式打破了ML中对等式的一些要求。特别是nan不等于自身,所以关系不是自反的。

元组和记录类型是等式类型,当时且仅当它的每个成员类型是等式类型;例如int * string{b : bool, c : char}unit是等式类型,而int * real{x : real}不是。函数类型永远不是等式类型,因为一般情况下不可能确定两个函数是否等价。

类型声明

类型声明或同义词(synonym)使用type关键字来定义。下面是给在平面中的点的类型声明,计算两点间距离,和通过海伦公式计算给定角点的三角形的面积的函数。

type loc = real * real fun heron (a: loc, b: loc, c: loc) = let fun dist ((x0, y0), (x1, y1)) = let val dx = x1 - x0 val dy = y1 - y0 in Math.sqrt (dx * dx + dy * dy) end val ab = dist (a, b) val bc = dist (b, c) val ac = dist (a, c) val s = (ab + bc + ac) / 2.0 in Math.sqrt (s * (s - ab) * (s - bc) * (s - ac)) end 

数据类型

Standard ML提供了对代数数据类型(ADT)的强力支持。一个ML数据类型可以被当作是元组不交并英语Product type)。数据类型使用datatype关键字来定义,比如:

datatype int_or_string = INT of int | STRING of string | NEITHER 

这个数据类型声明建立一个全新的数据类型int_or_string,还有一起的新构造子(一种特殊函数或值)INTSTRINGNEITHER;每个这种类型的值都是要么INT具有一个整数,要么STRING具有一个字符串,要么NEITHER。写为如下这样:

val i = INT 3 val s = STRING "qq" val n = NEITHER val INT j = i 

这里最后的一个声明通过模式匹配,将变量j绑定到变量i所绑定的整数3val 模式 = 表达式是绑定的一般形式,它是良好定义的,当且仅当模式和表达式有相同的类型。

数据类型可以是多态的:

datatype 'a pair = PAIR of 'a * 'a 

这个数据类型声明建立一个新的类型'a pair家族,比如int pairstring pair等等。

数据类型可以是递归的:

datatype int_list = EMPTY | INT_LIST of int * int_list 

这个数据类型声明建立一个新类型int_list,这个类型的每个值是要么EMPTY(空列表),要么是一个整数和另一个int_list的接合。

通过datatype创建的类型是等式类型,如果它的所有变体,要么是没有参数的空构造子,要么是有等式类型参数的构造子,并且在多态类型情况下所有类型参数也都是等式类型。递归类型在有可能情况下是等式类型,否则就不是。

列表

基础库提供的复杂数据类型之一是列表list。它是一个递归的、多态的数据类型,可以等价的定义为:

datatype 'a list = nil | :: of 'a * 'a list 

这里的::是中缀算符,例如3 :: 4 :: 5 :: nil是三个整数的列表。列表是ML程序中最常用的数据类型之一,语言还为生成列表提供了特殊表示法[3, 4, 5]

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的简单应用:

fun revAppend ([], l) = l | revAppend (x :: r, l) = revAppend(r, x :: l) fun rev l = revAppend(l, []) fun l1 @ l2 = revAppend(rev l1, l2) 

模式匹配

Standard ML的数据类型可以轻易的定义和用于编程,在很大程度上是由它的模式匹配,还有多数Standard ML实现的模式穷尽性检查和模式冗余检查。

模式匹配可以在语法上嵌入到变量绑定之中,比如:

val ((m: int, n: int), (r: real, s: real)) = ((2, 3), (2.0, 3.0)) type hyperlink = {protocol: string, address: string, title: string} val url : hyperlink = {title="The Standard ML Basis Library", protocol="https", address="//smlfamily.github.io/Basis/overview.html"} val {protocol=port, address=addr, title=name} = url val x as (fst, snd) = (2, true) 

第一个val绑定了四个变量mnrs;第二个val绑定了一个变量url;第三个val绑定了三个变量portaddrname,第四个叫分层模式,绑定了三个变量xfstsnd

模式匹配可以在语法上嵌入到函数定义中,比如:

datatype shape = Circle of loc * real (* 中心和弧度 *) | Square of loc * real (* 左上角和边长,坐标轴对齐 *) | Triangle of loc * loc * loc (* 角点 *) fun area (Circle (_, r)) = 3.14 * r * r | area (Square (_, s)) = s * s | area (Triangle (a, b, c)) = heron (a, b, c) 

次序在模式匹配中是紧要的:模式按文本次序来依次进行匹配。在特定计算中,使用下划线_,来省略不需要它的值的子成员,这也叫做通配符(wildcard)模式。所谓的“子句形式”风格的函数定义,这里的模式紧随在函数名字之后出现,只是如下形式的一种语法糖

fun area shape = case shape of Circle (_, r) => 3.14 * r * r | Square (_, s) => s * s | Triangle (a, b, c) => heron (a, b, c) 

模式穷尽性检查将确保数据类型的每个情况都已经顾及到。[a] 如果有遗漏,则产生警告。[b] 如果模式存在冗余,也会导致一个编译时间警告。[c]

高阶函数

函数可以接受函数作为实际参数,比如:

fun applyToBoth f x y = (f x, f y) 

函数可以产生函数作为返回值,比如:

fun constantFn k = (fn anything => k) 

函数可以同时接受和产生函数,比如复合函数英语Function composition (computer science)

fun compose (f, g) = (fn x => f (g x)) 

基本库的函数List.map,是在Standard ML中最常用的Curry化高阶函数,它在概念上可定义为:

fun map' _ [] = [] | map' f (x :: xs) = f x :: map f xs 

在基本库中将函数复合定义为多态中缀算符(f o g)mapfold高阶函数有较高效率的实现。[d]

异常

异常可以使用raise关键字发起,并通过模式匹配handle构造来处理:

exception Undefined; fun max [x] = x | max (x :: xs) = let val m = max xs in if x > m then x else m end | max [] = raise Undefined fun main xs = let val msg = (Int.toString (max xs)) handle Undefined => "empty list...there is no max!" in print (msg ^ "\n") end 

这里的^是字符串串接算符。可以利用异常系统来实现非局部退出,例如这个函数所采用技术:

exception Zero; fun listProd ns = let fun p [] = 1 | p (0 :: _) = raise Zero | p (h :: t) = h * p t in (p ns) handle Zero => 0 end 

异常Zero0情况下发起,控制从函数p中一起出离。

引用

初始化基础库还以引用的形式提供了可变的存储。引用ref可以在某种意义上被认为是如下这样定义的:

datatype 'a ref = ref of 'a 

还定义了内建的:=函数来修改引用的内容,和!函数来检索引用的内容。阶乘函数可以使用引用定义为指令式风格:

fun factImperative n = let val i = ref n and acc = ref 1 in while !i > 0 do (acc := !acc * !i; i := !i - 1); !acc end 

这里使用圆括号对以;分隔的表达式进行了顺序复合。

可变类型'a ref是等式类型,即使它的成员类型不是。两个引用被称为是相等的,如果它们标识相同的“ref单元”,就是说相同的对ref构造子调用生成的同一个指针。因此(ref 1) = (ref 1)(ref 1.0) = (ref 1.0)都是有效的,并且都求值为false,因为即使两个引用碰巧指向了相同的值,引用自身是分立的,每个都可以独立于其他而改变。

模块语言

模块是ML用于构造大型项目和库的系统。

模块

一个模块构成自一个签名(signature)文件和一个或多个结构文件。签名文件指定要实现的API(就像C语言头文件或Java接口文件)。结构实现这个签名(就像C语言源文件或Java文件)。解释器通过use命令导入它们。ML的标准库被实现为这种方式的模块。

例如,下列定义一个算术签名:

signature ARITH = sig eqtype t val zero : t val one : t val fromInt: int -> t val fromIntPair : int * int -> t val fromReal : real -> t val succ : t -> t val pred : t -> t val ~ : t -> t val + : t * t -> t val - : t * t -> t val * : t * t -> t val / : t * t -> t val == : t * t -> bool val <> : t * t -> bool val > : t * t -> bool val >= : t * t -> bool val < : t * t -> bool val <= : t * t -> bool end 

和这个签名使用有理数的实现:

structure Rational : ARITH = struct datatype t = Rat of int * int val zero = Rat (0, 1) val one = Rat (1, 1) fun fromInt n = Rat (n, 1) fun ineg (a, b) = (~a, b) fun fromIntPair (num, den) = let fun reduced_fraction (numerator, denominator) = let fun gcd (n, 0) = n | gcd (n, d) = gcd (d, n mod d) val d = gcd (numerator, denominator) in if d > 1 then (numerator div d, denominator div d) else (numerator, denominator) end in if num < 0 andalso den < 0 then Rat (reduced_fraction (~num, ~den)) else if num < 0 then Rat (ineg (reduced_fraction (~num, den))) else if den < 0 then Rat (ineg (reduced_fraction (num, ~den))) else Rat (reduced_fraction (num, den)) end val SOME maxInt = Int.maxInt val minPos = 1.0 / (real maxInt) fun fromReal r = let fun convergent (i, f, h_1, k_1, h_2, k_2) = if i <> 0 andalso ((h_1 > (maxInt - h_2) div i) orelse (k_1 > (maxInt - k_2) div i)) then (h_1, k_1) else if f < minPos then (i * h_1 + h_2, i * k_1 + k_2) else convergent (trunc (1.0 / f), Real.realMod (1.0 / f), i * h_1 + h_2, i * k_1 + k_2, h_1, k_1) in if r < 0.0 then Rat (ineg (convergent (trunc (~ r), Real.realMod (~ r), 1, 0, 0, 1))) else Rat (convergent (trunc r, Real.realMod r, 1, 0, 0, 1)) end fun succ (Rat (a, b)) = fromIntPair (a + b, b) fun pred (Rat (a, b)) = fromIntPair (a - b, b) fun add (Rat (a, b), Rat (c, d)) = if b = d then fromIntPair(a + c, b) else fromIntPair (a * d + c * b, b * d) fun sub (Rat (a, b), Rat (c, d)) = if b = d then fromIntPair(a - c, b) else fromIntPair (a * d - c * b, b * d) fun mul (Rat (a, b), Rat (c, d)) = fromIntPair (a * c, b * d) fun div_ (Rat (a, b), Rat (c, d)) = fromIntPair (a * d, b * c) fun gt (Rat (a, b), Rat (c, d)) = if b = d then (a > c) else (a * d) > (b * c) fun lt (Rat (a, b), Rat (c, d)) = if b = d then (a < c) else (a * d) < (b * c) fun neg (Rat (a, b)) = Rat (~a, b) fun eq (Rat (a, b), Rat (c, d)) = ((b = d) andalso (a = c)) fun ~ a = neg a fun a + b = add (a, b) fun a - b = sub (a, b) fun a * b = mul (a, b) fun a / b = div_ (a, b) fun op == (a, b) = eq (a, b) fun a <> b = not (eq (a, b)) fun a > b = gt (a, b) fun a >= b = (gt (a, b) orelse eq (a, b)) fun a < b = lt (a, b) fun a <= b = (lt (a, b) orelse eq (a, b)) end 

下面是这个结构的简单用例:

infix == local open Rational in val c = let val a = fromIntPair(2, 3) val b = fromIntPair(4, 6) in a + b end end structure R = Rational R.fromReal(3.245) 

Standard ML只允许通过签名函数同实现进行交互,例如不可以直接通过这个代码中的Rat来建立数据对象。结构块对外部隐藏所有实现细节。这里的:叫做透明归属(ascription),可以通过所绑定的变量见到此结构的数据内容,与之相对的是:>,它叫做不透明归属,此结构的数据内容对外完全不可见。比如上面用例有结果:val c = Rat (4,3) : Rational.t,如果改为不透明归属则有结果:val c = - : Rational.t

要用有理数进行实际上的数值计算,需要处理分数形式中分母快速增大导致溢出整数类型大小范围等问题。[e]

函子

函子接受指定签名的一个结构作为参数,并返回一个结构作为结果,下面示例的函子能在ARITH签名的结构上计算移动平均

signature MOVINGLIST = sig type t structure Arith : sig type t end val size : t -> int val average : t -> Arith.t val fromList : Arith.t list -> t val move : t * Arith.t -> t val expand : t * Arith.t -> t val shrink : t -> t val trunc : t -> t end 
functor MovingList (S: ARITH) : MOVINGLIST = struct type t = S.t list * int * S.t structure Arith = S fun size (ml : t) = #2 ml fun average (ml : t) = #3 ml fun fromList (l : S.t list) = let val n = length l val sum = foldl S.+ S.zero l local open S in val m = sum / (fromInt n) end in if (null l) then raise Empty else (l, n, m) end fun move ((l, n, m) : t, new : S.t) = let val old = List.nth (l, n - 1) local open S in val m' = m + (new - old) / (fromInt n) end in (new :: l, n, m') end fun expand ((l, n, m) : t, new : S.t) = let val n' = n + 1; local open S in val m' = m + (new - m) / (fromInt n') end in (new :: l, n', m') end fun shrink ((l, n, m) : t) = let val old = List.nth (l, n - 1) val n' = if (n > 2) then n - 1 else 1 local open S in val m' = m + (m - old) / (fromInt n') end in (l, n', m') end fun trunc ((l, n, m) : t) = (List.take (l, n), n, m) end 

和这个函子的简单用例:

structure R = Rational structure MLR = MovingList (Rational) val d = MLR.fromList [R.fromIntPair (4, 5), R.fromIntPair (2, 3)] val d = MLR.expand (d, R.fromIntPair (5, 6)) val d = MLR.move (d, R.fromIntPair (7, 8)) val d = MLR.shrink d val d = MLR.trunc d 

这个用例承上节示例,Rational结构采用了透明归属,有结果如:val d = ([Rat (4,5),Rat (2,3)],2,Rat (11,15)) : MLR.t。如果它改为不透明归属,则对应结果为:val d = ([-,-],2,-) : MLR.t

示例代码

下列例子使用了Standard ML的语法和语义。

素数

下面是求素数试除法实现:

fun prime n = let fun isPrime (l, i) = let fun existsDivisor [] = false | existsDivisor (x :: xs) = if (i mod x) = 0 then true else if (x * x) > i then false else existsDivisor xs in not (existsDivisor l) end fun iterate (acc, i) = if i > n then acc else if isPrime (acc, i) then iterate (acc @ [i], i + 2) else iterate (acc, i + 2) in if n < 2 then [] else iterate ([2], 3) end 

基本库findexists函数在不存在符合条件元素的时候会遍历整个列表,[f] 这里采用了特殊化了的existsDivisor,用以在后续元素都不满足条件时立即结束运算。

下面是埃拉托斯特尼筛法实现:

fun prime n = let fun dropComposite (acc, [], _, _) = rev acc | dropComposite (acc, l as x :: xs, j, i) = if j > n then List.revAppend (acc, l) else if x < j then dropComposite (x :: acc, xs, j, i) else if x > j then dropComposite (acc, l, j + i, i) else dropComposite (acc, xs, j + i, i) fun init i = let fun loop (l, i) = if i <= 2 then l else loop (i :: l, i - 2) in loop ([], i - (i + 1) mod 2) end fun iterate (acc, []) = rev acc | iterate (acc, l as x :: xs) = if x * x > n then 2 :: List.revAppend (acc, l) else iterate (x :: acc, dropComposite ([], xs, x * x, x * 2)) in if n < 2 then [] else iterate ([], init n) end 

这里基于列表的筛法实现符合埃拉托斯特尼的原初算法[41]筛法还有基于数组的直观实现。[g] 下面是其解释器下命令行运行实例:

- fun printIntList (l: int list) = = print ((String.concatWith " " (map Int.toString l)) ^ "\n"); val printIntList = fn : int list -> unit - val _ = printIntList (prime 100); 2 3 5 7 11 13 17 19 23 29 31 37 41 43 47 53 59 61 67 71 73 79 83 89 97 

汉明数

正规数是形如 整数,对于非负整数   ,它是可以整除 的数。计算升序的正规数的算法经由戴克斯特拉得以流行[42]理查德·汉明最初提出了这个问题,故而这个问题被称为“汉明问题”,这个数列也因而被称为汉明数。Dijkstra计算这些数的想法如下:

  • 汉明数的序列开始于数1
  • 要加入序列中的数有下述形式:2h, 3h, 5h,这里的h是序列已有的任意的汉明数。
  • 因此,可以生成最初只有一个1的序列H,并接着归并英语Merge algorithm序列2H, 3H, 5H,并以此类推。

示例汉明数程序代码,一般用来展示,确使计算只在需要时进行的纯函数式编程方式[43]

fun Hamming_number n = let fun merge (p, q) = let fun revMerge (acc, p, q) = if not (null p) andalso not (null q) then if hd p < hd q then revMerge ((hd p) :: acc, tl p, q) else if hd p > hd q then revMerge ((hd q) :: acc, p, tl q) else revMerge ((hd p) :: acc, tl p, tl q) else if null p then List.revAppend (q, acc) else List.revAppend (p, acc) in if (null p) then q else if (null q) then p else rev (revMerge ([], p, q)) end fun mul m x = if x <= (n div m) then SOME (x * m) else NONE fun mapPrefix pred l = let fun mapp ([], acc) = rev acc | mapp (x :: xs, acc) = (case (pred x) of SOME a => mapp (xs, a :: acc) | NONE => rev acc) in mapp (l, []) end fun mergeWith f (m, i) = merge (f m, i) fun generate l = let fun listMul m = mapPrefix (mul m) l in foldl (mergeWith listMul) [] [2, 3, 5] end fun iterate (acc, l) = if (hd l) > (n div 2) then merge (l, acc) else iterate (merge (l, acc), generate l) in if n > 0 then iterate ([], [1]) else [] end 

产生指定范围内的汉明数需要多轮运算,后面每轮中的三个列表元素乘积运算中都可能产生超出这个范围的结果,它们不需要出现在后续的运算之中。[h] 基本库mapPartial函数与它所映射的函数,通过基于Option结构的SOMENONE构造子的协定,可以将所映射函数认为不符合条件的元素或者结果排除掉,它会遍历整个列表。[i] 由于这个算法采用升序列表,故而这里将它改写为mapPrefix函数,用来在特定条件不满足条件就立即结束。下面是汉明数程序在解释器下命令行运行实例:

- fun printIntList (l: int list) = = print ((String.concatWith " " (map Int.toString l)) ^ "\n"); val printIntList = fn : int list -> unit - val _ = printIntList (Hamming_number 400); 1 2 3 4 5 6 8 9 10 12 15 16 18 20 24 25 27 30 32 36 40 45 48 50 54 60 64 72 75 80 81 90 96 100 108 120 125 128 135 144 150 160 162 180 192 200 216 225 240 243 250 256 270 288 300 320 324 360 375 384 400 

续体传递风格实例

下面是续体传递风格英语Continuation-passing style(CPS)[44]高阶函数foldrmap的实现,和达成一个整数列表的合计函数的简单用例:

fun foldr' f b l = let fun f2 (k, []) = k b | f2 (k, a :: r) = f2 (fn x => k (f (a, x)), r) in f2 (fn x => x, l) end fun map' f l = foldr' (fn (x, y) => (f x) :: y) [] l fun sum l = foldr' (fn (x, y) => (x + y)) 0 l 

对于输入[e1, e2, ..., en]sum函数等价于函数复合(fn x => x) o (fn x => e1 + x) o (fn x => e2 + x) o ... o (fn x => en + x),它应用于0上得到(e1 + (e2 + (... + (en + 0)...)))[45]

SML/NJ支持头等对象续体[46]。头等续体对一门语言而言是能完全控制指令执行次序的能力。它们可以用来跳转到产生对当前函数调用的那个函数,或者跳转到此前已经退出了的函数。头等续体保存了程序执行状态,它不保存程序数据,只保存执行上下文

排序算法

排序算法关注计算复杂度,特别是时间复杂度,基本库函数的实现细节也要考虑在内,比如串接函数@,它被实现为fun l1 @ l2 = revAppend(rev l1, l2),除非必需的情况避免使用遍历整个列表的revlength函数。[j] 通过比较于这些排序算法的周知过程式编程语言比如C语言的实现,可以体察到ML在控制流程和列表数据结构上的相关限制,和与之相适应的采用尾递归的特色函数式编程风格。

插入排序

下面是简单的插入排序算法的尾递归和等价的普通递归实现:

尾递归 普通递归
fun insertSort l = let fun insert pred (ins, l) = let fun loop (acc, []) = List.revAppend (acc, [ins]) | loop (acc, l as x :: xs) = if pred (ins, x) then List.revAppend (acc, ins :: l) else loop (x :: acc, xs) in loop ([], l) end val rec ge = fn (x, y) => (x >= y) in rev (foldl (insert ge) [] l) end 
fun insertSort l = let fun insert pred (ins, []) = [ins] | insert pred (ins, l as x :: xs) = if pred (ins, x) then ins :: l else x :: (insert pred (ins, xs)) val rec ge = fn (x, y) => (x >= y) in rev (foldl (insert ge) [] l) end 
x保存在形式参数acc对应的分配堆 x保存在调用栈栈帧中

插入排序算法是稳定自适应排序英语Adaptive sort,它在输入列表趋于正序的时候性能最佳,在输入列表趋于反序的时候性能最差,因此在算法实现中,需要insert函数所插入列表保持为反序,在插入都完成后经rev函数再反转回正序。在预期输入数据趋于随机化或者预知它经过了反转的情况下,可以采用保持要插入列表为正序的变体插入排序算法实现,它在输入列表趋于反序的时候性能最佳,在输入列表趋于正序的时候性能最差,它比自适应实现少作一次全列表反转。[k] 采用foldr函数可以相应的保持要插入列表为正序,由于fun foldr f b l = foldl f b (rev l),它等同于对反转过的列表应用变体插入排序。

希尔排序

希尔排序算法是对插入排序的改进,保持了自适应性英语Adaptive sort,放弃了稳定性[l] 下面是希尔排序的实现:

fun shellSort l = let fun insert pred (ins, l) = let fun loop (acc, []) = List.revAppend (acc, [ins]) | loop (acc, l as x :: xs) = if pred (ins, x) then List.revAppend (acc, ins :: l) else loop (x :: acc, xs) in loop ([], l) end val rec lt = fn (x, y) => (x < y) fun insertSort [] = [] | insertSort [x] = [x] | insertSort [x, y] = if (y < x) then [y, x] else [x, y] | insertSort (x :: y :: z :: xs) = let val (x, y, z) = if (y < x) then if z < y then (z, y, x) else if z < x then (y, z, x) else (y, x, z) else if z < x then (z, x, y) else if z < y then (x, z, y) else (x, y, z) in foldl (insert lt) [x, y, z] xs end fun group (lol, n) = let fun dup n = let fun loop (acc, i) = if i <= 0 then acc else loop ([] :: acc, i - 1) in loop ([], n) end fun loop ([], [], accj, lol') = List.revAppend (accj, lol') | loop (acci, [], accj, []) = loop ([], rev acci, [], rev accj) | loop (acci, [], accj, lol') = loop ([], rev acci, accj, lol') | loop (acci, lol, accj, []) = loop (acci, lol, [], rev accj) | loop (acci, [] :: ls, accj, lol') = loop (acci, ls, accj, lol') | loop (acci, (x :: xs) :: ls, accj, l' :: ls') = loop (xs :: acci, ls, (x :: l') :: accj, ls') in loop ([], lol, [], dup n) end val (lol, len) = foldl (fn (x, (l, n)) => ([x] :: l, n + 1)) ([], 0) (rev l) val incs = [1, 4, 9, 20, 46, 103, 233, 525, 1182, 2660, 5985, 13467, 30301, 68178, 153401, 345152, 776591, 1747331, 3931496, 8845866, 19903198, 44782196, 100759940, 226709866, 510097200] val gap = let val v = len * 3 div 4 val thold = if (v = 0) then 1 else v fun loop (acc, h) = if (hd h) > thold then acc else loop ((hd h) :: acc, tl h) in loop ([], incs) end fun sort (h, lol) = map insertSort (group (lol, h)) in hd (foldl sort lol gap) end 

这里采用的间隔序列是OEIS A108870,即 ,它是徳田尚之在1992年提出的[47]。这个序列用递推公式表示为:hk = ⌈h'k,这里的h'k = 2.25·h'k-1 + 1h'1 = 1。假定一个列表的长度s位于序列两个元素之间,即hk-1 < hk ≤ s < hk+1,如果hk ·s,这里的n ≤ m,则选择初始间隔为hk,否则为hk-1。在这个阈值下,对于不同长度s的列表和对应的初始间隔h,每个列表的这些初始子列表的平均长度 ,约在   <  · 范围之内。间隔序列还可以采用OEIS A102549,它是Marcin Ciura在2001年通过实验得到的[48][m]

快速排序

下面是快速排序算法的自顶向下实现:

fun quickSort [] = [] | quickSort [x] = [x] | quickSort [x, y] = if x <= y then [x, y] else [y, x] | quickSort [x, y, z] = let val (x, y) = if x <= y then (x, y) else (y, x) val (y, z) = if y <= z then (y, z) else (z, y) val (x, y) = if x <= y then (x, y) else (y, x) in [x, y, z] end | quickSort (pivot :: xs) = let fun partition pred l = let fun loop ([], p, q) = (p, q) | loop (h :: t, p, q) = if (pred h) then loop (t, h :: p, q) else loop (t, p, h :: q) in loop (l, [], []) end val (le, gt) = partition (fn x => (x <= pivot)) xs in (quickSort le) @ (pivot :: (quickSort gt)) end 

基本库partition函数实现对快速排序而言有不必要的反转,[n] 这里采用了它的简化改写。在ML中快速排序应采用自底向上实现:

fun quickSort l = let fun partition pred l = let fun loop ([], p, q) = (p, q) | loop (h :: t, p, q) = if (pred h) then loop (t, h :: p, q) else loop (t, p, h :: q) in loop (l, [], []) end fun iterate (acc, []) = acc | iterate (acc, [] :: xs) = iterate (acc, xs) | iterate (acc, [x] :: xs) = iterate (x :: acc, xs) | iterate (acc, [x, y] :: xs) = let val (x, y) = if x <= y then (x, y) else (y, x) in iterate (x :: y :: acc, xs) end | iterate (acc, [x, y, z] :: xs) = let val (x, y) = if x <= y then (x, y) else (y, x) val (x, y, z) = if y <= z then (x, y, z) else if x <= z then (x, z, y) else (z, x, y) in iterate (x :: y :: z :: acc, xs) end | iterate (acc, (pivot :: d) :: xs) = let val (le, gt) = partition (fn x => (x <= pivot)) d in iterate (acc, gt :: [pivot] :: le :: xs) end in iterate ([], [l]) end 

归并排序

下面是归并排序算法的自底向上法实现:

fun mergeSort l = let fun init (acc, []) = acc | init (acc, [x]) = [x] :: acc | init (acc, [x, y]) = if x <= y then [x, y] :: acc else [y, x] :: acc | init (acc, x :: y :: z :: xs) = let val (x, y, z) = if x <= y then if y <= z then (x, y, z) else if x <= z then (x, z, y) else (z, x, y) else if x <= z then (y, x, z) else if y <= z then (y, z, x) else (z, y, x) in init ([x, y, z] :: acc, xs) end fun mergeWith _ (acc, [], []) = acc | mergeWith _ (acc, p, []) = List.revAppend (p, acc) | mergeWith _ (acc, [], q) = List.revAppend (q, acc) | mergeWith cmp (acc, p :: ps, q :: qs) = if cmp (p, q) then mergeWith cmp (p :: acc, ps, q :: qs) else mergeWith cmp (q :: acc, p :: ps, qs) val mergeRev = mergeWith (fn (x, y) => (x > y)) val revMerge = mergeWith (fn (x, y) => (x < y)) fun iterate ([], _) = [] | iterate ([x], isRev) = if isRev then rev x else x | iterate (acc, isRev) = let val merge = if isRev then mergeRev else revMerge fun loop (acci, []) = acci | loop (acci, [x]) = (rev x) :: acci | loop (acci, x :: y :: xs) = loop (merge ([], x, y) :: acci, xs) in iterate (loop ([], acc), not isRev) end in iterate (init ([], l), false) end 

考虑输入列表[x1, ..., xi, a0, ..., a9, xj, ..., xn],这里在xixj之间的10a,具有相同的值并且需要保持其下标表示的次序,这里的xi > a并且xj < a,并且在这个区段前后的元素总数都能被3整除,则它被分解成子列表的列表[Xm, ..., [xj, a8, a9], [a5, a6, a7], [a2, a3, a4], [a0, a1, xi], ..., X1],这里有m = n div 3;假定这4个含有a的子列表两两归并,在归并正序子列表的归并条件x < y下,能得到[X1, ..., [xi, a4, ..., a0], [a9, ..., a5, xj], ..., Xk];继续推演下去,在归并反序子列表的归并条件x > y下,能得到[Xh, ..., [xj, a0, ..., a9, xi], ..., X1]。可以看出这种归并操作能够保证排序算法的稳定性,即具有相同值的元素之间的相对次序保持不变。

分解初始的子列表采用了插入排序,还可进一步增加其大小。归并排序也有自顶向下实现。[o]

堆排序

下面是堆排序的基于数组的实现:

fun heapSort l = let val h = Array.fromList l val len = Array.length h fun get i = Array.sub (h, i) fun set i v = Array.update (h, i, v) fun siftdown (i, ins, n) = let fun sift k = let val l = k * 2 + 1 val r = l + 1 in if (r < n) andalso (get r) > (get l) then r else if (l < n) then l else k end fun loop i = let val j = sift i in if j = i orelse (get j) <= ins then set i ins else (set i (get j); loop j) end in loop i end fun heapify () = let fun loop i = if i < 0 then () else (siftdown (i, get i, len); loop (i - 1)) in loop (len div 2 - 1) end fun generate () = let fun loop (acc, i) = let val t = get 0 in if i <= 0 then t :: acc else (siftdown (0, get i, i); loop (t :: acc, i - 1)) end in if len = 0 then [] else loop ([], len - 1) end in heapify (); generate () end 

在数组实现中,siftdown函数融合了插入和筛选功能,它首先在暂时位于堆顶的要插入的元素,和从堆顶节点左右子堆的两个堆顶元素中筛选出的那个元素,二者中选择出哪个适合作堆顶元素;如果要插入元素适合,则以它为新堆顶元素而结束整个过程,否则以筛选出元素为新堆顶元素,并自顶向下逐级处理提供了新堆顶元素的子堆,将要插入元素暂时作为其堆顶元素并对它继续进行siftdownsiftdown只要到达了某个堆底,就插入要插入的元素而结束整个过程。

在提取堆顶元素生成结果列表时,先提取走堆顶元素的内容,再摘掉最后的堆底元素将它的内容暂时放置在堆顶,这时堆的大小也相应的减一,随后的siftdown函数,筛选出新的堆顶元素,并把原最后堆底元素插入回堆中。

heapify函数建造堆的时候,首先自列表中间将元素分为前后两组,后组中的元素被视为只有一个元素的堆,然后从后往前处理前组中的元素,这时它的左右子节点已经是已有的堆或者为空,在其上进行siftdown,从而合成一个新堆。建造堆也可以采用siftup函数来实现,它自第二个元素开始从前往后逐个处理列表元素,其前面是已有的堆,将这个新元素自堆底向上插入到这个堆中。[p]

排序算法也可以使用二叉树数据结构来实现二叉堆

fun heapSort l = let datatype 'a heap = Nil | Leaf of 'a | Node of 'a * int * 'a heap * 'a heap fun key Nil = let val SOME a = Int.minInt in a end | key (Leaf k) = k | key (Node (k, _, _, _)) = k fun count Nil = 0 | count (Leaf _) = 1 | count (Node (_, c, _, _)) = c fun left Nil = Nil | left (Leaf _) = Nil | left (Node (_, _, l, _)) = l fun insert (Nil, x) = Leaf x | insert (Leaf k, l) = if l >= k then Node (l, 2, Leaf k, Nil) else Node (k, 2, Leaf l, Nil) | insert (Node (k, _, Leaf l, Nil), r) = if r >= k then Node (r, 3, Leaf k, Leaf l) else if r >= l then Node (k, 3, Leaf r, Leaf l) else Node (k, 3, Leaf l, Leaf r) | insert (Node (k, c, l, r), x) = let val (k, x) = if k >= x then (k, x) else (x, k) in if (count l) <= (count r) then Node (k, c + 1, insert (l, x), r) else if x >= (key l) then Node (k, c + 1, insert (r, x), l) else Node (k, c + 1, l, insert (r, x)) end fun extract Nil = Nil | extract (Leaf _) = Nil | extract (Node (_, _, l, Nil)) = l | extract (Node (_, c, l, r)) = let val k = key l val n = left l in if n = Nil then Node (k, c - 1, r, Nil) else if (key n) >= (key r) then Node (k, c - 1, extract l, r) else Node (k, c - 1, r, extract l) end fun heapify () = let fun loop (acc, []) = acc | loop (acc, x :: xs) = loop (insert (acc, x), xs) in loop (Nil, l) end fun generate h = let fun loop (acc, Nil) = acc | loop (acc, h) = loop ((key h) :: acc, extract h) in loop ([], h) end in generate (heapify ()) end 

二叉树实现不能直接访问堆底元素,从而不适宜通过摘掉它使堆的大小减一。这里的insert函数,在原堆顶元素和要插入元素中选择适合者作为新的堆顶元素,将落选的另一个元素作为新的要插入元素,插入到利于保持这个堆平衡的那个子树之中。这里的extract函数只筛选不插入,它将堆的大小减一。

这里的insertextract函数也可以直接转写为等价的尾递归形式,与列表情况不同,只要树结构能保持良好的平衡,采用尾递归形式就没有太大的必要性。[q] 在二叉树实现下,也可以采用siftdown函数来初始建造堆,而不需要在节点中保存关于树状态的统计信息。[r]

基数排序

下面是针对非负整数基数排序算法的实现:

fun radixSort l = let fun distribute (l, d) = let val t0 = ([], [], [], [], [], [], [], []) fun loop (t, []) = let fun join (acc, i) = let val f = case i of 1 => (#1 t) | 2 => (#2 t) | 3 => (#3 t) | 4 => (#4 t) | 5 => (#5 t) | 6 => (#6 t) | 7 => (#7 t) | 8 => (#8 t) | _ => [] in if i <= 0 then acc else join (List.revAppend (f, acc), i - 1) end in join ([], 8) end | loop (t, x :: xs) = let val (f0, f1, f2, f3, f4, f5, f6, f7) = t val t = case ((x div d) mod 8) of 0 => (x :: f0, f1, f2, f3, f4, f5, f6, f7) | 1 => (f0, x :: f1, f2, f3, f4, f5, f6, f7) | 2 => (f0, f1, x :: f2, f3, f4, f5, f6, f7) | 3 => (f0, f1, f2, x :: f3, f4, f5, f6, f7) | 4 => (f0, f1, f2, f3, x :: f4, f5, f6, f7) | 5 => (f0, f1, f2, f3, f4, x :: f5, f6, f7) | 6 => (f0, f1, f2, f3, f4, f5, x :: f6, f7) | 7 => (f0, f1, f2, f3, f4, f5, f6, x :: f7) | _ => t0 in loop (t, xs) end in loop (t0, l) end val SOME maxInt = Int.maxInt val max = foldl (fn (x, y) => if x > y then x else y) 0 l fun iterate (l, d) = let val l' = distribute (l, d) in if d >= (maxInt div 8 + 1) orelse ((max div d) div 8) = 0 then l' else iterate (l', d * 8) end in iterate (l, 1) end 

这里采用的基数238,代码所使用的列表元组大小与基数大小成正比,运算量与列表中元素的总数与最大数的位数的乘积成正比。

随机数生成

编写排序算法进行测试除了使用简单的数列,[s] 测试用列表还可以使用线性同余伪随机数函数来生成[49]

fun randList (n, seed) = let val randx = ref seed fun lcg () = (randx := (!randx * 421 + 1663) mod 7875; !randx) (* fun lcg () = (randx := (!randx * 1366 + 150889) mod 714025; !randx) *) fun iterate (acc, i) = if i <= 0 then acc else iterate (lcg () :: acc, i - 1) in iterate ([], n) end 

语言解释器

定义和处理一个小型表达式语言是相对容易的:

exception Err; datatype ty = IntTy | BoolTy datatype exp = True | False | Int of int | Not of exp | Add of exp * exp | If of exp * exp * exp fun typeOf (True) = BoolTy | typeOf (False) = BoolTy | typeOf (Int _) = IntTy | typeOf (Not e) = if typeOf e = BoolTy then BoolTy else raise Err | typeOf (Add (e1, e2)) = if (typeOf e1 = IntTy) andalso (typeOf e2 = IntTy) then IntTy else raise Err | typeOf (If (e1, e2, e3)) = if typeOf e1 <> BoolTy then raise Err else if typeOf e2 <> typeOf e3 then raise Err else typeOf e2 fun eval (True) = True | eval (False) = False | eval (Int n) = Int n | eval (Not e) = (case eval e of True => False | False => True | _ => raise Fail "type-checking is broken") | eval (Add (e1, e2)) = let val (Int n1) = eval e1 val (Int n2) = eval e2 in Int (n1 + n2) end | eval (If (e1, e2, e3)) = if eval e1 = True then eval e2 else eval e3 fun exp_repr e = let val msg = case e of True => "True" | False => "False" | Int n => Int.toString n | _ => "" in msg ^ "\n" end (* 忽略TypeOf的返回值,它在类型错误时发起Err *) fun evalPrint e = (ignore (typeOf e); print (exp_repr (eval e))); 

将这段代码录入文件比如expr-lang.sml,并在命令行下执行sml expr-lang.sml,可以用如下在正确类型的和不正确类型上运行的例子,测试这个新语言:

- val e1 = Add (Int 1, Int 2); (* 正确的类型 *) val e1 = Add (Int 1,Int 2) : exp - val _ = evalPrint e1; 3 - val e2 = Add (Int 1, True); (* 不正确的类型 *) val e2 = Add (Int 1,True) : exp - val _ = evalPrint e2; uncaught exception Err raised at: expr-lang.sml:25.20-25.23 

注释和附录代码

  1. ^ 子句集合是穷尽和不冗余的函数示例:
    fun hasCorners (Circle _) = false | hasCorners _ = true 

    如果控制通过了第一个模式Circle,则这个值必定是要么Square要么Triangle。在任何这些情况下,这个形状都有角点,所以返回true而不用区分具体是那种情况。

  2. ^ 不详尽的模式示例:
    fun center (Circle (c, _)) = c | center (Square ((x, y), s)) = (x + s / 2.0, y + s / 2.0) 

    这里在center函数中没有给Triangle的模式。 编译器发起模式不详尽的一个警告,并且如果在运行时间,Triangle被传递给这个函数,则发起异常Match

  3. ^ 存在模式冗余的(无意义)函数示例:
    fun f (Circle ((x, y), r)) = x+y | f (Circle _) = 1.0 | f _ = 0.0 

    匹配第二个子句的模式的任何值都也匹配第一个子句的模式,所以第二个子句是不可到达的。因此这个定义整体上是冗余的。

  4. ^ 映射函数的实际实现:
    fun map f = let fun m [] = [] | m [a] = [f a] | m [a, b] = [f a, f b] | m [a, b, c] = [f a, f b, f c] | m (a :: b :: c :: d :: r) = f a :: f b :: f c :: f d :: m r in m end 

    折叠函数的实际实现:

    fun foldl f b l = let fun f2 ([], b) = b | f2 (a :: r, b) = f2 (r, f (a, b)) in f2 (l, b) end fun foldr f b l = foldl f b (rev l) 

    过滤器函数的实际实现:

    fun filter pred [] = [] | filter pred (a :: rest) = if pred a then a :: (filter pred rest) else (filter pred rest) 
  5. ^ 对分数采取修约的有理数实现:
    signature ARITH = sig eqtype t val zero : t val one : t val fromInt: int -> t val fromIntPair : int * int -> t val repr : t -> unit val succ : t -> t val pred : t -> t val ~ : t -> t val + : t * t -> t val - : t * t -> t val * : t * t -> t val / : t * t -> t end 
    structure Rational : ARITH = struct type t = int * int val zero = (0, 1) val one = (1, 1) val maxInt = (let val SOME a = Int.maxInt in Int.toLarge a end) fun fromInt n = (n, 1) fun neg (a, b) = (~a, b) fun fromLargePair (a, b) = (Int.fromLarge a, Int.fromLarge b) fun fromIntPair (num, den) = let fun reduced_fraction (numerator, denominator) = let fun gcd (n, 0) = n | gcd (n, d) = gcd (d, n mod d) val d = gcd (numerator, denominator) in if d > 1 then (numerator div d, denominator div d) else (numerator, denominator) end in if num < 0 andalso den < 0 then reduced_fraction (~num, ~den) else if num < 0 then neg (reduced_fraction (~num, den)) else if den < 0 then neg (reduced_fraction (num, ~den)) else reduced_fraction (num, den) end fun repr (a, b) = let val m = if (b = 0) then 0 else if (a >= 0) then a div b else ~a div b val n = if (b = 0) then 1 else if (a >= 0) then a mod b else ~a mod b val ms = Int.toString m and ns = Int.toString n and bs = Int.toString b in if n <> 0 andalso m <> 0 andalso a < 0 then print ("~" ^ ms ^ " - " ^ ns ^ "/" ^ bs ^ "\n") else if n <> 0 andalso m <> 0 then print (ms ^ " + " ^ ns ^ "/" ^ bs ^ "\n") else if n <> 0 andalso m = 0 andalso a < 0 then print ("~" ^ ns ^ "/" ^ bs ^ "\n") else if n <> 0 andalso m = 0 then print (ns ^ "/" ^ bs ^ "\n") else if a < 0 then print ("~" ^ ms ^ "\n") else print (ms ^ "\n") end fun convergent (i, n, d, h_1, k_1, h_2, k_2) = if i <> 0 andalso ((h_1 > (maxInt - h_2) div i) orelse (k_1 > (maxInt - k_2) div i)) then (h_1, k_1) else if n = 0 then (i * h_1 + h_2, i * k_1 + k_2) else convergent (d div n, d mod n, n, i * h_1 + h_2, i * k_1 + k_2, h_1, k_1) fun add ((a, b), (c, d)) = let val la = Int.toLarge a and lb = Int.toLarge b val lc = Int.toLarge c and ld = Int.toLarge d val m = la * ld + lb * lc and n = lb * ld in if b = d then fromIntPair (a + c, b) else fromLargePair (convergent (m div n, m mod n, n, 1, 0, 0, 1)) end fun sub ((a, b), (c, d)) = let val la = Int.toLarge a and lb = Int.toLarge b val lc = Int.toLarge c and ld = Int.toLarge d val m = la * ld - lb * lc and n = lb * ld in if b = d then fromIntPair (a - c, b) else if m < 0 then neg (fromLargePair (convergent (~m div n, ~m mod n, n, 1, 0, 0, 1))) else if m > 0 then fromLargePair (convergent (m div n, m mod n, n, 1, 0, 0, 1)) else (0, 1) end fun mul ((a, b), (c, d)) = let val la = Int.toLarge a and lb = Int.toLarge b val lc = Int.toLarge c and ld = Int.toLarge d val m = la * lc and n = lb * ld in fromLargePair (convergent (m div n, m mod n, n, 1, 0, 0, 1)) end fun op + ((a, b), (c, d)) = if a < 0 andalso c < 0 then neg (add ((~a, b), (~c, d))) else if a < 0 then sub ((c, d), (~a, b)) else if c < 0 then sub ((a, b), (~c, d)) else add ((a, b), (c, d)) fun op - ((a, b), (c, d)) = if a < 0 andalso c < 0 then sub ((~c, d), (~a, b)) else if a < 0 then neg (add ((~a, b), (c, d))) else if c < 0 then add ((a, b), (~c, d)) else sub ((a, b), (c, d)) fun op * ((a, b), (c, d)) = if a < 0 andalso c < 0 then mul ((~a, b), (~c, d)) else if a < 0 then neg (mul ((~a, b), (c, d))) else if c < 0 then neg (mul ((a, b), (~c, d))) else mul ((a, b), (c, d)) fun op / ((a, b), (c, d)) = if a < 0 andalso c < 0 then mul ((~a, b), (d, ~c)) else if a < 0 then neg (mul ((~a, b), (d, c))) else if c < 0 then neg (mul ((a, b), (d, ~c))) else mul ((a, b), (d, c)) fun succ a = add (a, one) fun pred a = sub (a, one) fun ~ a = neg a end 
  6. ^ 找出函数的实际实现:
    fun find pred [] = NONE | find pred (a :: rest) = if pred a then SOME a else (find pred rest) 

    存在谓词函数的实际实现:

     fun exists pred = let fun f [] = false | f (h :: t) = pred h orelse f t in f end 
  7. ^ 筛法基于数组的实现:
    fun prime n = let val sieve = Array.array (n + 1, true); fun markComposite (j, i) = if j > n then () else (Array.update (sieve, j, false); markComposite (j + i, i)) fun iterate i = if i * i > n then () else if Array.sub (sieve, i) then (markComposite (i * i, i); iterate (i + 1)) else iterate (i + 1) fun generate (acc, i) = if i < 2 then acc else if Array.sub (sieve, i) then generate (i :: acc, i - 1) else generate (acc, i - 1) in if n < 2 then [] else (iterate 2; generate ([], n)) end 
  8. ^ 汉明数进一步性质演示代码:
    fun printIntList (l: int list) = print ((String.concatWith " " (map Int.toString l)) ^ "\n"); fun diff (p, q) = let fun revDiff (acc, p, q) = if not (null p) andalso not (null q) then if hd p < hd q then revDiff ((hd p) :: acc, tl p, q) else if hd p > hd q then revDiff (acc, p, tl q) else revDiff (acc, tl p, tl q) else if null q then List.revAppend (p, acc) else acc in if (null p) then [] else if (null q) then p else rev (revDiff ([], p, q)) end; fun Hamming_number n = let fun merge (p, q) = let fun revMerge (acc, p, q) = if not (null p) andalso not (null q) then if hd p < hd q then revMerge ((hd p) :: acc, tl p, q) else if hd p > hd q then revMerge ((hd q) :: acc, p, tl q) else revMerge ((hd p) :: acc, tl p, tl q) else if null p then List.revAppend (q, acc) else List.revAppend (p, acc) in if (null p) then q else if (null q) then p else rev (revMerge ([], p, q)) end fun mergeWith f (m, i) = merge (f m, i) fun mul m x = (x * m) fun generate l = let fun listMul m = map (mul m) l in printIntList (listMul 2); printIntList (diff (listMul 3, listMul 2)); printIntList (diff (listMul 5, merge (listMul 2, listMul 3))); foldl (mergeWith listMul) [] [2, 3, 5] end val count = ref 1; fun iterate (acc, l) = if (hd l) > (n div 2) then merge (l, acc) else (print ("round " ^ (Int.toString (!count)) ^ " for " ^ (Int.toString(length l)) ^ " number(s)\n"); count := !count + 1; iterate (merge (l, acc), generate l)) in if n > 0 then iterate ([], [1]) else [] end; 
    val l = Hamming_number 400; val h = List.filter (fn x => (x <= 400)) l; val _ = print ((Int.toString (length h)) ^ " numbers from " ^ (Int.toString (length l)) ^ " numbers\n"); 
  9. ^ 部份映射函数的实际实现:
    fun mapPartial pred l = let fun mapp ([], l) = rev l | mapp (x :: r, l) = (case (pred x) of SOME y => mapp (r, y :: l) | NONE => mapp (r, l) (* end case *)) in mapp (l, []) end 
  10. ^ 列表长度函数的实际实现:
    fun length l = let (* fast add that avoids the overflow test *) val op + = Int.fast_add fun loop (n, []) = n | loop (n, [_]) = n + 1 | loop (n, _ :: _ :: l) = loop (n + 2, l) in loop (0, l) end 
  11. ^ 变体的插入排序算法实现:
    fun insertSort l = let fun insert pred (ins, l) = let fun loop (acc, []) = List.revAppend (acc, [ins]) | loop (acc, l as x :: xs) = if pred (ins, x) then List.revAppend (acc, ins :: l) else loop (x :: acc, xs) in loop ([], l) end val rec lt = fn (x, y) => (x < y) in foldl (insert lt) [] l end 
  12. ^ 下面是希尔排序算法的原型实现,当输入列表趋于正序的时候,scatter函数将其分解为一组趋于反序的子列表,经过在输入趋于反序情况下性能最佳的变体插入排序后,gather函数再将它们合成为一个列表:
    fun shellSort l = let fun insert pred (ins, l) = let fun loop (acc, []) = List.revAppend (acc, [ins]) | loop (acc, l as x :: xs) = if pred (ins, x) then List.revAppend (acc, ins :: l) else loop (x :: acc, xs) in loop ([], l) end val rec lt = fn (x, y) => (x < y) fun insertSort l = foldl (insert lt) [] l fun scatter (l, n) = let fun dup n = let fun loop (acc, i) = if i <= 0 then acc else loop ([] :: acc, i - 1) in loop ([], n) end fun loop ([], acc, lol) = List.revAppend (acc, lol) | loop (l, acc, []) = loop (l, [], rev acc) | loop (x :: xs, acc, l :: ls) = loop (xs, (x :: l) :: acc, ls) in loop (l, [], dup n) end fun gather lol = let fun loop ([], [], l) = rev l | loop (acc, [], l) = loop ([], rev acc, l) | loop (acc, [] :: ls, l) = loop (acc, ls, l) | loop (acc, (x :: xs) :: ls, l) = loop (xs :: acc, ls, x :: l) in loop ([], lol, []) end val gap = let fun loop (acc, i) = let val h = (i * 5 - 1) div 11 in if i < 5 then rev (1 :: acc) else loop (h :: acc, h) end in loop ([], length l) end fun sort (h, l) = gather (map insertSort (scatter (l, h))) in foldl sort l gap end 
  13. ^ 希尔排序还可以采用Ciura提出的间隔序列:
     val incs = [1750, 701, 301, 132, 57, 23, 10, 4, 1] val gap = let fun loop (acc, i) = let val h = (i * 4 - 1) div 9 fun iter incs = if i >= (hd incs) * 4 div 3 then incs else iter (tl incs) in if i <= ((hd incs) * 3) then List.revAppend (acc, iter incs) else loop (h :: acc, h) end in if len = 0 then [1] else loop ([], len) end 
  14. ^ 划分函数的实际实现:
    fun partition pred l = let fun loop ([], trueList, falseList) = (rev trueList, rev falseList) | loop (h :: t, trueList, falseList) = if pred h then loop (t, h :: trueList, falseList) else loop (t, trueList, h :: falseList) in loop (l, [], []) end 
  15. ^ 归并排序算法的自顶向下实现:
    fun mergeSort l = let fun sort ([], _) = [] | sort ([x], _) = [x] | sort ([x, y], _) = if x <= y then [x, y] else [y, x] | sort ([x, y, z], _) = if x <= y then if y <= z then [x, y, z] else if x <= z then [x, z, y] else [z, x, y] else if x <= z then [y, x, z] else if y <= z then [y, z, x] else [z, y, x] | sort (l, n) = let val m = n div 2 fun split (l, acc, i) = if i = 0 then (rev acc, l) else split (tl l, (hd l) :: acc, i - 1) fun merge (p, q) = let fun revMerge (acc, p, q) = if not (null p) andalso not (null q) then if (hd p) <= (hd q) then revMerge ((hd p) :: acc, tl p, q) else revMerge ((hd q) :: acc, p, tl q) else if null p then List.revAppend (q, acc) else List.revAppend (p, acc) in rev (revMerge ([], p, q)) end val (ls, rs) = split (l, [], m) in merge (sort (ls, m), sort (rs, n - m)) end in sort (l, length l) end 
  16. ^ 堆排序算法的数组实现中,堆建造函数heapify也可以使用siftup函数的数组来完成,它将新节点自堆底向上插入到合适的位置,而不对途径节点左右子树顶点进行比较:
     fun siftup i = let val ins = get i fun loop i = let val j = (i - 1) div 2 in if i <= 0 orelse (get j) >= ins then set i ins else (set i (get j); loop j) end in loop i end fun heapify () = let fun loop i = if i > (len - 1) then () else (siftup i; loop (i + 1)) in loop 1 end 
  17. ^ 在堆排序算法的二叉树实现中,树插入和提取函数也可以写为等价的尾递归形式代码:
     exception Err; fun revLink ([], t) = t | revLink (Nil :: xs, t) = revLink (xs, t) | revLink ((Leaf k) :: xs, t) = revLink (xs, Node (k, (count t) + 1, t, Nil)) | revLink (Node (k, c, Nil, r) :: xs, t) = revLink (xs, Node (k, c, t, r)) | revLink (Node (k, c, l, Nil) :: xs, t) = revLink (xs, Node (k, c, l, t)) | revLink (_ :: xs, t) = raise Err fun insert (t, x) = let fun loop (acc, Nil, x) = revLink (acc, Leaf x) | loop (acc, Leaf k, l) = if l >= k then revLink (acc, Node (l, 2, Leaf k, Nil)) else revLink (acc, Node (k, 2, Leaf l, Nil)) | loop (acc, Node (k, _, Leaf l, Nil), r) = if r >= k then revLink (acc, Node (r, 3, Leaf k, Leaf l)) else if r >= l then revLink (acc, Node (k, 3, Leaf r, Leaf l)) else revLink (acc, Node (k, 3, Leaf l, Leaf r)) | loop (acc, Node (k, c, l, r), x) = let val (k, x) = if k >= x then (k, x) else (x, k) in if (count l) <= (count r) then loop (Node (k, c + 1, Nil, r) :: acc, l, x) else if x >= (key l) then loop (Node (k, c + 1, Nil, l) :: acc, r, x) else loop (Node (k, c + 1, l, Nil) :: acc, r, x) end in loop ([], t, x) end fun extract t = let fun loop (acc, Nil) = revLink (acc, Nil) | loop (acc, Leaf _) = revLink (acc, Nil) | loop (acc, Node (_, _, l, Nil)) = revLink (acc, l) | loop (acc, Node (_, c, l, r)) = let val k = key l val n = left l in if n = Nil then revLink (acc, Node (k, c - 1, r, Nil)) else if (key n) >= (key r) then loop (Node (k, c - 1, Nil, r) :: acc, l) else loop (Node (k, c - 1, r, Nil) :: acc, l) end in loop ([], t) end 
  18. ^ 堆排序算法的二叉树实现中,堆建造函数也可以主要采用siftdown函数来完成,这里不需要在节点中保存关于树状态的统计信息:
    fun heapSort l = let datatype 'a heap = Nil | Node of 'a * 'a heap * 'a heap fun key Nil = let val SOME a = Int.minInt in a end | key (Node (k, _, _)) = k fun left Nil = Nil | left (Node (_, l, _)) = l fun right Nil = Nil | right (Node (_, _, r)) = r fun leaf k = Node (k, Nil, Nil) fun sift (l, r) = if l <> Nil andalso r <> Nil then if (key l) >= (key r) then l else r else if l <> Nil then l else if r <> Nil then r else Nil fun siftdown (x, l, r) = let val superior = sift (l, r) in if superior = Nil then Node (x, Nil, Nil) else if x >= (key superior) then Node (x, l, r) else if superior = l then Node (key l, siftdown (x, left l, right l), r) else Node (key r, l, siftdown (x, left r, right r)) end fun insert (Nil, x) = Node (x, Nil, Nil) | insert (Node (k, l, r), x) = let val superior = sift (l, r) in if x >= k andalso superior = l then Node (x, l, insert (r, k)) else if x >= k then Node (x, insert (l, k), r) else if superior = l then Node (k, l, insert (r, x)) else Node (k, insert (l, x), r) end fun extract Nil = Nil | extract (Node (_, l, r)) = let val superior = sift (l, r) in if superior = Nil then Nil else if superior = l then Node (key l, extract l, r) else Node (key r, l, extract r) end fun join (l, r) = extract (Node (key Nil, l, r)) fun heapify () = let fun init (hs, ls, [], _) = (hs, ls) | init (hs, ls, x :: xs, flag) = if flag then init ((leaf x) :: hs, ls, xs, false) else init (hs, x :: ls, xs, true) val (hs, ls) = init ([], [], l, true) fun loop ([], [], []) = Nil | loop ([], [h], []) = h | loop ([], [], x :: xs) = loop ([], [leaf x], xs) | loop ([], [h], x :: xs) = loop ([], [insert (h, x)], xs) | loop (acc, [], l) = loop ([], acc, l) | loop (acc, [h], l) = loop ([], h :: acc, l) | loop (acc, l :: r :: hs, []) = loop (join (l, r) :: acc, hs, []) | loop (acc, l :: r :: hs, x :: xs) = loop (siftdown (x, l, r) :: acc, hs, xs) in loop ([], hs, ls) end fun generate h = let fun loop (acc, Nil) = acc | loop (acc, h) = loop ((key h) :: acc, extract h) in loop ([], h) end in generate (heapify ()) end 

    稍加处理,堆建造函数也可以只用siftdown函数来完成:

     fun heapify () = let exception Err; fun split () = let val (rs, ts) = let fun loop (acci, accj, [], i, n) = if i = n then (List.revAppend (accj, acci), []) else (acci, accj) | loop (acci, accj, x :: xs, i, n) = if i = n then loop (List.revAppend (accj, acci), [x], xs, i + 1, n * 2 + 1) else loop (acci, x :: accj, xs, i + 1, n) in loop ([], [], l, 0, 1) end fun loop (hs, ls, [], _) = (hs, ls, ts) | loop (hs, ls, x :: xs, flag) = if flag then loop (x :: hs, ls, xs, false) else loop (hs, x :: ls, xs, true) in loop ([], [], rs, true) end fun init () = let val (hs, ls, ts) = split () fun loop (acc, [], []) = (acc, ls) | loop (acc, [], ts) = (acc, List.revAppend (ts, ls)) | loop (acc, k :: hs, []) = loop ((leaf k) :: acc, hs, []) | loop (acc, k :: hs, [x]) = let val (k, x) = if k >= x then (k, x) else (x, k) in loop (Node (k, leaf x, Nil) :: acc, hs, []) end | loop (acc, k :: hs, l :: r :: rs) = let val (k, l, r) = if k >= l then if l >= r then (k, l, r) else if k >= r then (k, r, l) else (r, k, l) else if k >= r then (l, k, r) else if l >= r then (l, r, k) else (r, l, k) in loop (Node (k, leaf l, leaf r) :: acc, hs, rs) end in loop ([], hs, ts) end val (hs, ls) = init () fun loop ([], [], []) = Nil | loop ([], [h], []) = h | loop ([], [], _) = raise Err | loop ([], [h], _) = raise Err | loop (acc, [], l) = loop ([], acc, l) | loop (acc, [h], l) = loop ([], h :: acc, l) | loop (acc, l :: r :: hs, []) = raise Err | loop (acc, l :: r :: hs, x :: xs) = loop (siftdown (x, l, r) :: acc, hs, xs) in loop ([], hs, ls) end 
  19. ^ 排序算法的简单测试代码:
    fun printIntList (l: int list) = print ((String.concatWith " " (map Int.toString l)) ^ "\n") fun shuffle (l, n) = let fun split (l, acc, i) = if i = 0 then (acc, l) else split (tl l, (hd l) :: acc, i - 1) fun zip (acc, p, q, flag) = if null p then List.revAppend (q, acc) else if null q then List.revAppend (p, acc) else if flag then zip ((hd p) :: acc, tl p, q, false) else zip ((hd q) :: acc, p, tl q, true) val (p, q) = split (l, [], n div 2) in if (null l) then tl [0] else zip ([], p, q, true) end fun testsort f n = let fun loop (acc, i) = if (i <= 0) then acc else loop (i :: acc, i - 1) val sl = shuffle (loop ([], n), n) val ssl = shuffle (sl, n) in print ("source list is: "); printIntList ssl; print ("result list is: "); printIntList (f ssl) end 

参见

延伸阅读

  • Robin Milner, Mads Tofte英语Mads Tofte, Robert Harper英语Robert Harper (computer scientist). (PDF). MIT Press. 1990 [2021-03-01]. (原始内容 (PDF)存档于2021-01-14). 
  • Robin Milner, Mads Tofte英语Mads Tofte, Robert Harper英语Robert Harper (computer scientist), David MacQueen. (PDF). MIT Press. 1997 [2021-03-01]. ISBN 0-262-63181-4. (原始内容 (PDF)存档于2022-03-09). 
  • Robin Milner, Mads Tofte英语Mads Tofte. . MIT Press. 1991 [2021-08-31]. ISBN 978-0-262-63137-2. (原始内容存档于2021-08-31). 
  • Emden R. Gansner, John H. Reppy. (PDF). Cambridge University Press. 2004 [2021-09-17]. (原始内容 (PDF)存档于2022-01-29). 
  • Mads Tofte英语Mads Tofte. (PDF). University of Edinburgh. 1989 [2021-09-04]. (原始内容 (PDF)存档于2022-01-28).  . [2021-09-11]. 原始内容存档于2016-04-02. 
  • Mads Tofte英语Mads Tofte. . DIKU英语UCPH Department of Computer Science. 1996 [2021-09-04]. (原始内容存档于2021-09-04).  . [2021-09-18]. 原始内容存档于2005-03-07. 
  • Mads Tofte英语Mads Tofte. (PDF). ITU英语IT University of Copenhagen. 2009 [2021-09-04]. (原始内容 (PDF)存档于2021-11-27).  . [2022-01-03]. 原始内容存档于2017-09-15. 
  • Robert Harper英语Robert Harper (computer scientist). (PDF). Carnegie Mellon University. 2011 [2021-02-27]. (原始内容 (PDF)存档于2020-02-15).  . [2021-09-12]. (原始内容存档于2021-09-12). 
  • Michael J. C. Gordon英语Michael J. C. Gordon. . Cambridge University. 1996 [2021-09-11]. (原始内容存档于2021-04-11).  . [2021-09-11]. (原始内容存档于2006-06-23). 
  • Lawrence Paulson英语Lawrence Paulson. . Cambridge University Press. 1996 [2021-08-31]. ISBN 0-521-56543-X. (原始内容存档于2022-02-24).  . [2021-09-12]. (原始内容存档于2022-01-19). 
  • David MacQueen. (PDF). 2002 [2021-09-10]. (原始内容 (PDF)存档于2021-10-29). 
  • David MacQueen, Robert Harper英语Robert Harper (computer scientist), John Reppy. . 2020 [2021-08-31]. (原始内容存档于2021-12-01). 
  • Andrew W. Appel英语Andrew W. Appel. . Cambridge University Press. 1992 [2022-01-03]. (原始内容存档于2022-01-03). 
  • Andrew W. Appel英语Andrew W. Appel. . Cambridge University Press. 1998 [2022-01-12]. (原始内容存档于2022-01-12).  . [2021-09-12]. (原始内容存档于2022-05-06). 
  • Jeffrey D. Ullman. . Prentice-Hall. 1998 [2021-12-30]. ISBN 0-13-790387-1. (原始内容存档于2022-03-12).  . [2022-01-01]. (原始内容存档于2022-02-14). 
  • Anthony L. Shipman. (PDF). 2001 [2021-09-01]. (原始内容 (PDF)存档于2021-01-21). 

引用

  1. ^ 1.0 1.1 1.2 1.3 Michael J. Gordon, Arthur J. Milner, Christopher P. Wadsworth. . Lecture Notes in Computer Science, Vol. 78. Springer-Verlag, New York, NY, USA. 1979 [2021-12-28]. (原始内容存档于2021-12-28). ML is a general purpose programming language. It is derived in different aspects from ISWIM, POP2 and GEDANKEN, and contains perhaps two new features. First, it has an escape and escape trapping mechanism, well-adapted to programming strategies which may be (in fact usually are) inapplicable to certain goals. Second, it has a polymorphic type discipline which combines the flexibility of programming in a typeless language with the security of compile-time type checking (as in other languages, you may also define your own types, which may be abstract and/or recursive); this is what ensures that a well-typed program cannot perform faulty proofs. 
    Michael J. C. Gordon英语Michael J. C. Gordon. . 1996 [2021-02-27]. (原始内容存档于2016-09-05). Around 1973 Milner moved to Edinburgh University and established a project to build a successor to Stanford LCF, which was subsequently dubbed Edinburgh LCF. He initially hired Lockwood Morris and Malcolm Newey (both recent PhD graduates from Stanford) as research assistants. …… Milner, ably assisted by Morris and Newey, designed the programming language ML (an abbreviation for “Meta Language”). …… In 1975, Morris and Newey took up faculty positions at Syracuse University and the Australian National University, respectively, and were replaced by Chris Wadsworth and myself. The design and implementation of ML and Edinburgh LCF was finalised and the book “Edinburgh LCF” was written and published. In 1978, the first LCF project finished, Chris Wadsworth went off trekking in the Andes (returning to a permanent position at the Rutherford Appleton Laboratory) and I remained at Edinburgh supported by a postdoctoral fellowship and with a new research interest: hardware verification. 
  2. ^ 2.0 2.1 M. Gordon, R. Milner, L. Morris, M. Newey, C. Wadsworth. (PDF). 1978 [2021-08-31]. (原始内容 (PDF)存档于2021-05-06). ML is a higher-order functional programming language in the tradition of ISWIM, PAL, POP2 and GEDANKEN, but differs principally in its handling of failure and, more so, of types. 
  3. ^ 3.0 3.1 Bruce A. Tate, Fred Daoud, Ian Dees, Jack Moffitt. 3. Elm. (PDF) Book version: P1.0-November 2014. The Pragmatic Programmers, LLC. 2014: 97, 101 [2021-09-04]. ISBN 978-1-941222-15-7. (原始内容 (PDF)存档于2021-03-15). On page 101, Elm creator Evan Czaplicki says: 'I tend to say "Elm is an ML-family language" to get at the shared heritage of all these languages.' ["these languages" is referring to Haskell, OCaml, SML, and F#.] 
  4. ^ 4.0 4.1 Troels Henriksen, Niels G. W. Serup, Martin Elsman, Fritz Henglein, Cosmin Oancea. (PDF). Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation. PLDI 2017. ACM. 2017 [2021-09-04]. (原始内容 (PDF)存档于2020-09-20). 
  5. ^ Lennart Augustsson英语Lennart Augustsson, Thomas Johnsson. . 1989 [2021-09-17]. (原始内容存档于2021-09-17). 
  6. ^ 6.0 6.1 , Russian Software Development Network: Nemerle Project Team, [January 24, 2021], (原始内容存档于2021-05-04) 
  7. ^ 7.0 7.1 Adam Chlipala. (PDF). MIT / Association for Computing Machinery (ACM). January 2015 [2021-09-04]. (原始内容 (PDF)存档于2022-01-16). 
  8. ^ 8.0 8.1 Robin Milner. (PDF). 1978 [2021-09-01]. (原始内容 (PDF)存档于2020-11-01).  Journal of Computer and System Sciences, 17(3):348–375.
  9. ^ Robin Milner. (PDF). Polymorphism—The ML/LCF/Hope Newsletter,Vol. 1, No. 1. 1982 [2021-09-09]. (原始内容 (PDF)存档于2022-01-28). 
  10. ^ . 1977 [2021-10-10]. (原始内容存档于2021-10-10). 
  11. ^ Luca Cardelli英语Luca Cardelli. (PDF). 1982 [2021-09-04]. (原始内容 (PDF)存档于2021-11-06). 
  12. ^ Luca Cardelli. (PDF). 1982 [2021-09-04]. (原始内容 (PDF)存档于2021-11-06). 
  13. ^ Luca Cardelli英语Luca Cardelli. . 1983 [2021-09-04]. (原始内容存档于2021-09-04).  Bell Labs Technical Report TR-107.
    Luca Cardelli. . 1984 [2021-09-03]. (原始内容存档于2021-09-03).  In Proceedings of the 1984 ACM Symposium on LISP and Functional Programming, pages 208–217, New York, NY, USA. ACM.
  14. ^ Kevin Mitchell, Alan Mycroft. (PDF). 1985 [2021-09-10]. (原始内容 (PDF)存档于2022-01-29). 
  15. ^ 15.0 15.1 Guy Cousineau, Gérard Huet英语Gérard Huet. . 1990 [2021-09-02]. (原始内容存档于2022-05-04).  RT-0122, INRIA. pp.78.
    Pierre Weis, Maria Virginia Aponte, Alain Laville, Michel Mauny, Ascander Suarez. . 1990 [2021-09-02]. (原始内容存档于2022-04-06).  [Research Report] RT-0121, INRIA. pp.491.
  16. ^ G. Cousineau, M. Gordon, G. Huet, R. Milner, L. C. Paulson, C. Wadsworth. The ML Handbook, Version 6.2. Internal document. Project Formel, INRIA. July 1985. 
    Christoph Kreitz, Vincent Rahli. (PDF). 2011 [2021-09-09]. (原始内容 (PDF)存档于2022-01-29). This handbook is a revised edition of Section 2 of ‘Edinburgh LCF’, by M. Gordon, R. Milner, and C. Wadsworth, published in 1979 as Springer Verlag Lecture Notes in Computer Science no 78. ……The language is somewhere in between the original ML from LCF and standard ML, since Guy Cousineau added the constructors and call by patterns. This is a LISP based implementation, compatible for Maclisp on Multics, Franzlisp on VAX under Unix, Zetalisp on Symbolics 3600, and Le Lisp on 68000, VAX, Multics, Perkin-Elmer, etc... Video interfaces have been implemented by Philippe Le Chenadec on Multics, and by Maurice Migeon on Symbolics 3600. The ML system is maintained and distributed jointly by INRIA and the University of Cambridge. 
  17. ^ 17.0 17.1 . [2021-08-31]. (原始内容存档于2022-04-13). The Formel team became interested in the ML language in 1980-81. ……Gérard Huet decided to make the ML implementation compatible with various Lisp compilers (MacLisp, FranzLisp, LeLisp, ZetaLisp). This work involved Guy Cousineau and Larry Paulson. ……Guy Cousineau also added algebraic data types and pattern-matching, following ideas from Robin Milner ……. At some point, this implementation was called Le_ML, a name that did not survive. It was used by Larry Paulson to develop Cambridge LCF and by Mike Gordon for the first version of HOL ……. ……
    Our main reason for developing Caml was to use it for sofware development inside Formel. Indeed, it was used for developing the Coq system ……. We were reluctant to adopt a standard that could later prevent us from adapting the language to our programming needs. ……We did incorporate into Caml most of the improvements brought by Standard ML over Edinburgh ML. ……The first implementation of Caml appeared in 1987 and was further developed until 1992. It was created mainly by Ascander Suarez. ……
    In 1990 and 1991, Xavier Leroy designed a completely new implementation of Caml, based on a bytecode interpreter written in C. Damien Doligez provided an excellent memory management system. ……In 1995, Xavier Leroy released Caml Special Light, which improved over Caml Light in several ways. In 1995, Xavier Leroy released Caml Special Light, which improved over Caml Light in several ways. First, an optimizing native-code compiler was added to the bytecode compiler. ……Second, Caml Special Light offered a high-level module system, designed by Xavier Leroy and inspired by the module system of Standard ML. ……Didier Rémy, later joined by Jérôme Vouillon, designed an elegant and highly expressive type system for objects and classes. This design was integrated and implemented within Caml Special Light, leading to the Objective Caml language and implementation, first released in 1996 and renamed to OCaml in 2011.
     
  18. ^ Lawrence C. Paulson. . 1989 [2021-10-10]. (原始内容存档于2021-10-10). 
    Michael J. C. Gordon英语Michael J. C. Gordon. . 1996 [2021-02-27]. (原始内容存档于2016-09-05). In 1981, I moved to a permanent position as Lecturer at the University of Cambridge Computer Laboratory. ……Larry Paulson, recently graduated with a PhD from Stanford, was hired at Cambridge ……. About this time, and in parallel, G ́erard Huet ported the Edinburgh LCF code to Lelisp and MacLisp. Paulson and Huet then established a collaboration and did a lot of joint development of LCF by sending each other magnetic tapes in the post. …… Edinburgh LCF ran interpretively, but during Paulson and Huet’s collaboration an ML compiler was implemented that provided a speedup by a factor of about twenty. …… The resulting new LCF system was named “Cambridge LCF” and completed around 1985. Paulson did little work on it after that. Mikael Hedlund (of the Rutherford Appleton Laboratory) then ported Cambridge LCF to Standard ML (using a new implementation of ML that he created). The resulting Standard ML based version of Cambridge LCF is documented …… in Paulson’s 1987 book Logic and Computation. 
  19. ^ HOL88, source code. 
    Michael J. C. Gordon英语Michael J. C. Gordon. . 1996 [2021-02-27]. (原始内容存档于2016-09-05). Whilst Paulson was designing and implementing Cambridge LCF, I was mainly concerned with hardware verification. …… The first version of the HOL system was created by modifying the Cambridge LCF parser and pretty-printer to support higher order logic concrete syntax. …… The core HOL system became stable in about 1988. A new release that consolidated various changes and enhancements called HOL88 was issued then. We were fortunate to receive support from DSTO Australia to document HOL and from Hewlett Packard to port it from Franz Lisp to Common Lisp (a job very ably done by John Carroll). …… In the late 1980’s Graham Birtwistle of the University of Calgary started a project to reimplement HOL in Standard ML. The work was done by Konrad Slind, under Birtwistle’s direction and with the collaboration of the HOL group at Cambridge. The resulting system, called HOL90, was first released around 1990. …… Recently John Harrison and Konrad Slind have entirely reworked the design of HOL ……. …… This new version of HOL is called “HOL Light”. It is implemented in Caml Light and runs on modest platforms (e.g. standard PCs). It is faster than the Lisp-based HOL88, but a bit slower than HOL90 running in modern implementations of Standard ML. 
  20. ^ Robin Milner. (PDF). 1983 [2021-09-02]. (原始内容 (PDF)存档于2021-11-06). 
  21. ^ R. M. Burstall, J. A. Goguen. . 1977 [2021-09-03]. (原始内容存档于2021-09-03). 
    Donald Sannella. . 1982 [2021-09-06]. (原始内容存档于2021-09-06). 
  22. ^ Rod Burstall英语Rod Burstall, D.B. MacQueen, D.T. Sannella英语Don Sannella. (PDF). 1980 [2021-09-03]. (原始内容 (PDF)存档于2022-01-28).  Conference Record of the 1980 LISP Conference, Stanford University, pp. 136-143.
  23. ^ R.M. Burstall. (PDF). 1968 [2021-09-13]. (原始内容 (PDF)存档于2022-01-28). 
  24. ^ R.M. Burstall, J. Darlington. A transformati

ml语言, meta, language, 元语言, 是一个函数式, 指令式的通用的编程语言, 它著称于使用了多态的hindley, milner类型推论, ml能自动的指定多数表达式, 英语, expression, computer, science, 的类型, 不要求显式的类型标注, 而且能够确保类型安全, 已经正式证明了有良好类型的ml程序不会导致运行时间类型错误, ml编程范型多范型, 函数式, 指令式設計者罗宾, 米尔纳及爱丁堡大学其他人发行时间1973年, 49年前, 1973, 穩定版本standa. ML Meta Language 元语言 是一个函数式 指令式的通用的编程语言 它著称于使用了多态的Hindley Milner类型推论 8 ML能自动的指定多数表达式 英语 Expression computer science 的类型 不要求显式的类型标注 而且能够确保类型安全 已经正式证明了有良好类型的ML程序不会导致运行时间类型错误 8 ML编程范型多范型 函数式 指令式設計者罗宾 米尔纳及爱丁堡大学其他人发行时间1973年 49年前 1973 穩定版本Standard ML 97 1997年 25年前 1997 型態系統类型推论 静态类型 强类型衍生副語言Standard ML OCaml啟發語言ISWIM 1 PAL 2 POP 2 1 GEDANKEN 1 影響語言Clojure Coq Cyclone 英语 Cyclone programming language C Elm 3 Futhark 4 F F Haskell Idris Lazy ML 5 Miranda Nemerle 6 OCaml Opa 英语 Opa programming language Rust Scala Standard ML Ur 7 維基教科書中有關Standard ML Programming的文本ML提供了对函数实际参数的模式匹配 垃圾回收 指令式编程 传值调用和柯里化 它被大量的用于编程语言研究之中 并且是全面规定了的和使用形式语义验证了的少数语言之一 它的类型和模式匹配使得它非常适合并且经常用于在其他形式语言上进行操作 比如在编译器构造 自动化定理证明和形式验证中 目录 1 历史 2 解释与编译 3 核心语言 3 1 函数 3 2 类型 3 3 等式类型 3 4 类型声明 3 5 数据类型 3 6 列表 3 7 模式匹配 3 8 高阶函数 3 9 异常 3 10 引用 4 模块语言 4 1 模块 4 2 函子 5 示例代码 5 1 素数 5 2 汉明数 5 3 续体传递风格实例 5 4 排序算法 5 4 1 插入排序 5 4 2 希尔排序 5 4 3 快速排序 5 4 4 归并排序 5 4 5 堆排序 5 4 6 基数排序 5 5 随机数生成 5 6 语言解释器 6 注释和附录代码 7 参见 8 延伸阅读 9 引用 10 外部链接历史 编辑在1970年代早期 ML由爱丁堡大学的罗宾 米尔纳及他人研制出来 1 用于在LCF 英语 Logic for Computable Functions 定理证明器中开发证明策略 9 LCF的语言是 PPl 它是一阶逻辑演算与有类型的多态l演算的结合 以ML作为元语言 ML的语法从ISWIM及其扩展实现PAL得到了启发 2 LCF 英语 Logic for Computable Functions ML运行在DEC 10 TOPS 10主机的Stanford LISP 1 6下 10 在1980年 Luca Cardelli 英语 Luca Cardelli 于爱丁堡大学的VAX VMS系统上开发了ML编译器 它被称为 VAX ML 11 以区别于LCF版本的 DEC 10 ML 12 VAX ML的编译器和运行时间系统二者 都是用Pascal书写而建立在 函数抽象机器 FAM 之上 13 在1982年 爱丁堡大学的Kevin Mitchell 用VAX ML重写了VAX ML编译器 随即John Scott和Alan Mycroft 英语 Alan Mycroft 加入了开发 在又进行一系列重写改进之后 新的编译器被称为 Edinburgh ML 14 在1981年 INRIA的Gerard Huet 英语 Gerard Huet 将最初的LCF ML适配到Multics系统的Maclisp下 并且增加了编译器 15 这个实现被描述于INRIA内部文档 ML手册 之中 16 它被开发者自称为 Le ML 17 剑桥大学的Lawrence Paulson 英语 Lawrence Paulson 用它开发了基于Franz Lisp的Cambridge LCF 18 进而剑桥大学的Michael J C Gordon 英语 Michael J C Gordon 又用它开发了基于Common Lisp的第一版的HOL 英语 HOL proof assistant 19 在1983年 Robin Milner由两个动机驱使开始重新设计ML 20 其一是爱丁堡大学的Rod Burstall 英语 Rod Burstall 及其小组在规定上的工作 具体化为规定语言CLEAR 21 和表达可执行规定的函数式语言HOPE 22 这项工作与ML有关的是两方面成果 首先 HOPE拥有优雅的编程特征 特别是模式匹配 23 和子句式函数定义 24 其次 是使用在接口中的签名 进行规定的模块化构造的想法 其二是Luca Cardelli 英语 Luca Cardelli 在VAX ML上的工作 通过增加命名记录和可变类型 扩展了ML中数据类型的品目 25 在1984年 贝尔实验室的David MacQueen提出了对Standard ML的模块系统的设计 26 在Standard ML的持续设计期间 27 Edinburgh ML被渐进的修改 充当了Standard ML的近似原型实现 28 在1986年 普林斯顿大学的Andrew Appel 英语 Andrew Appel 和贝尔实验室的David MacQueen 以Edinburgh Standard ML作为起步开发环境 29 开始了专注于生成高质量机器代码的Standard ML of New Jersey的活跃开发 30 在1990年 Robin Milner Mads Tofte 英语 Mads Tofte 和Robert Harper 英语 Robert Harper computer scientist 制定的Standard ML的正式规定 The Definition of Standard ML 最终完成 31 在1997年 这个标准规定增补了David MacQueen为作者并进行了修订 32 在1989年 Mads Tofte 英语 Mads Tofte Nick Rothwell和David N Turner于爱丁堡大学开始开发ML Kit编译器 为了强调清晰性而非高效 将标准定义直接转译成一组Standard ML模块 在1992年和1993年期间 主要通过爱丁堡大学的Nick Rothwell和哥本哈根大学计算机科学系 英语 UCPH Department of Computer Science DIKU 的Lars Birkedal的工作 33 ML Kit第一版完成并开源发行 34 在1987年 INRIA的Ascander Suarez 基于巴黎第七大学的Guy Cousineau 法语 Guy Cousineau 的 范畴抽象机器 英语 Categorical abstract machine CAM 35 利用Le Lisp的运行时间系统重新实现了Le ML 并正式命名为Caml 15 在1990年和1991年 INRIA的Xavier Leroy 英语 Xavier Leroy 基于用C实现的字节码解释器 36 利用Damien Doligez 英语 Damien Doligez 提供的内存管理系统重新实现了Caml 并称其为Caml Light 37 在1995年 Xavier Leroy又增加了机器代码编译器和高层模块系统 38 这个版本也称为 Caml Special Light 在1996年 INRIA的Didier Remy和Jerome Vouillon 向Caml Special Light增加了面向对象特征 39 从而形成了OCaml 40 今天ML家族的两个主要的方言是Standard ML和OCaml ML的实力大多被用于语言设计和操作 比如建构编译器 分析器 定理证明器 但是它作为通用语言也被用于生物信息和财务系统等领域 ML确立了静态类型函数式编程范型 从而在编程语言历史上占有显要地位 它的思想在影响了众多的语言 例如Haskell Nemerle 6 ATS 英语 ATS programming language 和Elm 3 解释与编译 编辑ML代码片段很容易通过将其录入到 顶层 来研习 它也叫作读取 求值 输出循环或REPL 这是打印结果或定义的表达式的推论类型的交互式会话 很多SML实现提供交互式REPL 比如SML NJ sml Standard ML of New Jersey v110 79 built Sat Oct 26 12 27 04 2019 可以在提示符 后键入代码 例如计算1 2 3 1 2 3 val it 7 int 顶层推论这个表达式的类型为int并给出结果7 如果输入不完全则打印第二提示符 这时经常可以用 终结输入 it是给未指定变量的表达式的标准变量 输入control C可返回解释器顶层 输入control D可退出解释器 下面是hello world 的程序代码在SML NJ解释器下执行的结果 val print Hello world n Hello world 和使用MLton编译器进行编译执行的例子 echo print Hello world n gt hello world sml mlton hello world sml hello world Hello world 核心语言 编辑不同于纯函数式编程语言 ML是兼具一些指令式特征的函数式编程语言 ML的特征包括 传值调用的求值策略 头等函数 带有垃圾收集的自动内存管理 参数多态 静态类型 类型推论 代数数据类型 模式匹配和异常处理 不同于Haskell ML与大多数编程语言一样使用及早求值 用ML书写的程序构成自要被求值的表达式 英语 Expression computer science 而非语句或命令 尽管一些表达式返回一个平凡的unit值并且只为其副作用而求值 以下章节介绍采用Standard ML的语法和语义 函数 编辑 就像所有的函数式语言一样 ML的关键特征是函数 它被用于进行抽象 例如阶乘函数用纯ML可表达为 fun fac 0 1 fac n n fac n 1 这里将阶乘描述为递归函数 具有一个单一的终止基础情况 它类似于在数学教科书见到的阶乘描述 多数ML代码在设施和语法上类似于数学 凭借类型推论编译器能推导出 fac接受整数0作为实际参数 则形式参数n也是整数类型int 而fac 0的结果是整数1 则函数fac的结果也是整数类型 函数fac接受一个整数的形式参数并返回一个整数结果 它作为一个整体从而有着 从整数到整数的函数 类型int gt int 函数及其形式参数的 类型 还可以用类型标注 annotation 来描述 使用E t表示法 它可以被读作表达式E有类型t 它是可选也可忽略的 使用类型标注 这个例子可重写为如下 fun fac 0 1 fac n int int n fac n 1 这个函数还依赖于模式匹配 这是ML语言的重要部份 注意函数形式参数不必须在圆括号内但要用空格分隔 当一个函数的实际参数是0 它将返回整数1 对于所有其他情况 尝试第二行 这是一个递归 并且再次执行这个函数直到达到基础情况 它可以使用case表达式重写为 fun fac n case n of 0 gt 1 n gt n fac n 1 这里case介入了模式和对应表达式的序列 它还可以重写为将标识符绑定到lambda函数 val rec fac fn 0 gt 1 n gt n fac n 1 这里的关键字val介入了标识符到值的绑定 fn介入了匿名函数的定义 它可以用在fun的位置上 但使用 gt 算符而非 绑定到递归的匿名函数需要使用rec关键字来指示 通过将主要工作写入尾递归风格的内部迭代函数 借助于语言编译或解释系统进行的尾调用优化 这个函数可以得以增进性能 它的调用栈不需要随函数调用数目而成比例的增长 对这个函数可以采用向内部函数增加额外的 累加器 形式参数acc来实现 fun fact n let fun fac 0 acc acc fac n acc fac n 1 n acc in fac n 1 end let表达式的值是在in和end之间表达式的值 这个递归函数的实现不保证能够终止 因为负数实际参数会导致递归调用的无穷降链条件 更健壮的实现会在递归前检查实际参数为非负数 并在有问题的情况 即n是负数的时候 启用异常处理 fun fact n let fun fac 0 acc acc fac n acc fac n 1 n acc in if n lt 0 then raise Fail negative argument else fac n 1 end 类型 编辑 有一些基本类型可以当作是 内建 的 因为它们是在Standard ML标准基本库中预先定义的 并且语言为它们提供文字 英语 Literal computer programming 表示法 比如34是整数 而 34 是字符串 一些最常用的基本类型是 int 整数 比如3或 12 注意波浪号 表示负号 real浮点数 比如4 2或 6 4 Standard ML不隐含的提升整数为浮点数 因此表达式2 5 67 是无效的 string字符串 比如 this is a string 或 空串 char字符 比如 y 或 n 换行符 bool布尔值 它是要么true要么false 产生bool值的有比较算符 lt gt gt gt lt lt 逻辑函数not和短路求值的中缀算符andalso orelse 包括上述基本类型的各种类型可以用多种方式组合 一种方式是元组 它是值的有序集合 比如表达式 1 2 的类型是int int 而 foo false 的类型是string bool 可以使用 1 foo false 这样的语法来提取元组的指定次序的成员 有0元组 它的类型指示为unit 但是没有1元组 或者说在例子 1 和1之间没有区别 都有类型int 元组可以嵌套 1 2 3 不同于 1 2 3 和 1 2 3 二者 前者的类型是int int int 其他两个的类型分别是 int int int和int int int 组合值的另一种方式是记录 记录很像元组 除了它的成员是有名字的而非有次序的 例如 a 5 0 b five 有类型 a real b string 这同于类型 b string a real 可以使用 a a 5 0 b five 这样的语法来选取记录的指定名字的字段 Standard ML中的函数只接受一个值作为参数 而不是参数的一个列表 可以使用上述元组模式匹配来实际上传递多个参数 函数还可以返回一个元组 例如 fun sum a b a b fun average pair sum pair div 2 infix averaged with fun a averaged with b average a b val c 3 averaged with 7 fun int pair n int n n 这里第一段创建了两个类型是int int gt int的函数sum和average 第二段创建中缀算子averaged with 接着定义它为类型int int gt int的函数 最后的int pair函数的类型是int gt int int 下列函数是多态类型的一个例子 fun pair x x x 编译器无法推论出的pair的特殊化了的类型 它可以是int gt int int real gt real real甚至是 int real gt string gt int real gt string int real gt string 在Standard ML中 它可以简单指定为多态类型 a gt a a 这里的 a 读作 alpha 是一个类型变量 指示任何可能的类型 在上述定义下 pair 3和pair x 都是有良好定义的 分别产生 3 3 和 x x SML标准基本库包括了重载标识符 div mod abs lt gt lt gt 标准基本库提供了多态函数 o before ignore 中缀运算符可以有从缺省最低0到最高9的任何运算符优先级 标准基本库提供了如下内建中缀规定 infix 7 div mod infix 6 infixr 5 infix 4 lt gt gt gt lt lt infix 3 o infix 0 before 等式类型 编辑 算符 和 lt gt 分别被定义为多态的等式和不等式 它确定两个值是否相等 有着类型 a a gt bool 这意味着它的两个运算数必须有相同的类型 这个类型必须是等式类型 eqtype 上述基本类型中除了real之外 int real string char和bool都是等式类型 例如 3 3 3 3 3 3 和true true 都是有效的表达式并求值为true 而3 4是有效表达式并求值为false 3 0 3 0是无效表达式而被编译器拒绝 这是因为IEEE浮点数等式打破了ML中对等式的一些要求 特别是nan不等于自身 所以关系不是自反的 元组和记录类型是等式类型 当时且仅当它的每个成员类型是等式类型 例如int string b bool c char 和unit是等式类型 而int real和 x real 不是 函数类型永远不是等式类型 因为一般情况下不可能确定两个函数是否等价 类型声明 编辑 类型声明或同义词 synonym 使用type关键字来定义 下面是给在平面中的点的类型声明 计算两点间距离 和通过海伦公式计算给定角点的三角形的面积的函数 type loc real real fun heron a loc b loc c loc let fun dist x0 y0 x1 y1 let val dx x1 x0 val dy y1 y0 in Math sqrt dx dx dy dy end val ab dist a b val bc dist b c val ac dist a c val s ab bc ac 2 0 in Math sqrt s s ab s bc s ac end 数据类型 编辑 Standard ML提供了对代数数据类型 ADT 的强力支持 一个ML数据类型可以被当作是元组的不交并 积 英语 Product type 之和 数据类型使用datatype关键字来定义 比如 datatype int or string INT of int STRING of string NEITHER 这个数据类型声明建立一个全新的数据类型int or string 还有一起的新构造子 一种特殊函数或值 INT STRING和NEITHER 每个这种类型的值都是要么INT具有一个整数 要么STRING具有一个字符串 要么NEITHER 写为如下这样 val i INT 3 val s STRING qq val n NEITHER val INT j i 这里最后的一个声明通过模式匹配 将变量j绑定到变量i所绑定的整数3 val 模式 表达式是绑定的一般形式 它是良好定义的 当且仅当模式和表达式有相同的类型 数据类型可以是多态的 datatype a pair PAIR of a a 这个数据类型声明建立一个新的类型 a pair家族 比如int pair string pair等等 数据类型可以是递归的 datatype int list EMPTY INT LIST of int int list 这个数据类型声明建立一个新类型int list 这个类型的每个值是要么EMPTY 空列表 要么是一个整数和另一个int list的接合 通过datatype创建的类型是等式类型 如果它的所有变体 要么是没有参数的空构造子 要么是有等式类型参数的构造子 并且在多态类型情况下所有类型参数也都是等式类型 递归类型在有可能情况下是等式类型 否则就不是 列表 编辑 基础库提供的复杂数据类型之一是列表list 它是一个递归的 多态的数据类型 可以等价的定义为 datatype a list nil of a a list 这里的 是中缀算符 例如3 4 5 nil是三个整数的列表 列表是ML程序中最常用的数据类型之一 语言还为生成列表提供了特殊表示法 3 4 5 real list当然不是等式类型 但是没有int list不能是等式类型的理由 所以它就是等式类型 注意类型变量不同就是不同的列表类型 比如 nil int list nil char list 是无效的 因为两个表达式有不同的类型 即使它们有相同的值 但是nil nil和 nil int list nil都是有效的 基本库rev函数 反转 一个列表中的元素 它的类型是 a list gt a list 就是说它可以接受其元素有任何类型的列表 并返回相同类型的列表 更准确的说 它返回其元素相较于给定列表是反转次序的一个新列表 比如将 a b c 映射成 c b a 中缀算符 表示两个列表的串接 rev和 一般被实现为基本库函数revAppend的简单应用 fun revAppend l l revAppend x r l revAppend r x l fun rev l revAppend l fun l1 l2 revAppend rev l1 l2 模式匹配 编辑 Standard ML的数据类型可以轻易的定义和用于编程 在很大程度上是由它的模式匹配 还有多数Standard ML实现的模式穷尽性检查和模式冗余检查 模式匹配可以在语法上嵌入到变量绑定之中 比如 val m int n int r real s real 2 3 2 0 3 0 type hyperlink protocol string address string title string val url hyperlink title The Standard ML Basis Library protocol https address smlfamily github io Basis overview html val protocol port address addr title name url val x as fst snd 2 true 第一个val绑定了四个变量m n r和s 第二个val绑定了一个变量url 第三个val绑定了三个变量port addr和name 第四个叫分层模式 绑定了三个变量x fst和snd 模式匹配可以在语法上嵌入到函数定义中 比如 datatype shape Circle of loc real 中心和弧度 Square of loc real 左上角和边长 坐标轴对齐 Triangle of loc loc loc 角点 fun area Circle r 3 14 r r area Square s s s area Triangle a b c heron a b c 次序在模式匹配中是紧要的 模式按文本次序来依次进行匹配 在特定计算中 使用下划线 来省略不需要它的值的子成员 这也叫做通配符 wildcard 模式 所谓的 子句形式 风格的函数定义 这里的模式紧随在函数名字之后出现 只是如下形式的一种语法糖 fun area shape case shape of Circle r gt 3 14 r r Square s gt s s Triangle a b c gt heron a b c 模式穷尽性检查将确保数据类型的每个情况都已经顾及到 a 如果有遗漏 则产生警告 b 如果模式存在冗余 也会导致一个编译时间警告 c 高阶函数 编辑 函数可以接受函数作为实际参数 比如 fun applyToBoth f x y f x f y 函数可以产生函数作为返回值 比如 fun constantFn k fn anything gt k 函数可以同时接受和产生函数 比如复合函数 英语 Function composition computer science fun compose f g fn x gt f g x 基本库的函数List map 是在Standard ML中最常用的Curry化高阶函数 它在概念上可定义为 fun map map f x xs f x map f xs 在基本库中将函数复合定义为多态中缀算符 f o g a href Map E9 AB 98 E9 98 B6 E5 87 BD E6 95 B0 html title Map 高阶函数 map a 和 a href Fold E9 AB 98 E9 98 B6 E5 87 BD E6 95 B0 html title Fold 高阶函数 fold a 高阶函数有较高效率的实现 d 异常 编辑 异常可以使用raise关键字发起 并通过模式匹配handle构造来处理 exception Undefined fun max x x max x xs let val m max xs in if x gt m then x else m end max raise Undefined fun main xs let val msg Int toString max xs handle Undefined gt empty list there is no max in print msg n end 这里的 是字符串串接算符 可以利用异常系统来实现非局部退出 例如这个函数所采用技术 exception Zero fun listProd ns let fun p 1 p 0 raise Zero p h t h p t in p ns handle Zero gt 0 end 异常Zero在0情况下发起 控制从函数p中一起出离 引用 编辑 初始化基础库还以引用的形式提供了可变的存储 引用ref可以在某种意义上被认为是如下这样定义的 datatype a ref ref of a 还定义了内建的 函数来修改引用的内容 和 函数来检索引用的内容 阶乘函数可以使用引用定义为指令式风格 fun factImperative n let val i ref n and acc ref 1 in while i gt 0 do acc acc i i i 1 acc end 这里使用圆括号对以 分隔的表达式进行了顺序复合 可变类型 a ref是等式类型 即使它的成员类型不是 两个引用被称为是相等的 如果它们标识相同的 ref单元 就是说相同的对ref构造子调用生成的同一个指针 因此 ref 1 ref 1 和 ref 1 0 ref 1 0 都是有效的 并且都求值为false 因为即使两个引用碰巧指向了相同的值 引用自身是分立的 每个都可以独立于其他而改变 模块语言 编辑模块是ML用于构造大型项目和库的系统 模块 编辑 一个模块构成自一个签名 signature 文件和一个或多个结构文件 签名文件指定要实现的API 就像C语言头文件或Java接口文件 结构实现这个签名 就像C语言源文件或Java类文件 解释器通过use命令导入它们 ML的标准库被实现为这种方式的模块 例如 下列定义一个算术签名 signature ARITH sig eqtype t val zero t val one t val fromInt int gt t val fromIntPair int int gt t val fromReal real gt t val succ t gt t val pred t gt t val t gt t val t t gt t val t t gt t val t t gt t val t t gt t val t t gt bool val lt gt t t gt bool val gt t t gt bool val gt t t gt bool val lt t t gt bool val lt t t gt bool end 和这个签名使用有理数的实现 structure Rational ARITH struct datatype t Rat of int int val zero Rat 0 1 val one Rat 1 1 fun fromInt n Rat n 1 fun ineg a b a b fun fromIntPair num den let fun reduced fraction numerator denominator let fun gcd n 0 n gcd n d gcd d n mod d val d gcd numerator denominator in if d gt 1 then numerator div d denominator div d else numerator denominator end in if num lt 0 andalso den lt 0 then Rat reduced fraction num den else if num lt 0 then Rat ineg reduced fraction num den else if den lt 0 then Rat ineg reduced fraction num den else Rat reduced fraction num den end val SOME maxInt Int maxInt val minPos 1 0 real maxInt fun fromReal r let fun convergent i f h 1 k 1 h 2 k 2 if i lt gt 0 andalso h 1 gt maxInt h 2 div i orelse k 1 gt maxInt k 2 div i then h 1 k 1 else if f lt minPos then i h 1 h 2 i k 1 k 2 else convergent trunc 1 0 f Real realMod 1 0 f i h 1 h 2 i k 1 k 2 h 1 k 1 in if r lt 0 0 then Rat ineg convergent trunc r Real realMod r 1 0 0 1 else Rat convergent trunc r Real realMod r 1 0 0 1 end fun succ Rat a b fromIntPair a b b fun pred Rat a b fromIntPair a b b fun add Rat a b Rat c d if b d then fromIntPair a c b else fromIntPair a d c b b d fun sub Rat a b Rat c d if b d then fromIntPair a c b else fromIntPair a d c b b d fun mul Rat a b Rat c d fromIntPair a c b d fun div Rat a b Rat c d fromIntPair a d b c fun gt Rat a b Rat c d if b d then a gt c else a d gt b c fun lt Rat a b Rat c d if b d then a lt c else a d lt b c fun neg Rat a b Rat a b fun eq Rat a b Rat c d b d andalso a c fun a neg a fun a b add a b fun a b sub a b fun a b mul a b fun a b div a b fun op a b eq a b fun a lt gt b not eq a b fun a gt b gt a b fun a gt b gt a b orelse eq a b fun a lt b lt a b fun a lt b lt a b orelse eq a b end 下面是这个结构的简单用例 infix local open Rational in val c let val a fromIntPair 2 3 val b fromIntPair 4 6 in a b end end structure R Rational R fromReal 3 245 Standard ML只允许通过签名函数同实现进行交互 例如不可以直接通过这个代码中的Rat来建立数据对象 结构块对外部隐藏所有实现细节 这里的 叫做透明归属 ascription 可以通过所绑定的变量见到此结构的数据内容 与之相对的是 gt 它叫做不透明归属 此结构的数据内容对外完全不可见 比如上面用例有结果 val c Rat 4 3 Rational t 如果改为不透明归属则有结果 val c Rational t 要用有理数进行实际上的数值计算 需要处理分数形式中分母快速增大导致溢出整数类型大小范围等问题 e 函子 编辑 主条目 函子 函数式编程 函子接受指定签名的一个结构作为参数 并返回一个结构作为结果 下面示例的函子能在ARITH签名的结构上计算移动平均 signature MOVINGLIST sig type t structure Arith sig type t end val size t gt int val average t gt Arith t val fromList Arith t list gt t val move t Arith t gt t val expand t Arith t gt t val shrink t gt t val trunc t gt t end functor MovingList S ARITH MOVINGLIST struct type t S t list int S t structure Arith S fun size ml t 2 ml fun average ml t 3 ml fun fromList l S t list let val n length l val sum foldl S S zero l local open S in val m sum fromInt n end in if null l then raise Empty else l n m end fun move l n m t new S t let val old List nth l n 1 local open S in val m m new old fromInt n end in new l n m end fun expand l n m t new S t let val n n 1 local open S in val m m new m fromInt n end in new l n m end fun shrink l n m t let val old List nth l n 1 val n if n gt 2 then n 1 else 1 local open S in val m m m old fromInt n end in l n m end fun trunc l n m t List take l n n m end 和这个函子的简单用例 structure R Rational structure MLR MovingList Rational val d MLR fromList R fromIntPair 4 5 R fromIntPair 2 3 val d MLR expand d R fromIntPair 5 6 val d MLR move d R fromIntPair 7 8 val d MLR shrink d val d MLR trunc d 这个用例承上节示例 Rational结构采用了透明归属 有结果如 val d Rat 4 5 Rat 2 3 2 Rat 11 15 MLR t 如果它改为不透明归属 则对应结果为 val d 2 MLR t 示例代码 编辑下列例子使用了Standard ML的语法和语义 素数 编辑 下面是求素数的试除法实现 fun prime n let fun isPrime l i let fun existsDivisor false existsDivisor x xs if i mod x 0 then true else if x x gt i then false else existsDivisor xs in not existsDivisor l end fun iterate acc i if i gt n then acc else if isPrime acc i then iterate acc i i 2 else iterate acc i 2 in if n lt 2 then else iterate 2 3 end 基本库find和exists函数在不存在符合条件元素的时候会遍历整个列表 f 这里采用了特殊化了的existsDivisor 用以在后续元素都不满足条件时立即结束运算 下面是埃拉托斯特尼筛法实现 fun prime n let fun dropComposite acc rev acc dropComposite acc l as x xs j i if j gt n then List revAppend acc l else if x lt j then dropComposite x acc xs j i else if x gt j then dropComposite acc l j i i else dropComposite acc xs j i i fun init i let fun loop l i if i lt 2 then l else loop i l i 2 in loop i i 1 mod 2 end fun iterate acc rev acc iterate acc l as x xs if x x gt n then 2 List revAppend acc l else iterate x acc dropComposite xs x x x 2 in if n lt 2 then else iterate init n end 这里基于列表的筛法实现符合埃拉托斯特尼的原初算法 41 筛法还有基于数组的直观实现 g 下面是其解释器下命令行运行实例 fun printIntList l int list print String concatWith map Int toString l n val printIntList fn int list gt unit val printIntList prime 100 2 3 5 7 11 13 17 19 23 29 31 37 41 43 47 53 59 61 67 71 73 79 83 89 97 汉明数 编辑 正规数是形如 2 i 3 j 5 k displaystyle 2 i cdot 3 j cdot 5 k 的整数 对于非负整数 i displaystyle i j displaystyle j 和 k displaystyle k 它是可以整除 60 max i 2 j k displaystyle 60 max lceil i 2 rceil j k 的数 计算升序的正规数的算法经由戴克斯特拉得以流行 42 理查德 汉明最初提出了这个问题 故而这个问题被称为 汉明问题 这个数列也因而被称为汉明数 Dijkstra计算这些数的想法如下 汉明数的序列开始于数1 要加入序列中的数有下述形式 2h 3h 5h 这里的h是序列已有的任意的汉明数 因此 可以生成最初只有一个1的序列H 并接着归并 英语 Merge algorithm 序列2H 3H 5H 并以此类推 示例汉明数程序代码 一般用来展示 确使计算只在需要时进行的纯函数式编程方式 43 fun Hamming number n let fun merge p q let fun revMerge acc p q if not null p andalso not null q then if hd p lt hd q then revMerge hd p acc tl p q else if hd p gt hd q then revMerge hd q acc p tl q else revMerge hd p acc tl p tl q else if null p then List revAppend q acc else List revAppend p acc in if null p then q else if null q then p else rev revMerge p q end fun mul m x if x lt n div m then SOME x m else NONE fun mapPrefix pred l let fun mapp acc rev acc mapp x xs acc case pred x of SOME a gt mapp xs a acc NONE gt rev acc in mapp l end fun mergeWith f m i merge f m i fun generate l let fun listMul m mapPrefix mul m l in foldl mergeWith listMul 2 3 5 end fun iterate acc l if hd l gt n div 2 then merge l acc else iterate merge l acc generate l in if n gt 0 then iterate 1 else end 产生指定范围内的汉明数需要多轮运算 后面每轮中的三个列表元素乘积运算中都可能产生超出这个范围的结果 它们不需要出现在后续的运算之中 h 基本库mapPartial函数与它所映射的函数 通过基于Option结构的SOME和NONE构造子的协定 可以将所映射函数认为不符合条件的元素或者结果排除掉 它会遍历整个列表 i 由于这个算法采用升序列表 故而这里将它改写为mapPrefix函数 用来在特定条件不满足条件就立即结束 下面是汉明数程序在解释器下命令行运行实例 fun printIntList l int list print String concatWith map Int toString l n val printIntList fn int list gt unit val printIntList Hamming number 400 1 2 3 4 5 6 8 9 10 12 15 16 18 20 24 25 27 30 32 36 40 45 48 50 54 60 64 72 75 80 81 90 96 100 108 120 125 128 135 144 150 160 162 180 192 200 216 225 240 243 250 256 270 288 300 320 324 360 375 384 400 续体传递风格实例 编辑 下面是续体传递风格 英语 Continuation passing style CPS 44 的高阶函数foldr和map的实现 和达成一个整数列表的合计函数的简单用例 fun foldr f b l let fun f2 k k b f2 k a r f2 fn x gt k f a x r in f2 fn x gt x l end fun map f l foldr fn x y gt f x y l fun sum l foldr fn x y gt x y 0 l 对于输入 e sub 1 sub e sub 2 sub e sub n sub sum函数等价于函数复合 fn x gt x o fn x gt e sub 1 sub x o fn x gt e sub 2 sub x o o fn x gt e sub n sub x 它应用于0上得到 e sub 1 sub e sub 2 sub e sub n sub 0 45 SML NJ支持头等对象的续体 46 头等续体对一门语言而言是能完全控制指令执行次序的能力 它们可以用来跳转到产生对当前函数调用的那个函数 或者跳转到此前已经退出了的函数 头等续体保存了程序执行状态 它不保存程序数据 只保存执行上下文 排序算法 编辑 排序算法关注计算复杂度 特别是时间复杂度 基本库函数的实现细节也要考虑在内 比如串接函数 它被实现为fun l1 l2 revAppend rev l1 l2 除非必需的情况避免使用遍历整个列表的rev和length函数 j 通过比较于这些排序算法的周知过程式编程语言比如C语言的实现 可以体察到ML在控制流程和列表数据结构上的相关限制 和与之相适应的采用尾递归的特色函数式编程风格 插入排序 编辑 下面是简单的插入排序算法的尾递归和等价的普通递归实现 尾递归 普通递归fun insertSort l let fun insert pred ins l let fun loop acc List revAppend acc ins loop acc l as x xs if pred ins x then List revAppend acc ins l else loop x acc xs in loop l end val rec ge fn x y gt x gt y in rev foldl insert ge l end fun insertSort l let fun insert pred ins ins insert pred ins l as x xs if pred ins x then ins l else x insert pred ins xs val rec ge fn x y gt x gt y in rev foldl insert ge l endx保存在形式参数acc对应的分配堆中 x保存在调用栈栈帧中插入排序算法是稳定的自适应排序 英语 Adaptive sort 它在输入列表趋于正序的时候性能最佳 在输入列表趋于反序的时候性能最差 因此在算法实现中 需要insert函数所插入列表保持为反序 在插入都完成后经rev函数再反转回正序 在预期输入数据趋于随机化或者预知它经过了反转的情况下 可以采用保持要插入列表为正序的变体插入排序算法实现 它在输入列表趋于反序的时候性能最佳 在输入列表趋于正序的时候性能最差 它比自适应实现少作一次全列表反转 k 采用foldr函数可以相应的保持要插入列表为正序 由于fun foldr f b l foldl f b rev l 它等同于对反转过的列表应用变体插入排序 希尔排序 编辑 希尔排序算法是对插入排序的改进 保持了自适应性 英语 Adaptive sort 放弃了稳定性 l 下面是希尔排序的实现 fun shellSort l let fun insert pred ins l let fun loop acc List revAppend acc ins loop acc l as x xs if pred ins x then List revAppend acc ins l else loop x acc xs in loop l end val rec lt fn x y gt x lt y fun insertSort insertSort x x insertSort x y if y lt x then y x else x y insertSort x y z xs let val x y z if y lt x then if z lt y then z y x else if z lt x then y z x else y x z else if z lt x then z x y else if z lt y then x z y else x y z in foldl insert lt x y z xs end fun group lol n let fun dup n let fun loop acc i if i lt 0 then acc else loop acc i 1 in loop n end fun loop accj lol List revAppend accj lol loop acci accj loop rev acci rev accj loop acci accj lol loop rev acci accj lol loop acci lol accj loop acci lol rev accj loop acci ls accj lol loop acci ls accj lol loop acci x xs ls accj l ls loop xs acci ls x l accj ls in loop lol dup n end val lol len foldl fn x l n gt x l n 1 0 rev l val incs 1 4 9 20 46 103 233 525 1182 2660 5985 13467 30301 68178 153401 345152 776591 1747331 3931496 8845866 19903198 44782196 100759940 226709866 510097200 val gap let val v len 3 div 4 val thold if v 0 then 1 else v fun loop acc h if hd h gt thold then acc else loop hd h acc tl h in loop incs end fun sort h lol map insertSort group lol h in hd foldl sort lol gap end 这里采用的间隔序列是OEIS A108870 即 1 5 9 9 4 k 1 4 displaystyle begin smallmatrix left lceil frac 1 5 left 9 cdot left frac 9 4 right k 1 4 right right rceil end smallmatrix 它是徳田尚之在1992年提出的 47 这个序列用递推公式表示为 h sub k sub h sub k sub 这里的h sub k sub 2 25 h sub k 1 sub 1而h sub 1 sub 1 假定一个列表的长度s位于序列两个元素之间 即h sub k 1 sub lt h sub k sub s lt h sub k 1 sub 如果h sub k sub span class mwe math element span class mwe math mathml inline mwe math mathml a11y style display none math xmlns http www w3 org 1998 Math MathML alttext displaystyle tfrac n m semantics mrow class MJX TeXAtom ORD mstyle displaystyle true scriptlevel 0 mrow class MJX TeXAtom ORD mstyle displaystyle false scriptlevel 0 mfrac mi n mi mi m mi mfrac mstyle mrow mstyle mrow annotation encoding application x tex displaystyle tfrac n m annotation semantics math span noscript noscript span class lazy image placeholder style width 2 279ex height 3 009ex vertical align 1 005ex data src https wikimedia org api rest v1 media math render svg bd4d59ffec7a1176fd50f43970de08240094378a data alt displaystyle tfrac n m data class mwe math fallback image inline span span s 这里的n m 则选择初始间隔为h sub k sub 否则为h sub k 1 sub 在这个阈值下 对于不同长度s的列表和对应的初始间隔h 每个列表的这些初始子列表的平均长度 span class mwe math element span class mwe math mathml inline mwe math mathml a11y style display none math xmlns http www w3 org 1998 Math MathML alttext displaystyle tfrac s h semantics mrow class MJX TeXAtom ORD mstyle displaystyle true scriptlevel 0 mrow class MJX TeXAtom ORD mstyle displaystyle false scriptlevel 0 mfrac mi s mi mi h mi mfrac mstyle mrow mstyle mrow annotation encoding application x tex displaystyle tfrac s h annotation semantics math span noscript noscript span class lazy image placeholder style width 1 783ex height 3 343ex vertical align 1 338ex data src https wikimedia org api rest v1 media math render svg 1c8b8b5da9451fbe174bc17e0973c2ece0c6a3a8 data alt displaystyle tfrac s h data class mwe math fallback image inline span span 约在 span class mwe math element span class mwe math mathml inline mwe math mathml a11y style display none math xmlns http www w3 org 1998 Math MathML alttext displaystyle tfrac m n semantics mrow class MJX TeXAtom ORD mstyle displaystyle true scriptlevel 0 mrow class MJX TeXAtom ORD mstyle displaystyle false scriptlevel 0 mfrac mi m mi mi n mi mfrac mstyle mrow mstyle mrow annotation encoding application x tex displaystyle tfrac m n annotation semantics math span noscript noscript span class lazy image placeholder style width 2 279ex height 3 009ex vertical align 1 005ex data src https wikimedia org api rest v1 media math render svg 1413d4c83a94e754258e428fcd72d4fc6bcc2e3e data alt tfrac m n data class mwe math fallback image inline span span span class mwe math element span class mwe math mathml inline mwe math mathml a11y style display none math xmlns http www w3 org 1998 Math MathML alttext displaystyle tfrac s h semantics mrow class MJX TeXAtom ORD mstyle displaystyle true scriptlevel 0 mrow class MJX TeXAtom ORD mstyle displaystyle false scriptlevel 0 mfrac mi s mi mi h mi mfrac mstyle mrow mstyle mrow annotation encoding application x tex displaystyle tfrac s h annotation semantics math span noscript noscript span class lazy image placeholder style width 1 783ex height 3 343ex vertical align 1 338ex data src https wikimedia org api rest v1 media math render svg 1c8b8b5da9451fbe174bc17e0973c2ece0c6a3a8 data alt displaystyle tfrac s h data class mwe math fallback image inline span span lt span class mwe math element span class mwe math mathml inline mwe math mathml a11y style display none math xmlns http www w3 org 1998 Math MathML alttext displaystyle tfrac 9 4 semantics mrow class MJX TeXAtom ORD mstyle displaystyle true scriptlevel 0 mrow class MJX TeXAtom ORD mstyle displaystyle false scriptlevel 0 mfrac mn 9 mn mn 4 mn mfrac mstyle mrow mstyle mrow annotation encoding application x tex displaystyle tfrac 9 4 annotation semantics math span noscript noscript span class lazy image placeholder style width 1 658ex height 3 509ex vertical align 1 171ex data src https wikimedia org api rest v1 media math render svg c6d280f9dcbe1697c0d1f75b91c66e966a89dd5f data alt displaystyle tfrac 9 4 data class mwe math fallback image inline span span span class mwe math element span class mwe math mathml inline mwe math mathml a11y style display none math xmlns http www w3 org 1998 Math MathML alttext displaystyle tfrac m n semantics mrow class MJX TeXAtom ORD mstyle displaystyle true scriptlevel 0 mrow class MJX TeXAtom ORD mstyle displaystyle false scriptlevel 0 mfrac mi m mi mi n mi mfrac mstyle mrow mstyle mrow annotation encoding application x tex displaystyle tfrac m n annotation semantics math span noscript noscript span class lazy image placeholder style width 2 279ex height 3 009ex vertical align 1 005ex data src https wikimedia org api rest v1 media math render svg 1413d4c83a94e754258e428fcd72d4fc6bcc2e3e data alt tfrac m n data class mwe math fallback image inline span span 范围之内 间隔序列还可以采用OEIS A102549 它是Marcin Ciura在2001年通过实验得到的 48 m 快速排序 编辑 下面是快速排序算法的自顶向下实现 fun quickSort quickSort x x quickSort x y if x lt y then x y else y x quickSort x y z let val x y if x lt y then x y else y x val y z if y lt z then y z else z y val x y if x lt y then x y else y x in x y z end quickSort pivot xs let fun partition pred l let fun loop p q p q loop h t p q if pred h then loop t h p q else loop t p h q in loop l end val le gt partition fn x gt x lt pivot xs in quickSort le pivot quickSort gt end 基本库partition函数实现对快速排序而言有不必要的反转 n 这里采用了它的简化改写 在ML中快速排序应采用自底向上实现 fun quickSort l let fun partition pred l let fun loop p q p q loop h t p q if pred h then loop t h p q else loop t p h q in loop l end fun iterate acc acc iterate acc xs iterate acc xs iterate acc x xs iterate x acc xs iterate acc x y xs let val x y if x lt y then x y else y x in iterate x y acc xs end iterate acc x y z xs let val x y if x lt y then x y else y x val x y z if y lt z then x y z else if x lt z then x z y else z x y in iterate x y z acc xs end iterate acc pivot d xs let val le gt partition fn x gt x lt pivot d in iterate acc gt pivot le xs end in iterate l end 归并排序 编辑 下面是归并排序算法的自底向上法实现 fun mergeSort l let fun init acc acc init acc x x acc init acc x y if x lt y then x y acc else y x acc init acc x y z xs let val x y z if x lt y then if y lt z then x y z else if x lt z then x z y else z x y else if x lt z then y x z else if y lt z then y z x else z y x in init x y z acc xs end fun mergeWith acc acc mergeWith acc p List revAppend p acc mergeWith acc q List revAppend q acc mergeWith cmp acc p ps q qs if cmp p q then mergeWith cmp p acc ps q qs else mergeWith cmp q acc p ps qs val mergeRev mergeWith fn x y gt x gt y val revMerge mergeWith fn x y gt x lt y fun iterate iterate x isRev if isRev then rev x else x iterate acc isRev let val merge if isRev then mergeRev else revMerge fun loop acci acci loop acci x rev x acci loop acci x y xs loop merge x y acci xs in iterate loop acc not isRev end in iterate init l false end 考虑输入列表 x sub 1 sub x sub i sub a sub 0 sub a sub 9 sub x sub j sub x sub n sub 这里在x sub i sub 和x sub j sub 之间的10个a 具有相同的值并且需要保持其下标表示的次序 这里的x sub i sub gt a并且x sub j sub lt a 并且在这个区段前后的元素总数都能被3整除 则它被分解成子列表的列表 X sub m sub x sub j sub a sub 8 sub a sub 9 sub a sub 5 sub a sub 6 sub a sub 7 sub a sub 2 sub a sub 3 sub a sub 4 sub a sub 0 sub a sub 1 sub x sub i sub X sub 1 sub 这里有m n div 3 假定这4个含有a的子列表两两归并 在归并正序子列表的归并条件x lt y下 能得到 X sub 1 sub x sub i sub a sub 4 sub a sub 0 sub a sub 9 sub a sub 5 sub x sub j sub X sub k sub 继续推演下去 在归并反序子列表的归并条件x gt y下 能得到 X sub h sub x sub j sub a sub 0 sub a sub 9 sub x sub i sub X sub 1 sub 可以看出这种归并操作能够保证排序算法的稳定性 即具有相同值的元素之间的相对次序保持不变 分解初始的子列表采用了插入排序 还可进一步增加其大小 归并排序也有自顶向下实现 o 堆排序 编辑 下面是堆排序的基于数组的实现 fun heapSort l let val h Array fromList l val len Array length h fun get i Array sub h i fun set i v Array update h i v fun siftdown i ins n let fun sift k let val l k 2 1 val r l 1 in if r lt n andalso get r gt get l then r else if l lt n then l else k end fun loop i let val j sift i in if j i orelse get j lt ins then set i ins else set i get j loop j end in loop i end fun heapify let fun loop i if i lt 0 then else siftdown i get i len loop i 1 in loop len div 2 1 end fun generate let fun loop acc i let val t get 0 in if i lt 0 then t acc else siftdown 0 get i i loop t acc i 1 end in if len 0 then else loop len 1 end in heapify generate end 在数组实现中 siftdown函数融合了插入和筛选功能 它首先在暂时位于堆顶的要插入的元素 和从堆顶节点左右子堆的两个堆顶元素中筛选出的那个元素 二者中选择出哪个适合作堆顶元素 如果要插入元素适合 则以它为新堆顶元素而结束整个过程 否则以筛选出元素为新堆顶元素 并自顶向下逐级处理提供了新堆顶元素的子堆 将要插入元素暂时作为其堆顶元素并对它继续进行siftdown siftdown只要到达了某个堆底 就插入要插入的元素而结束整个过程 在提取堆顶元素生成结果列表时 先提取走堆顶元素的内容 再摘掉最后的堆底元素将它的内容暂时放置在堆顶 这时堆的大小也相应的减一 随后的siftdown函数 筛选出新的堆顶元素 并把原最后堆底元素插入回堆中 在heapify函数建造堆的时候 首先自列表中间将元素分为前后两组 后组中的元素被视为只有一个元素的堆 然后从后往前处理前组中的元素 这时它的左右子节点已经是已有的堆或者为空 在其上进行siftdown 从而合成一个新堆 建造堆也可以采用siftup函数来实现 它自第二个元素开始从前往后逐个处理列表元素 其前面是已有的堆 将这个新元素自堆底向上插入到这个堆中 p 堆排序算法也可以使用二叉树数据结构来实现二叉堆 fun heapSort l let datatype a heap Nil Leaf of a Node of a int a heap a heap fun key Nil let val SOME a Int minInt in a end key Leaf k k key Node k k fun count Nil 0 count Leaf 1 count Node c c fun left Nil Nil left Leaf Nil left Node l l fun insert Nil x Leaf x insert Leaf k l if l gt k then Node l 2 Leaf k Nil else Node k 2 Leaf l Nil insert Node k Leaf l Nil r if r gt k then Node r 3 Leaf k Leaf l else if r gt l then Node k 3 Leaf r Leaf l else Node k 3 Leaf l Leaf r insert Node k c l r x let val k x if k gt x then k x else x k in if count l lt count r then Node k c 1 insert l x r else if x gt key l then Node k c 1 insert r x l else Node k c 1 l insert r x end fun extract Nil Nil extract Leaf Nil extract Node l Nil l extract Node c l r let val k key l val n left l in if n Nil then Node k c 1 r Nil else if key n gt key r then Node k c 1 extract l r else Node k c 1 r extract l end fun heapify let fun loop acc acc loop acc x xs loop insert acc x xs in loop Nil l end fun generate h let fun loop acc Nil acc loop acc h loop key h acc extract h in loop h end in generate heapify end 二叉树实现不能直接访问堆底元素 从而不适宜通过摘掉它使堆的大小减一 这里的insert函数 在原堆顶元素和要插入元素中选择适合者作为新的堆顶元素 将落选的另一个元素作为新的要插入元素 插入到利于保持这个堆平衡的那个子树之中 这里的extract函数只筛选不插入 它将堆的大小减一 这里的insert和extract函数也可以直接转写为等价的尾递归形式 与列表情况不同 只要树结构能保持良好的平衡 采用尾递归形式就没有太大的必要性 q 在二叉树实现下 也可以采用siftdown函数来初始建造堆 而不需要在节点中保存关于树状态的统计信息 r 基数排序 编辑 下面是针对非负整数的基数排序算法的实现 fun radixSort l let fun distribute l d let val t0 fun loop t let fun join acc i let val f case i of 1 gt 1 t 2 gt 2 t 3 gt 3 t 4 gt 4 t 5 gt 5 t 6 gt 6 t 7 gt 7 t 8 gt 8 t gt in if i lt 0 then acc else join List revAppend f acc i 1 end in join 8 end loop t x xs let val f0 f1 f2 f3 f4 f5 f6 f7 t val t case x div d mod 8 of 0 gt x f0 f1 f2 f3 f4 f5 f6 f7 1 gt f0 x f1 f2 f3 f4 f5 f6 f7 2 gt f0 f1 x f2 f3 f4 f5 f6 f7 3 gt f0 f1 f2 x f3 f4 f5 f6 f7 4 gt f0 f1 f2 f3 x f4 f5 f6 f7 5 gt f0 f1 f2 f3 f4 x f5 f6 f7 6 gt f0 f1 f2 f3 f4 f5 x f6 f7 7 gt f0 f1 f2 f3 f4 f5 f6 x f7 gt t0 in loop t xs end in loop t0 l end val SOME maxInt Int maxInt val max foldl fn x y gt if x gt y then x else y 0 l fun iterate l d let val l distribute l d in if d gt maxInt div 8 1 orelse max div d div 8 0 then l else iterate l d 8 end in iterate l 1 end 这里采用的基数是2的3次幂8 代码所使用的列表元组大小与基数大小成正比 运算量与列表中元素的总数与最大数的位数的乘积成正比 随机数生成 编辑 编写排序算法进行测试除了使用简单的数列 s 测试用列表还可以使用线性同余伪随机数函数来生成 49 fun randList n seed let val randx ref seed fun lcg randx randx 421 1663 mod 7875 randx fun lcg randx randx 1366 150889 mod 714025 randx fun iterate acc i if i lt 0 then acc else iterate lcg acc i 1 in iterate n end 语言解释器 编辑 定义和处理一个小型表达式语言是相对容易的 exception Err datatype ty IntTy BoolTy datatype exp True False Int of int Not of exp Add of exp exp If of exp exp exp fun typeOf True BoolTy typeOf False BoolTy typeOf Int IntTy typeOf Not e if typeOf e BoolTy then BoolTy else raise Err typeOf Add e1 e2 if typeOf e1 IntTy andalso typeOf e2 IntTy then IntTy else raise Err typeOf If e1 e2 e3 if typeOf e1 lt gt BoolTy then raise Err else if typeOf e2 lt gt typeOf e3 then raise Err else typeOf e2 fun eval True True eval False False eval Int n Int n eval Not e case eval e of True gt False False gt True gt raise Fail type checking is broken eval Add e1 e2 let val Int n1 eval e1 val Int n2 eval e2 in Int n1 n2 end eval If e1 e2 e3 if eval e1 True then eval e2 else eval e3 fun exp repr e let val msg case e of True gt True False gt False Int n gt Int toString n gt in msg n end 忽略TypeOf的返回值 它在类型错误时发起Err fun evalPrint e ignore typeOf e print exp repr eval e 将这段代码录入文件比如expr lang sml 并在命令行下执行sml expr lang sml 可以用如下在正确类型的和不正确类型上运行的例子 测试这个新语言 val e1 Add Int 1 Int 2 正确的类型 val e1 Add Int 1 Int 2 exp val evalPrint e1 3 val e2 Add Int 1 True 不正确的类型 val e2 Add Int 1 True exp val evalPrint e2 uncaught exception Err raised at expr lang sml 25 20 25 23注释和附录代码 编辑 子句集合是穷尽和不冗余的函数示例 fun hasCorners Circle false hasCorners true 如果控制通过了第一个模式Circle 则这个值必定是要么Square要么Triangle 在任何这些情况下 这个形状都有角点 所以返回true而不用区分具体是那种情况 不详尽的模式示例 fun center Circle c c center Square x y s x s 2 0 y s 2 0 这里在center函数中没有给Triangle的模式 编译器发起模式不详尽的一个警告 并且如果在运行时间 Triangle被传递给这个函数 则发起异常Match 存在模式冗余的 无意义 函数示例 fun f Circle x y r x y f Circle 1 0 f 0 0 匹配第二个子句的模式的任何值都也匹配第一个子句的模式 所以第二个子句是不可到达的 因此这个定义整体上是冗余的 映射函数的实际实现 fun map f let fun m m a f a m a b f a f b m a b c f a f b f c m a b c d r f a f b f c f d m r in m end 折叠函数的实际实现 fun foldl f b l let fun f2 b b f2 a r b f2 r f a b in f2 l b end fun foldr f b l foldl f b rev l 过滤器函数的实际实现 fun filter pred filter pred a rest if pred a then a filter pred rest else filter pred rest 对分数采取修约的有理数实现 signature ARITH sig eqtype t val zero t val one t val fromInt int gt t val fromIntPair int int gt t val repr t gt unit val succ t gt t val pred t gt t val t gt t val t t gt t val t t gt t val t t gt t val t t gt t end structure Rational ARITH struct type t int int val zero 0 1 val one 1 1 val maxInt let val SOME a Int maxInt in Int toLarge a end fun fromInt n n 1 fun neg a b a b fun fromLargePair a b Int fromLarge a Int fromLarge b fun fromIntPair num den let fun reduced fraction numerator denominator let fun gcd n 0 n gcd n d gcd d n mod d val d gcd numerator denominator in if d gt 1 then numerator div d denominator div d else numerator denominator end in if num lt 0 andalso den lt 0 then reduced fraction num den else if num lt 0 then neg reduced fraction num den else if den lt 0 then neg reduced fraction num den else reduced fraction num den end fun repr a b let val m if b 0 then 0 else if a gt 0 then a div b else a div b val n if b 0 then 1 else if a gt 0 then a mod b else a mod b val ms Int toString m and ns Int toString n and bs Int toString b in if n lt gt 0 andalso m lt gt 0 andalso a lt 0 then print ms ns bs n else if n lt gt 0 andalso m lt gt 0 then print ms ns bs n else if n lt gt 0 andalso m 0 andalso a lt 0 then print ns bs n else if n lt gt 0 andalso m 0 then print ns bs n else if a lt 0 then print ms n else print ms n end fun convergent i n d h 1 k 1 h 2 k 2 if i lt gt 0 andalso h 1 gt maxInt h 2 div i orelse k 1 gt maxInt k 2 div i then h 1 k 1 else if n 0 then i h 1 h 2 i k 1 k 2 else convergent d div n d mod n n i h 1 h 2 i k 1 k 2 h 1 k 1 fun add a b c d let val la Int toLarge a and lb Int toLarge b val lc Int toLarge c and ld Int toLarge d val m la ld lb lc and n lb ld in if b d then fromIntPair a c b else fromLargePair convergent m div n m mod n n 1 0 0 1 end fun sub a b c d let val la Int toLarge a and lb Int toLarge b val lc Int toLarge c and ld Int toLarge d val m la ld lb lc and n lb ld in if b d then fromIntPair a c b else if m lt 0 then neg fromLargePair convergent m div n m mod n n 1 0 0 1 else if m gt 0 then fromLargePair convergent m div n m mod n n 1 0 0 1 else 0 1 end fun mul a b c d let val la Int toLarge a and lb Int toLarge b val lc Int toLarge c and ld Int toLarge d val m la lc and n lb ld in fromLargePair convergent m div n m mod n n 1 0 0 1 end fun op a b c d if a lt 0 andalso c lt 0 then neg add a b c d else if a lt 0 then sub c d a b else if c lt 0 then sub a b c d else add a b c d fun op a b c d if a lt 0 andalso c lt 0 then sub c d a b else if a lt 0 then neg add a b c d else if c lt 0 then add a b c d else sub a b c d fun op a b c d if a lt 0 andalso c lt 0 then mul a b c d else if a lt 0 then neg mul a b c d else if c lt 0 then neg mul a b c d else mul a b c d fun op a b c d if a lt 0 andalso c lt 0 then mul a b d c else if a lt 0 then neg mul a b d c else if c lt 0 then neg mul a b d c else mul a b d c fun succ a add a one fun pred a sub a one fun a neg a end 找出函数的实际实现 fun find pred NONE find pred a rest if pred a then SOME a else find pred rest 存在谓词函数的实际实现 fun exists pred let fun f false f h t pred h orelse f t in f end 筛法基于数组的实现 fun prime n let val sieve Array array n 1 true fun markComposite j i if j gt n then else Array update sieve j false markComposite j i i fun iterate i if i i gt n then else if Array sub sieve i then markComposite i i i iterate i 1 else iterate i 1 fun generate acc i if i lt 2 then acc else if Array sub sieve i then generate i acc i 1 else generate acc i 1 in if n lt 2 then else iterate 2 generate n end 汉明数进一步性质演示代码 fun printIntList l int list print String concatWith map Int toString l n fun diff p q let fun revDiff acc p q if not null p andalso not null q then if hd p lt hd q then revDiff hd p acc tl p q else if hd p gt hd q then revDiff acc p tl q else revDiff acc tl p tl q else if null q then List revAppend p acc else acc in if null p then else if null q then p else rev revDiff p q end fun Hamming number n let fun merge p q let fun revMerge acc p q if not null p andalso not null q then if hd p lt hd q then revMerge hd p acc tl p q else if hd p gt hd q then revMerge hd q acc p tl q else revMerge hd p acc tl p tl q else if null p then List revAppend q acc else List revAppend p acc in if null p then q else if null q then p else rev revMerge p q end fun mergeWith f m i merge f m i fun mul m x x m fun generate l let fun listMul m map mul m l in printIntList listMul 2 printIntList diff listMul 3 listMul 2 printIntList diff listMul 5 merge listMul 2 listMul 3 foldl mergeWith listMul 2 3 5 end val count ref 1 fun iterate acc l if hd l gt n div 2 then merge l acc else print round Int toString count for Int toString length l number s n count count 1 iterate merge l acc generate l in if n gt 0 then iterate 1 else end val l Hamming number 400 val h List filter fn x gt x lt 400 l val print Int toString length h numbers from Int toString length l numbers n 部份映射函数的实际实现 fun mapPartial pred l let fun mapp l rev l mapp x r l case pred x of SOME y gt mapp r y l NONE gt mapp r l end case in mapp l end 列表长度函数的实际实现 fun length l let fast add that avoids the overflow test val op Int fast add fun loop n n loop n n 1 loop n l loop n 2 l in loop 0 l end 变体的插入排序算法实现 fun insertSort l let fun insert pred ins l let fun loop acc List revAppend acc ins loop acc l as x xs if pred ins x then List revAppend acc ins l else loop x acc xs in loop l end val rec lt fn x y gt x lt y in foldl insert lt l end 下面是希尔排序算法的原型实现 当输入列表趋于正序的时候 scatter函数将其分解为一组趋于反序的子列表 经过在输入趋于反序情况下性能最佳的变体插入排序后 gather函数再将它们合成为一个列表 fun shellSort l let fun insert pred ins l let fun loop acc List revAppend acc ins loop acc l as x xs if pred ins x then List revAppend acc ins l else loop x acc xs in loop l end val rec lt fn x y gt x lt y fun insertSort l foldl insert lt l fun scatter l n let fun dup n let fun loop acc i if i lt 0 then acc else loop acc i 1 in loop n end fun loop acc lol List revAppend acc lol loop l acc loop l rev acc loop x xs acc l ls loop xs x l acc ls in loop l dup n end fun gather lol let fun loop l rev l loop acc l loop rev acc l loop acc ls l loop acc ls l loop acc x xs ls l loop xs acc ls x l in loop lol end val gap let fun loop acc i let val h i 5 1 div 11 in if i lt 5 then rev 1 acc else loop h acc h end in loop length l end fun sort h l gather map insertSort scatter l h in foldl sort l gap end 希尔排序还可以采用Ciura提出的间隔序列 val incs 1750 701 301 132 57 23 10 4 1 val gap let fun loop acc i let val h i 4 1 div 9 fun iter incs if i gt hd incs 4 div 3 then incs else iter tl incs in if i lt hd incs 3 then List revAppend acc iter incs else loop h acc h end in if len 0 then 1 else loop len end 划分函数的实际实现 fun partition pred l let fun loop trueList falseList rev trueList rev falseList loop h t trueList falseList if pred h then loop t h trueList falseList else loop t trueList h falseList in loop l end 归并排序算法的自顶向下实现 fun mergeSort l let fun sort sort x x sort x y if x lt y then x y else y x sort x y z if x lt y then if y lt z then x y z else if x lt z then x z y else z x y else if x lt z then y x z else if y lt z then y z x else z y x sort l n let val m n div 2 fun split l acc i if i 0 then rev acc l else split tl l hd l acc i 1 fun merge p q let fun revMerge acc p q if not null p andalso not null q then if hd p lt hd q then revMerge hd p acc tl p q else revMerge hd q acc p tl q else if null p then List revAppend q acc else List revAppend p acc in rev revMerge p q end val ls rs split l m in merge sort ls m sort rs n m end in sort l length l end 堆排序算法的数组实现中 堆建造函数heapify也可以使用siftup函数的数组来完成 它将新节点自堆底向上插入到合适的位置 而不对途径节点左右子树顶点进行比较 fun siftup i let val ins get i fun loop i let val j i 1 div 2 in if i lt 0 orelse get j gt ins then set i ins else set i get j loop j end in loop i end fun heapify let fun loop i if i gt len 1 then else siftup i loop i 1 in loop 1 end 在堆排序算法的二叉树实现中 树插入和提取函数也可以写为等价的尾递归形式代码 exception Err fun revLink t t revLink Nil xs t revLink xs t revLink Leaf k xs t revLink xs Node k count t 1 t Nil revLink Node k c Nil r xs t revLink xs Node k c t r revLink Node k c l Nil xs t revLink xs Node k c l t revLink xs t raise Err fun insert t x let fun loop acc Nil x revLink acc Leaf x loop acc Leaf k l if l gt k then revLink acc Node l 2 Leaf k Nil else revLink acc Node k 2 Leaf l Nil loop acc Node k Leaf l Nil r if r gt k then revLink acc Node r 3 Leaf k Leaf l else if r gt l then revLink acc Node k 3 Leaf r Leaf l else revLink acc Node k 3 Leaf l Leaf r loop acc Node k c l r x let val k x if k gt x then k x else x k in if count l lt count r then loop Node k c 1 Nil r acc l x else if x gt key l then loop Node k c 1 Nil l acc r x else loop Node k c 1 l Nil acc r x end in loop t x end fun extract t let fun loop acc Nil revLink acc Nil loop acc Leaf revLink acc Nil loop acc Node l Nil revLink acc l loop acc Node c l r let val k key l val n left l in if n Nil then revLink acc Node k c 1 r Nil else if key n gt key r then loop Node k c 1 Nil r acc l else loop Node k c 1 r Nil acc l end in loop t end 堆排序算法的二叉树实现中 堆建造函数也可以主要采用siftdown函数来完成 这里不需要在节点中保存关于树状态的统计信息 fun heapSort l let datatype a heap Nil Node of a a heap a heap fun key Nil let val SOME a Int minInt in a end key Node k k fun left Nil Nil left Node l l fun right Nil Nil right Node r r fun leaf k Node k Nil Nil fun sift l r if l lt gt Nil andalso r lt gt Nil then if key l gt key r then l else r else if l lt gt Nil then l else if r lt gt Nil then r else Nil fun siftdown x l r let val superior sift l r in if superior Nil then Node x Nil Nil else if x gt key superior then Node x l r else if superior l then Node key l siftdown x left l right l r else Node key r l siftdown x left r right r end fun insert Nil x Node x Nil Nil insert Node k l r x let val superior sift l r in if x gt k andalso superior l then Node x l insert r k else if x gt k then Node x insert l k r else if superior l then Node k l insert r x else Node k insert l x r end fun extract Nil Nil extract Node l r let val superior sift l r in if superior Nil then Nil else if superior l then Node key l extract l r else Node key r l extract r end fun join l r extract Node key Nil l r fun heapify let fun init hs ls hs ls init hs ls x xs flag if flag then init leaf x hs ls xs false else init hs x ls xs true val hs ls init l true fun loop Nil loop h h loop x xs loop leaf x xs loop h x xs loop insert h x xs loop acc l loop acc l loop acc h l loop h acc l loop acc l r hs loop join l r acc hs loop acc l r hs x xs loop siftdown x l r acc hs xs in loop hs ls end fun generate h let fun loop acc Nil acc loop acc h loop key h acc extract h in loop h end in generate heapify end 稍加处理 堆建造函数也可以只用siftdown函数来完成 fun heapify let exception Err fun split let val rs ts let fun loop acci accj i n if i n then List revAppend accj acci else acci accj loop acci accj x xs i n if i n then loop List revAppend accj acci x xs i 1 n 2 1 else loop acci x accj xs i 1 n in loop l 0 1 end fun loop hs ls hs ls ts loop hs ls x xs flag if flag then loop x hs ls xs false else loop hs x ls xs true in loop rs true end fun init let val hs ls ts split fun loop acc acc ls loop acc ts acc List revAppend ts ls loop acc k hs loop leaf k acc hs loop acc k hs x let val k x if k gt x then k x else x k in loop Node k leaf x Nil acc hs end loop acc k hs l r rs let val k l r if k gt l then if l gt r then k l r else if k gt r then k r l else r k l else if k gt r then l k r else if l gt r then l r k else r l k in loop Node k leaf l leaf r acc hs rs end in loop hs ts end val hs ls init fun loop Nil loop h h loop raise Err loop h raise Err loop acc l loop acc l loop acc h l loop h acc l loop acc l r hs raise Err loop acc l r hs x xs loop siftdown x l r acc hs xs in loop hs ls end 排序算法的简单测试代码 fun printIntList l int list print String concatWith map Int toString l n fun shuffle l n let fun split l acc i if i 0 then acc l else split tl l hd l acc i 1 fun zip acc p q flag if null p then List revAppend q acc else if null q then List revAppend p acc else if flag then zip hd p acc tl p q false else zip hd q acc p tl q true val p q split l n div 2 in if null l then tl 0 else zip p q true end fun testsort f n let fun loop acc i if i lt 0 then acc else loop i acc i 1 val sl shuffle loop n n val ssl shuffle sl n in print source list is printIntList ssl print result list is printIntList f ssl end参见 编辑Standard ML和它的实现 SML NJ 由普林斯顿大学和贝尔实验室联合开发的实现 它具有并发编程扩展Concurrent ML MLton 严格遵循标准定义的强力的全程序优化 英语 Interprocedural optimization 编译器 50 HaMLet 51 由马克斯 普朗克软件系统研究所 英语 Max Planck Institute for Software Systems MPI SWS 的Andreas Rossberg编写 是一个SML解释器 意图成为精确且合宜接近的标准定义参考实现 OCaml 由法国国家信息与自动化研究所 INRIA 维护 是一个 工业强度 的ML方言 52 演化自最初用来实现Coq定理证明器的Caml 17 Alice 英语 Alice programming language 由萨尔兰大学设计的Alice ML 是基于Standard ML的函数式编程语言 扩展了对并发 分布式和约束式编程的丰富支持 53 ATS 英语 ATS programming language 由波士顿大学的Hongwei Xi和卡内基 梅隆大学的Frank Pfenning 英语 Frank Pfenning 提出的Dependent ML 英语 Dependent ML 发展而来 它向ML扩展了依赖类型 F 由微软研究院 MSR 开发 是一个基于OCaml的一个以 NET为目标的编程语言 F 由MSR和INRIA主导开发 是一个基于ML的依赖类型函数式编程语言 Futhark 由哥本哈根大学计算机科学系 英语 UCPH Department of Computer Science DIKU 开发 是属于ML家族的一个函数式 数据并行 阵列编程语言 4 Ur 由麻省理工学院的Adam Chlipala开发 是语法基于Standard ML的专门用于web开发的一个函数式编程语言 7 CM Lex和CM Yacc 由卡内基 梅隆大学的Karl Crary开发 是用于Standard ML OCaml和Haskell的词法分析器和语法解析器 54 Amulet 是一个类ML的函数式编程语言 其编译器输出Lua文件 55 Alpaca 是一个受ML启发的运行在Erlang虚拟机 英语 BEAM Erlang virtual machine 上的函数式编程语言 56 延伸阅读 编辑Robin Milner Mads Tofte 英语 Mads Tofte Robert Harper 英语 Robert Harper computer scientist The Definition of Standard ML PDF MIT Press 1990 2021 03 01 原始内容 PDF 存档于2021 01 14 Robin Milner Mads Tofte 英语 Mads Tofte Robert Harper 英语 Robert Harper computer scientist David MacQueen The Definition of Standard ML Revised PDF MIT Press 1997 2021 03 01 ISBN 0 262 63181 4 原始内容 PDF 存档于2022 03 09 Robin Milner Mads Tofte 英语 Mads Tofte Commentary on Standard ML MIT Press 1991 2021 08 31 ISBN 978 0 262 63137 2 原始内容存档于2021 08 31 Emden R Gansner John H Reppy The Standard ML Basis Library PDF Cambridge University Press 2004 2021 09 17 原始内容 PDF 存档于2022 01 29 Mads Tofte 英语 Mads Tofte Four Lectures on Standard ML PDF University of Edinburgh 1989 2021 09 04 原始内容 PDF 存档于2022 01 28 Code examples in lectures 2021 09 11 原始内容存档于2016 04 02 Mads Tofte 英语 Mads Tofte Essentials of Standard ML Modules DIKU 英语 UCPH Department of Computer Science 1996 2021 09 04 原始内容存档于2021 09 04 The SML code uuencoded compressed tar 2021 09 18 原始内容存档于2005 03 07 Mads Tofte 英语 Mads Tofte Tips for Computer Scientists on Standard ML Revised PDF ITU 英语 IT University of Copenhagen 2009 2021 09 04 原始内容 PDF 存档于2021 11 27 Examples 2022 01 03 原始内容存档于2017 09 15 Robert Harper 英语 Robert Harper computer scientist Programming in Standard ML PDF Carnegie Mellon University 2011 2021 02 27 原始内容 PDF 存档于2020 02 15 Examples 2021 09 12 原始内容存档于2021 09 12 Michael J C Gordon 英语 Michael J C Gordon Introduction to Functional Programming Cambridge University 1996 2021 09 11 原始内容存档于2021 04 11 Lecture notes 2021 09 11 原始内容存档于2006 06 23 Lawrence Paulson 英语 Lawrence Paulson ML for the Working Programmer 2nd Edition Cambridge University Press 1996 2021 08 31 ISBN 0 521 56543 X 原始内容存档于2022 02 24 Sample programs 2021 09 12 原始内容存档于2022 01 19 David MacQueen Should ML be Object Oriented PDF 2002 2021 09 10 原始内容 PDF 存档于2021 10 29 David MacQueen Robert Harper 英语 Robert Harper computer scientist John Reppy The History of Standard ML 2020 2021 08 31 原始内容存档于2021 12 01 Andrew W Appel 英语 Andrew W Appel Compiling with Continuations Cambridge University Press 1992 2022 01 03 原始内容存档于2022 01 03 Andrew W Appel 英语 Andrew W Appel Modern Compiler Implementation in ML Cambridge University Press 1998 2022 01 12 原始内容存档于2022 01 12 Tiger compiler modules for programming exercises 2021 09 12 原始内容存档于2022 05 06 Jeffrey D Ullman Elements of ML Programming ML97 Edition Prentice Hall 1998 2021 12 30 ISBN 0 13 790387 1 原始内容存档于2022 03 12 Programs from the text 2022 01 01 原始内容存档于2022 02 14 Anthony L Shipman Unix System Programming with Standard ML PDF 2001 2021 09 01 原始内容 PDF 存档于2021 01 21 引用 编辑 1 0 1 1 1 2 1 3 Michael J Gordon Arthur J Milner Christopher P Wadsworth Edinburgh LCF A Mechanised Logic of Computation Lecture Notes in Computer Science Vol 78 Springer Verlag New York NY USA 1979 2021 12 28 原始内容存档于2021 12 28 ML is a general purpose programming language It is derived in different aspects from ISWIM POP2 and GEDANKEN and contains perhaps two new features First it has an escape and escape trapping mechanism well adapted to programming strategies which may be in fact usually are inapplicable to certain goals Second it has a polymorphic type discipline which combines the flexibility of programming in a typeless language with the security of compile time type checking as in other languages you may also define your own types which may be abstract and or recursive this is what ensures that a well typed program cannot perform faulty proofs Michael J C Gordon 英语 Michael J C Gordon From LCF to HOL a short history 1996 2021 02 27 原始内容存档于2016 09 05 Around 1973 Milner moved to Edinburgh University and established a project to build a successor to Stanford LCF which was subsequently dubbed Edinburgh LCF He initially hired Lockwood Morris and Malcolm Newey both recent PhD graduates from Stanford as research assistants Milner ably assisted by Morris and Newey designed the programming language ML an abbreviation for Meta Language In 1975 Morris and Newey took up faculty positions at Syracuse University and the Australian National University respectively and were replaced by Chris Wadsworth and myself The design and implementation of ML and Edinburgh LCF was finalised and the book Edinburgh LCF was written and published In 1978 the first LCF project finished Chris Wadsworth went off trekking in the Andes returning to a permanent position at the Rutherford Appleton Laboratory and I remained at Edinburgh supported by a postdoctoral fellowship and with a new research interest hardware verification 2 0 2 1 M Gordon R Milner L Morris M Newey C Wadsworth A Metalanguage for Interactive Proof in LCF PDF 1978 2021 08 31 原始内容 PDF 存档于2021 05 06 ML is a higher order functional programming language in the tradition of ISWIM PAL POP2 and GEDANKEN but differs principally in its handling of failure and more so of types 3 0 3 1 Bruce A Tate Fred Daoud Ian Dees Jack Moffitt 3 Elm Seven More Languages in Seven Weeks PDF Book version P1 0 November 2014 The Pragmatic Programmers LLC 2014 97 101 2021 09 04 ISBN 978 1 941222 15 7 原始内容 PDF 存档于2021 03 15 On page 101 Elm creator Evan Czaplicki says I tend to say Elm is an ML family language to get at the shared heritage of all these languages these languages is referring to Haskell OCaml SML and F 4 0 4 1 Troels Henriksen Niels G W Serup Martin Elsman Fritz Henglein Cosmin Oancea Futhark Purely Functional GPU Programming with Nested Parallelism and In Place Array Updates PDF Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation PLDI 2017 ACM 2017 2021 09 04 原始内容 PDF 存档于2020 09 20 Lennart Augustsson 英语 Lennart Augustsson Thomas Johnsson The Chalmers Lazy ML Compiler 1989 2021 09 17 原始内容存档于2021 09 17 6 0 6 1 Programming language for special forces of developers Russian Software Development Network Nemerle Project Team January 24 2021 原始内容存档于2021 05 04 7 0 7 1 Adam Chlipala Ur Web A Simple Model for Programming the Web PDF MIT Association for Computing Machinery ACM January 2015 2021 09 04 原始内容 PDF 存档于2022 01 16 8 0 8 1 Robin Milner A theory of type polymorphism in programming PDF 1978 2021 09 01 原始内容 PDF 存档于2020 11 01 Journal of Computer and System Sciences 17 3 348 375 Robin Milner How ML Evolved PDF Polymorphism The ML LCF Hope Newsletter Vol 1 No 1 1982 2021 09 09 原始内容 PDF 存档于2022 01 28 The original Edinburgh LCF 1977 2021 10 10 原始内容存档于2021 10 10 Luca Cardelli 英语 Luca Cardelli ML under VMS PDF 1982 2021 09 04 原始内容 PDF 存档于2021 11 06 Luca Cardelli Differences between VAX and DEC 10 ML PDF 1982 2021 09 04 原始内容 PDF 存档于2021 11 06 Luca Cardelli 英语 Luca Cardelli The Functional Abstract Machine 1983 2021 09 04 原始内容存档于2021 09 04 Bell Labs Technical Report TR 107 Luca Cardelli Compiling a functional language 1984 2021 09 03 原始内容存档于2021 09 03 In Proceedings of the 1984 ACM Symposium on LISP and Functional Programming pages 208 217 New York NY USA ACM Kevin Mitchell Alan Mycroft The Edinburgh Standard ML Compiler PDF 1985 2021 09 10 原始内容 PDF 存档于2022 01 29 15 0 15 1 Guy Cousineau Gerard Huet 英语 Gerard Huet The CAML primer Version 2 6 1 1990 2021 09 02 原始内容存档于2022 05 04 RT 0122 INRIA pp 78 Pierre Weis Maria Virginia Aponte Alain Laville Michel Mauny Ascander Suarez The CAML reference manual Version 2 6 1 1990 2021 09 02 原始内容存档于2022 04 06 Research Report RT 0121 INRIA pp 491 G Cousineau M Gordon G Huet R Milner L C Paulson C Wadsworth The ML Handbook Version 6 2 Internal document Project Formel INRIA July 1985 Christoph Kreitz Vincent Rahli Introduction to Classic ML PDF 2011 2021 09 09 原始内容 PDF 存档于2022 01 29 This handbook is a revised edition of Section 2 of Edinburgh LCF by M Gordon R Milner and C Wadsworth published in 1979 as Springer Verlag Lecture Notes in Computer Science no 78 The language is somewhere in between the original ML from LCF and standard ML since Guy Cousineau added the constructors and call by patterns This is a LISP based implementation compatible for Maclisp on Multics Franzlisp on VAX under Unix Zetalisp on Symbolics 3600 and Le Lisp on 68000 VAX Multics Perkin Elmer etc Video interfaces have been implemented by Philippe Le Chenadec on Multics and by Maurice Migeon on Symbolics 3600 The ML system is maintained and distributed jointly by INRIA and the University of Cambridge 17 0 17 1 A History of Caml 2021 08 31 原始内容存档于2022 04 13 The Formel team became interested in the ML language in 1980 81 Gerard Huet decided to make the ML implementation compatible with various Lisp compilers MacLisp FranzLisp LeLisp ZetaLisp This work involved Guy Cousineau and Larry Paulson Guy Cousineau also added algebraic data types and pattern matching following ideas from Robin Milner At some point this implementation was called Le ML a name that did not survive It was used by Larry Paulson to develop Cambridge LCF and by Mike Gordon for the first version of HOL Our main reason for developing Caml was to use it for sofware development inside Formel Indeed it was used for developing the Coq system We were reluctant to adopt a standard that could later prevent us from adapting the language to our programming needs We did incorporate into Caml most of the improvements brought by Standard ML over Edinburgh ML The first implementation of Caml appeared in 1987 and was further developed until 1992 It was created mainly by Ascander Suarez In 1990 and 1991 Xavier Leroy designed a completely new implementation of Caml based on a bytecode interpreter written in C Damien Doligez provided an excellent memory management system In 1995 Xavier Leroy released Caml Special Light which improved over Caml Light in several ways In 1995 Xavier Leroy released Caml Special Light which improved over Caml Light in several ways First an optimizing native code compiler was added to the bytecode compiler Second Caml Special Light offered a high level module system designed by Xavier Leroy and inspired by the module system of Standard ML Didier Remy later joined by Jerome Vouillon designed an elegant and highly expressive type system for objects and classes This design was integrated and implemented within Caml Special Light leading to the Objective Caml language and implementation first released in 1996 and renamed to OCaml in 2011 Lawrence C Paulson The theorem prover Cambridge LCF coded in Franz Lisp 1989 2021 10 10 原始内容存档于2021 10 10 Michael J C Gordon 英语 Michael J C Gordon From LCF to HOL a short history 1996 2021 02 27 原始内容存档于2016 09 05 In 1981 I moved to a permanent position as Lecturer at the University of Cambridge Computer Laboratory Larry Paulson recently graduated with a PhD from Stanford was hired at Cambridge About this time and in parallel G erard Huet ported the Edinburgh LCF code to Lelisp and MacLisp Paulson and Huet then established a collaboration and did a lot of joint development of LCF by sending each other magnetic tapes in the post Edinburgh LCF ran interpretively but during Paulson and Huet s collaboration an ML compiler was implemented that provided a speedup by a factor of about twenty The resulting new LCF system was named Cambridge LCF and completed around 1985 Paulson did little work on it after that Mikael Hedlund of the Rutherford Appleton Laboratory then ported Cambridge LCF to Standard ML using a new implementation of ML that he created The resulting Standard ML based version of Cambridge LCF is documented in Paulson s 1987 book Logic and Computation HOL88 source code Michael J C Gordon 英语 Michael J C Gordon From LCF to HOL a short history 1996 2021 02 27 原始内容存档于2016 09 05 Whilst Paulson was designing and implementing Cambridge LCF I was mainly concerned with hardware verification The first version of the HOL system was created by modifying the Cambridge LCF parser and pretty printer to support higher order logic concrete syntax The core HOL system became stable in about 1988 A new release that consolidated various changes and enhancements called HOL88 was issued then We were fortunate to receive support from DSTO Australia to document HOL and from Hewlett Packard to port it from Franz Lisp to Common Lisp a job very ably done by John Carroll In the late 1980 s Graham Birtwistle of the University of Calgary started a project to reimplement HOL in Standard ML The work was done by Konrad Slind under Birtwistle s direction and with the collaboration of the HOL group at Cambridge The resulting system called HOL90 was first released around 1990 Recently John Harrison and Konrad Slind have entirely reworked the design of HOL This new version of HOL is called HOL Light It is implemented in Caml Light and runs on modest platforms e g standard PCs It is faster than the Lisp based HOL88 but a bit slower than HOL90 running in modern implementations of Standard ML Robin Milner A Proposal for Standard ML PDF 1983 2021 09 02 原始内容 PDF 存档于2021 11 06 R M Burstall J A Goguen The semantics of CLEAR a specification language 1977 2021 09 03 原始内容存档于2021 09 03 Donald Sannella Semantics Implementation and Pragmatics of Clear a Program Specification Language 1982 2021 09 06 原始内容存档于2021 09 06 Rod Burstall 英语 Rod Burstall D B MacQueen D T Sannella 英语 Don Sannella Hope An Experimental Applicative Language PDF 1980 2021 09 03 原始内容 PDF 存档于2022 01 28 Conference Record of the 1980 LISP Conference Stanford University pp 136 143 R M Burstall Proving properties of programs by structural induction PDF 1968 2021 09 13 原始内容 PDF 存档于2022 01 28 R M Burstall J Darlington A transformati, 维基百科,wiki,书籍,书籍,图书馆,

文章

,阅读,下载,免费,免费下载,mp3,视频,mp4,3gp, jpg,jpeg,gif,png,图片,音乐,歌曲,电影,书籍,游戏,游戏。