SML 基础

ML Basics.

绑定 (binding) 与我们熟悉的赋值语句 (assignment statement) 尽管形式相似，却有着本质的不同：最主要的区别在于 bindings 是 immutable 的，而 assignment statement 支持以赋值的形式 mutate 变量的值。

• Each binding gets type-checked and (assume it type-checks) then evaluated.
• What type of a binding has depends on a static environment or context, which is roughly the types of the preceding bindings.
• How a binding is evaluated depends on a dynamic environment or just environment, which is roughly the values of the preceding bindings.

这也就是说，if x maps to some value v in some environment, it will forever map to v in that environment. There is NO assignment statement that changes x to map to a different value. 尽管你可以在之后引入新的 binding 来 shadows x，但这并不会改变之前的环境中 x 与 v 对应的事实。

接下来，我们看看 ML 如何处理 variable bindings 与 function bindings。

Variable Bindings

variable binding 的语法 (syntax) 如下：

1

var x = e;

e 是一个表达式 (expression)；注意表达式与值 (value) 之间的区别：A value is an expression that “has no more computation to do”. Therefore, all values are expressions, but not all expressions are values.

• We use current static environment to type-check e, and (if it type-checks) add x : t back to the static environment where t is the type of e.
• We use current dynamic environment to evaluate e, and (if it type-checks) add x = v back to the dynamic environment where v is the value of e.

Function Bindings

function binding 的语法如下：

1

fun x0 (x1:t1, ..., xn:tn) = e

Binding x0 takes arguments x1, ..., xn of types t1, ..., tn and has an expression e for its body.

Type-checking:

• Type-check the body e in a static environment that (in addition to all the earlier binding) maps x1 to t1, … xn to tn and x0 to t1 * ... * tn -> t. Since x0 is in the environment, we can make recursive function calls, i.e., a function definition can use itself.
• For the function binding to type-check, body e must have the type t, i.e., the result type of x0.
• If the function binding type-checks, x0 : t1 * ... * tn -> t is added to the static environment. Note that the arguments are not added to the top-level static environment.

Note that t is never wrote down: it is up to the type-checker to figure out what t should be such that using it for the result type of x0 makes everything work out. This is called type inference.

**Evaluation: **

function bindings 的 evaluation 就比较 trivial 了，这是因为在 ML 中，A function is a value.

我们仅仅需要将 x0 加入 current dynamic environment 即可。As expected for recursion, x0 is in the dynamic environment in the function body and for subsequent bindings.

Function Call

function binding 的存在是为了支持 function calls。它的语法如下：

1

e0 (e1,...,en)

Typing rules:

若 e0 的类型为 t1 * ... * tn -> t 且 ei 的类型为 ti，则整个函数调用的类型为 t.

Evaluation rules:

我们使用调用处的环境 (environment at the point of the call) 来 evaluate e0 to v0, e1 to v1, …, en to vn. 若 v0 是函数，则函数调用是 type-checked 的。

接下来，我们使用定义处的环境 (environment where the function is defined) extends 函数参数形成的 bindings x1 = v1, ..., xn = vn 来 evaluate 函数体。