OCaml 的局部值、模式与子模式关系

前几期视频中，我们先看了局部参数，接着看了局部变量和返回值。这次我想暂时离开函数编写，从理论层面理解局部和全局是如何相互作用的。局部和全局都称为模式。

模式有点像类型，虽然两者存在区别。每个 OCaml 表达式都有类型：5 的类型是 int，而更大的表达式可能是 string list option 类型。每个变量也有类型，因为它代表一个表达式，表达式在存入变量之前会先求值。同样，每个表达式和变量也都有模式。

例如，在 `let local_ x = "hello"` 中，标注强制 x 处于局部模式，表达式 `"hello"` 也是局部的。这段代码可以编译。做实验时，我可以关掉未使用变量的警告。

如果我引入 y，并没有相应的标注可以直接写在这个变量上，表示我希望它是全局的。不过，我可以定义 `mark_global : 'a -> unit`，让它忽略实参。它的参数没有标为局部，因此调用 `mark_global y` 会通过推断强制 y 为全局模式。

如果接着写 `let y = x`，并将 y 传给 `mark_global`，编译器会报告该值逃出了它的区域。y 的用法要求全局值，但声明为局部的 x 流入了 y。局部值不能逃逸；如果允许它流入全局值，就会给它一条间接逃逸的途径。

实际程序碰巧是安全的：`mark_global` 只是忽略了实参。但它的类型并没有保证它不会把实参存到别处。编译器依赖函数的类型，因此即便这个绑定本身不在区域末尾，它也必须拒绝该调用。

现在假设 y 是全局的，我写下 `let local_ z = y`。这段代码可以编译。即使 `mark_global y` 的调用位于程序较靠后的位置，它仍能决定 y 的模式，就像远处的用法可以影响类型推断一样。全局标注在这个演示中会很方便，尽管我们通常不需要它。

为什么全局的 y 可以流入局部的 z？全局是局部的子模式，写作 `global < local`。这类似于将子类型赋给超类型：全局表达式可以用于局部上下文。局部模式表示值不会逃逸；在局部上下文中使用全局值，表示这次使用不会让它逃逸，这是安全的。

反过来就不行了。可以把全局模式理解为拥有逃逸的能力。在局部上下文中使用全局值时，我们可以主动放弃这种能力；但把局部值变成全局值，就相当于凭空创造它原本没有的能力。我觉得这种顺序有点违反直觉，因为全局听起来比局部更大，但我们却要写成全局小于局部。

模式也会与函数相互作用。我可以定义 `mark_local : local_ 'a -> unit`，同样让实现忽略实参。无论用局部的 x、全局的 y 还是局部的 z 调用它，都可以正常工作。传入 y 没问题，因为全局值可以用于局部上下文。

参数上的局部标注表示这个参数不会逃逸。这是函数实现作出的承诺，而不是要求调用方提供一开始就声明为局部的值。调用方既可以传入局部值，也可以传入全局值。

这个承诺会限制函数实现：例如，将参数存入引用会因逃逸而遭到拒绝。即使我立刻忽略这个引用，逃逸分析也不够聪明，无法接受这种情况。因此，只要可能，把参数标为局部或许都有意义；我会在之后的视频中讨论局部性推断。

这与函数上的普通类型标注有所不同：普通类型标注既描述实现，也规定使用处的要求。由于子模式关系，局部参数并没有对调用方提供的值原本是全局还是局部施加实质限制。我的 `mark_local` 示例本质上就是 `ignore`。

模式与函数类型之间还有一个细节。箭头两侧都可以是局部或全局模式，因此有四种箭头类型：`string -> string`、`local_ string -> string`、`string -> local_ string` 和 `local_ string -> local_ string`。局部输入、全局输出的情况在实现时需要更小心。

这是四种不同的类型，它们之间没有子类型关系，尽管 OCaml 在某些情况下可以进行转换。为了展示区别，我把一个函数放入引用，并声明引用的内容类型为 `string -> string`。引用匹配的函数没有问题，但引用其他函数类型会产生错误。引用阻止了编译器可能执行的转换。

这里的关键是：模式描述每个表达式和变量；子模式关系允许任何全局值视为局部值，反过来则不行。我们可以在函数箭头上标注输入和输出的模式。

还要记住，`local_ string` 本身并不是一个独立类型。`local_` 标注实际上描述的是箭头。在理论记法中，我们也许会用四种不同的箭头符号；具体语法则把 `local_` 放在输入或输出旁边。我会在之后的视频中再讨论这些话题。