函数式编程语言、编程和程序验证

函数式编程语言、编程和程序验证内容摘要：

type student = { name : string。 age : int。 score : real } type student 记录是具有标签的元组 函数式语言 SML及编程简介 • 例 4（多态类型） fun gcd(m, n) = if m = 0 then n else gcd(n mod m, m)。 其中的 if … then …else 是一个内部定义的多态函数 if … then …else = fn : bool  a  a  a 其中 a是类型变量，类型变量以撇号开始 函数式语言 SML及编程简介 • 例 4（多态函数）取二元组的第 1元和第 2元 fun fst(x, y) = x。 val fst = fn : a  b  a fun snd(x, y) = y。 val snd = fn : a  b  b 函数式语言 SML及编程简介 • 表的简介 – 表（ list）是相同类型元素的有限序列 – 如： [3, 5, 9], [ (1, “one”), (2, “two”), (3, “three”) ] – 表的构造符 空表： [ ] 在已有的表前加入一个元素： :: 9 :: [ ] = [9], 5 :: [9] = [5, 9] – 基本的表函数 null（测试空表）、 hd（返回表头元素）、 tl（返回非空表的表尾）、 length（返回表长） 函数式语言 SML及编程简介 • 例 5（表类型）计算表的长度 fun length [ ] = 0 | length (x :: xs) = 1 + length xs。 val length = fn : a list int length [3, 5, 9] length [“one”, “two”, “three”] 3 : int 3 : int – 竖线“ | ”将函数声明分成两子句，各处理一个模式 – length是一个多态类型的函数 – list相当于一个类型构造符 函数式语言 SML及编程简介 • 例 6（表类型）插入排序 fun insert(x, [ ]) : real list = [ x ] | insert(x, y :: ys) = if x = y then x :: y :: ys else y :: insert(x, ys)。 val insert = fn : real  real list real list – 排序需要用到两个变元的比较运算，关系运算“ =”不是多态的，因此 insert不是多态函数 – 在第 1行上给出函数的结果类型就是为了避免类型推断出现错误 函数式语言 SML及编程简介 • 例 7（表类型）基于表的一个高阶函数 fun map f [ ] = [ ] | map f (x :: xs) = (f x) :: map f xs。 val map = fn : (a b) (a list b list) – 算子 map把函数 f 应用到表的每个元素上，即 map f [x1, …, x n] = [f x1, …, f x n] – map f的结果是一个新函数 函数式语言 SML及编程简介 • 例 8 静态作用域（静态绑定） let val x = 2 fun f y = x + y /* x是函数 f的非局部变。