SML学习笔记02-求值，类型，绑定与范围

参考：CMU 15-150 Lecture01

1 SML语言哲学

  • 计算是函数式的
  • 编程是一个阐明的过程

1.1 计算是函数式的

所有的计算都可以看成是函数式的

函数将值（等号左侧的值）映射到另一个值上（等号右侧的值）

1.1.1 指令式编程与函数式编程的区别

指令式编程：

  命令 -> 被执行，并且产生一个影响 -> 该影响即是一个状态：变量的状态被改变（如：命令执行完后变量x=5）

函数式编程：

  表达式 -> 被求值，并且不会产生影响 -> 仅得到一个值而已（如：表达式被求值完仅得到3+4这个值）

1.2 编程是一个阐明的过程

面对一个问题进行编程时，我们需要先阐明该问题中的不变量、规范以及我们算法正确性的证明。都阐明完毕后我们最后才开始针对问题进行编程。

阐明的过程也即是 对问题进行分析 -> 分解 -> 找到合适的算法解法 -> 证明该方法正确性 的过程

2 定义ML语言

我们学习的是 Standard ML，即标准的 ML。我们在此定义 ML 语言

ML 有三个元素：

  • 类型 \(t\)
  • 表达式 \(e\)
  • 值 \(v\)（值也是表达式的一个子集）

2.1 类型

何为类型？类型是对表达式化简所得最终值的类型的预测。

例：

  • 表达式 \(3+4\) 的类型是整数，因为我们可以预测出 \(3+4\) 化简完的最终值是 \(7\) ，而 \(7\) 是个整数，所以表达式的类型是整数
  • 表达式 \(5\) 的类型也是整数，因为我们可以预测出 \(5\) 化简完还是 \(5\) ，是个整数

为何 \(5\) 也称作表达式？因为在上文ML的三个元素中我们提到 值 \(v\) 是表达式的一个子集，所以 \(5\) 自然也是表达式

  • 而表达式 \(2+"String"\) 就没有类型，因为我们无法预测出一个整型 \(+\) 一个字符串会得到什么类型

2.1.1ML语言的类型

基本类型

  int, real, bool, char, string

构造类型

  乘积类型，函数类型，用户定义类型

2.1.2 well-typed, type-checks 以及 ill-typed

well-typed 与 type-checks:

  当一个表达式至少存在一种类型时即可称其为 well-typed 或 type-checks

注意：

  符号 “ \(:\) ”表示 “有一个类型”

  如：\(e:t\) 表示 \(e\) 有一个类型 \(t\) ，并不意味着 \(e\) 只有一种类型 \(t\)

ill-typed:

  不属于 well-typed 与 type-checks 的表达式都称为 ill-typed

2.1.3 类型与 ML 编译器

首先对表达式做一个 type-checks

如果表达式是 well-typed

那么就对表达式求值

2.2 表达式

每一个符合语法规则的 ML 表达式 \(e\)

  • 都有个类型 \(t\)，记作 \(e : t\)
  • 或许会有个值 \(v\)，记作 \(e \hookrightarrow v\)
  • \(e\) 能化简为 \(e'\)，记作 \(e\Rightarrow e'\)

例：

  • \((3+4)\times2 : int\)
  • \((3+4)\times2 \hookrightarrow 14\)
  • \(5\div0:int\)
  • \(5\div0\) 没有值

2.2.1 表达式类型的确定

  • 对于值来说，表达式的类型可以直接确定，如：\(5:\) int
  • 对于含运算符的表达式来说，我们通过以下两点来确定一个表达式的类型
    1. 将运算符号看作一个函数，明确其接受参数的类型以及返回值的类型
    2. 确定参与运算的每个值的类型

举例说明：

  \(if\ e_1:\) int \(\ and\ \ e_2:\) int

  \(and\ +\ \)运算 以两个 int 类型作为参数时，将同样返回一个 int 类型

  \(i.e.\ \ e_1+e_2:\) int

更具体地：

  \((3+4)\times2:\) int

    因为：\(3:\) int 且 \(4:\) int

    且\(\ +\ \)运算 以两个 int 类型作为参数时，将同样返回一个 int 类型

    所以：\((3+4):\) int

    又因为：\((3+4):\) int 且 \(2:\) int

    且\(\ \times\ \)运算以两个 int 类型作为参数时，将同样返回一个 int 类型

  所以：\((3+4)\times2:\) int

3 扩展等价\(\ \cong\ \)

扩展等价描述的是同种类型表达式之间的一种等价关系

3.1 表达式的扩展等价

两个表达式是 扩展等价的 当两个表达式是同类型的，并且满足下列条件之一：

  • 两个表达式都能化简求得相同的值
  • 两个表达式都会引发相同的异常
  • 两个表达式都会永远循环下去

3.2 函数的扩展等价

两个函数之间是 扩展等价的 当它们能把等价的参数映射到等价的结果

在证明中，我们用\(\ \cong\ \)来表达 “ 等价于 ” 的含义

例：

  • \(21+21\)\(\ \cong\ \)\(42\)\(\ \cong\ \)\(6\times7\)

  • \([2,7,6]\)\(\ \cong\ \)\([1+1,2+5,3+3]\)

  • \((fn\ x=>x+x)\)\(\ \cong\ \)\((fn\ y=>2\times y)\)

3.2.1 函数式编程的参考通透

函数式编程的参考通透意为：

  • 表达式的值仅取决于其子表达式的值
  • 表达式的类型仅取决于其子表达式的类型

4 乘积表达式

\((e_1,e_2):t_1* t2\)

  \(if\ e_1:t_1\ and\ e_2:t_2\)

类型：\(t_1*t_2\)

值：\((e_1,e_2)\)

例：

  \((3+4,true):int*bool\)

5 函数

在数学中，我们会说一个函数 \(f\) 将 \(X\) 空间映射到 \(Y\) 空间，记作\[f:X\to Y\]

在 SML 中同样如此，只是 \(X\) 和 \(Y\) 变成了类型

注意：

  在计算时，一个函数不总会返回一个值。此时检查等价性会变得复杂。

5.1 函数的完全性

定义：

  当对于 \(X\) 中的每一个值 \(x\) , \(f(x)\) 都能返回一个值，则称该函数 \(f\) 是完全的

完全性是数学和计算之间的一个关键区别

6 声明

6.1 最基本的声明表达式

1
2
3
val pi:real = 3.14
//也即：
//关键词 标识符:类型 = 值

本语句介绍了 pi 与 3.14 的结合，有时写作 [ 3.14 / pi ]

注意：

  形如：[ 3.14 / pi ] 的写法仅用于表达一种值与变量名间的绑定关系，并不是 Standard ML 语言中的一条合法语句。

例：

1
2
3
4
val x:int = 8-5;		//意为[3/x]
val y:int = x+1;		//意为[4/y]
val x:int = 10;			//意为[10/x]
val z:int = x+1;		//意为[x+1]

6.2 本地声明

本地声明也即 let...in...end 语句

其中let之后，in之前的语句用来声明变量，这些变量的作用域仅限于in之后，end之前的区域。

in之后，end之前仅能写一条语句，该语句的值和类型将作为此本地声明语句的值和类型。并且这条仅能使用上文let后所声明过的变量

end; 代表着本地声明语句的结束，本地声明语句一结束，其内定义过的变量将立即被销毁。

例：

1
let val m:int = 6 val n:int = 7 in m*n end;

也可写作

1
2
3
4
5
6
let					//下面声明的变量作用域仅限于in后，end前
	val m:int = 6
	val n:int = 7
in
	m*n				//仅能包含一条语句
end;				//本地声明语句结束，m与n变量被销毁，无法再被下文调用

在本例中，m*n 的值为 42，类型为 int。所以此本地声明表达式的值便是 42，类型便是 int

运行图示：

可以看到，整个本地声明表达式的值为 42，类型为 int。同时再 end; 结束本地声明表达式后，我们尝试再次访问其内定义过的 m 变量，发现无法访问： "stdIn: 18.1 Error: unbound variable or constructor: m"

6.3 类型定义表达式

例：

1
2
3
type float = real;				//定义 float 类型
type point = float*float;		//定义 point 类型
val p:point = (1.0,2.6);		//定义 point 类型的变量 p

运行图例

可以看到，用户将 real*real 类型自定义为 point 类型。最终的变量 p 值为 (1.0 , 2.6) 类型为 point。

6.4 函数的声明

Standard ML中支持两种声明函数的方式：

  1. 匿名声明： 
    1
    fn (x : int) => x * x;
  2. 非匿名声明： 
    1
    fun square (x : int) : int = x * x;

如图：两种方式都可以正确地声明一个函数

6.4.1 函数的匿名声明

1
fn (x : int) => x * x;

函数的匿名声明由三部分组成：

  1. 关键字：fn
  2. 参数名与其类型：(x : int)
  3. 函数体：x * x

注意：

  如上例代码所示，函数的匿名声明不要写出其返回值类型

6.4.2 函数的非匿名声明

1
fun square (x : int) : int = x * x;

square为函数名，又称该函数的标识符。

函数的非匿名声明会将其标识符（函数名）与一个 closure 绑定

而一个 closure 由两个部分组成：

  1. 一个 lambda 表达式（又称匿名函数值）：
1
fn (x : int) => x * x;
  1. 一个环境：

  意即：函数将用到的所有的值绑定

一个形象的图例：