函数（funciton）：

1. 实例

val fun myPlus(a : int, b : int) = a + b
val fun myPow(x: int, y : int) = 
  if y = x                                           错误 if y = 0
  then 1
  else x * myPow(x, y - 1)
调用
myPlus(5, 6)
myPow(2, 4)

2. 函数绑定：

val fun e0(t1, t2, t3..., tn) = e;

2019/07/24 20:38:00 纠正
val fun x0(x1 : t1, x2 : t2, x3 : t3..., xn : tn) = e;

1. 语法（syntax）：

• fun 关键字，表明这是一个函数
• fun后是函数的名字，在定义后，我们就可以在后面的环境中使用它。（补充：同时允许让函数拥有调用自己的能力，即迭代）
• 函数名后紧跟括号，里面是该函数需要的参数，多个参数使用“,”分隔，其中参数与类型，用“:”分割
• = 后是函数体，函数体即该函数可以完成的任务，或者说该函数的能力。

2. 类型检查（type check）：
2019/07/24 20:38:00 补充

• 添加一个新的函数类型到静态环境：x0 : t1 * t2 * t3...tn -> t（函数类型：以“*”分割所有使用到的类型绑定，“-> t” 箭头代表，若进行恰当的类型检查将得到结果t）
• 对函数体e的类型检查：
  1. e可以在静态环境中使用所有声明的早期的绑定（earlier binding），所以e可以使用参数，函数绑定类型；
     即x1 : t1, x2 : t2, x3 : t3..., xn : tn和x0 : t1 * t2 * t3...tn -> t

！！深入类型检查

• 全局类型检查结果是将函数类型的结果t，赋给x0
• 函数的参数x1 : t1, x2 : t2, x3 : t3..., xn : tn，不会添加到全局静态环境，只能在函数体e内的静态环境使用
• 对函数x0调用的运算结果将会返回函数体e的运算结果，所以x0的类型即e的类型。
  类型检查器，对e进行类型检查，得到结果类型t，也是x0返回结果类型

3. 求值规则（evaluation rules）：

• 函数是一个值！
  函数在我们声明之后，就会添加静态环境中（错误！），以供我们后面调用。 （补充：将变量e0添加到动态环境）
• 函数在被调用前，不会进行任何计算

3. 函数调用

1. 语法（syntax）：

e0(e1, ...en)

• 只有一个参数时，可以省略括号

2. 类型检查（type check）：

• 对e0检查，拥有函数类型，写作：e0 : t1 * t2 * t3...tn -> t
• 然后检查参数，有：e1 : t1, ... en : tn
• 参数数量必须与函数参数数量一致，每个参数类型，也必须和函数参数类型对应。这样函数调用的结果类型才是e0的类型：t

3. 求值规则（evaluation rules）：

• 在当前的动态环境中，找到正确的函数绑定：e0
• 当前的动态环境中，计算参数e1, ..., en，得到v1, ..., vn
• 从之前的动态环境中继承并得到一个函数体内的动态环境，然后计算函数体，得到值