用ML编写正确的程序 ML – Programming Correctly

Presentation on theme: "用ML编写正确的程序 ML – Programming Correctly"— Presentation transcript:

1 用ML编写正确的程序 ML – Programming Correctly
汪旻

2 函数式程序设计 过程式语言面向命令，函数式语言面向表达式 函数式语言避免繁琐的内存管理 函数式语言要求写出可靠正确的程序
函数式语言的几个概念 函数，递归，模式匹配，多态类型检测，高阶函数，无穷数据结构，惰性求值

3 ML与纯函数式编程语言的区别   ML是非纯函数式语言 热情求值 没有无穷数据结构 模块 …… 多态类型检测 异常处理 简单的IO指令 ……

4 ML的诞生 ML(Meta-Language) 是一个通用的函数式编程语言，它是由 爱丁堡大学的Robin Milner在二十世纪七十年代晚期开发的， 现在流行的方言有Standard ML和Caml. 启发语言：ISWIM 影响语言：Miranda, Haskell, Cyclone, C++, F#, Clojure, Felix, Opa, Erlang …… 设计初衷：LCF定理证明机中寻找证明策略 ML大多被用于语言设计和操作（编译器、分析器、定理证明 机）， 但是它作为通用语言也被用于生化，金融系统，和 宗谱数据库，一个P2P的客户／服务器程序等等。

5 Level 0 猿 Hello world 阶乘函数 “Hello world!”; (*make a string*)
print it; (*output it*) 阶乘函数 fun fac 0 = 1 | fac n = n * fac (n - 1); Level Up! 猿 LV.0 ML Programmer LV.1 ML Programmer

6 Level 1 值的声明 命名常量 声明函数 标识符 val pi = 3.14159;
fun circle_area (r) = pi*r*r; 标识符 字母开头，允许数字、下划线、撇号’

7 Level 1 ↓ 基本类型 数 字符串 真值 int, real + - * div mod ~ 负号 类型约束 连接符^
#”0”和“0” 真值 orelse, andalso, not if E then E1 else E2 - fun square x = x*x; ↓ - fun square x = x*x :real;

8 Level 1 猿 序偶、元组、记录 序偶 记录 Level Up! 向量(2.5 , ~1.2) : real*real
type vec = real * real; 记录 val ZS = {name=“Zhang San”, age=20, major=“CS”}; #age ZS; > 20 : int Level Up! 猿 LV.1 ML Programmer LV.2 ML Programmer

9 Level 2 表达式 局部声明 中缀操作符(infix operator)及其优先级、结合方式 传值调用(add….)
let ... in ... end local ... in ... end 支持嵌套

10 (* Example for infix operator *)
infix xor; fun (p xor q) = (p orelse q) andalso not (p andalso q); (* 中缀优先级 *) infix 7 times; (* 传值调用 *) sqr(sqr(sqr(2))) zero(sqr(sqr(sqr(2))) =sqr(sqr(2*2)) =zero(sqr(sqr(2*2))) =sqr(sqr(4)) =zero(sqr(sqr(4))) =sqr(4*4) =zero(sqr(4*4)) =sqr(16) =zero(sqr(16)) =16*16 =zero(16*16) =256 =zero(256) =0 .

11 猿 Level Up! (* Example for let ... in ... end *) fun fraction (n,d) =
let val com = gcd(n,d) in (n div com, d div com) end; > val fraction = fn : int * int -> int * int (* Example for local ... in ... end *) local fun itfib (n, prev, curr) : int = if n=1 then curr else itfib (n-1, curr, prev+curr) in fun fib (n) = itfib(n, 0, 1) > val fib = fn ; int -> int Level Up! 猿 LV.2 ML Programmer LV.3 ML Programmer

12 Level 3 模块系统 结构 通过Conplex.zero这样的形式来访问 不同结构里的标识符可以相同 签名

13 猿 Level Up! LV.4 LV.3 ML Programmer ML Programmer
structure Complex : ARITH = struct type t = real*real; val zero = (0.0, 0.0); fun sum ((x,y), (x',y')) = (x+x', y+y') : t; fun diff ((x,y), (x',y')) = (x-x', y-y') : t; fun prod ((x,y), (x',y')) = (x*x' - y*y', x*y' + x'*y) : t; fun recip (x,y) = let val t:real = x*x + y*y in (x/t, ~y/t) end fun quo (z,z') = prod(z, recip z'); end; signature ARITH = sig type t val zero : t val sum : t * t -> t val diff : t * t -> t val prod : t * t -> t val quo : t * t -> t Level Up! 猿 LV.3 ML Programmer LV.4 ML Programmer

14 Level 4 猿 多态类型检测 多态类型的声明 关于算法（Damas(1985)的博士论文） Level Up! LV.5 LV.4
- fun pairself x = (x,x); > val pairself = fn : ‘a -> ‘a * ‘a fun fst (x,y) = x; > val fst = fn : ‘a * ‘b -> ‘a fun snd (x,y) = y; > val snd = fn : ‘a * ‘b -> ‘b Level Up! 猿 LV.4 ML Programmer LV.5 ML Programmer

15 Level 5 猿 List :: _ 顺序 [3, 4] 可重复 [3, 4, 3] 元素类型任意 Level Up!
顺序 [3, 4] 可重复 [3, 4, 3] 元素类型任意 [(1,”one”),(2,”two”),(3,”three”)] : (int*string) list :: 右结合中缀操作符cons 在表前加入一个元素 _ 通配符 Level Up! 猿 LV.5 ML Programmer LV.6 ML Programmer

16 Level 6 数据类型声明 datatype person = King | Peer of string*string*int
| Knight of string | Peasant of string; fun title King = "His Majesty the King“ | title (Peer(deg,terr,_)) = "The " ^ deg ^ " of " ^ terr | title (Knight name) = "Sir " ^ name | title (Peasant name) = name;

17 Level 6 树 节点=节点+子树or叶子 size(tree) 应用
datatype ‘a tree = Lf | Br of ‘a tree * ‘a tree; size(tree) 应用

18 val tree2 = Br(2, Br(1,Lf,Lf), Br(3,Lf,Lf));
val tree4 = Br(4, tree2, tree5); 4 2 1 3 5 6 7

19 （* make a tree *） datatype 'a tree = Lf | Br of 'a * 'a tree * 'a tree; structure Tree = struct fun size Lf = 0 | size (Br(v,t1,t2)) = 1 + size t1 + size t2; fun depth Lf = 0 | depth (Br(v,t1,t2)) = 1 + Int.max (depth t1, depth t2); fun reflect Lf = Lf | reflect (Br(v,t1,t2)) = Br(v, reflect t2, reflect t1); .... end;

20 （* 二叉查找树 *） (*** Dictionaries as Binary search trees ***)signature DICTIONARY = sig type key (*type of keys*) type 'a t (*type of tables*) exception E of key (*errors in lookup, insert*) val empty: 'a t (*the empty dictionary*) val lookup: 'a t * key -> 'a val insert: 'a t * key * 'a -> 'a t val update: 'a t * key * 'a -> 'a t end; (*Structure Order can vary; Tree avoids referring to a free structure. *) structure Dict : DICTIONARY = struct type key = string; type 'a t = (key * 'a) tree; exception E of key; val empty = Lf;

21 猿 Level Up! LV.7 LV.6 ML Programmer ML Programmer
fun lookup (Lf, b) = raise E b | lookup (Br ((a,x),t1,t2), b) = (case String.compare(a,b) of GREATER => lookup(t1, b) | EQUAL => x | LESS => lookup(t2, b)); fun insert (Lf, b, y) = Br((b,y), Lf, Lf) | insert (Br((a,x),t1,t2), b, y) = GREATER => Br ((a,x), insert(t1,b,y), t2) | EQUAL => raise E b | LESS => Br ((a,x), t1, insert(t2,b,y))); fun update (Lf, b, y) = Br((b,y), Lf, Lf) | update (Br((a,x),t1,t2), b, y) = GREATER => Br ((a,x), update(t1,b,y), t2) | EQUAL => Br ((a,y), t1, t2) | LESS => Br ((a,x), t1, update(t2,b,y))); end; Level Up! 猿 LV.6 ML Programmer LV.7 ML Programmer

22 后期升级攻略 函数与算子 实现惰性求值 实现搜索策略 函数式程序正确性的证明 抽象类型（用于建立大型系统） ML中的命令式程序设计
应用：LAMBDA演算解释器

23 总结 用ML可以很容易写出清晰、可靠的程序。值得作为函数式编程的入门语言。
在牺牲部分效率的情况下，提升程序的安全性是十分必要的。因为在函数式编程里，正确性第一，清晰性次之，效率排在第三位。 ML在运行前会检查所有的类型和接口以防止出错，让程序员将更多的精力放在丰富语言上，而不是冗长又无用的调试和测试。 ML远没有这次所展示的这么少，它的强大之处还待继续去深入地了解。

24 参考资料 ML for the Working Programmer Second Edition, Lawrence C. Paulson
en.Wikipedia.org - ML (programming language) Functional programming 3. A Gentle Introduction to ML, Andrew Cumming, Computer Studies, Napier University 4. The ML Language - Typed Functional Programming with Assignments

25 问答 谢谢聆听