So You Still Don't Understand Hindley-Milner?

[wangwangwar]

http://akgupta.ca/blog/2013/05/14/so-you-still-dont-understand-hindley-milner/ Part1

博主是为了回答 StackOverflow 上的一个问题 ref1 写了这个系列，共 3 个部分。 翻译了 99 %。

介绍了 HM 算法的目的，什么是形式化（formalize），为了形式化（formalization） 需要准备哪些积木（Building blocks）。

1. HM 算法的目的

从功能上来说，Hindley-Milner (或 Damas-Milner) 是一个算法，根据使用（情况）来推导值的类型。算法从字面上形式化了一种直觉，即可以根据类型所提供的功能来推导其类型。

2. 什么是形式化

我们需要一个元语言 (meta-language)，用来描述任意编程语言中的表达式 (expression)。这个元语言必须满足：

• 是抽象 (abstract) 和通用的 (generic) ，因此允许我们在推理类型推断声明 (statements of type inference) 时只需要单纯考虑类型的形式 (form)，而不用关注其内容。
• 为表达式给出精确无歧义的，但仍直观的 (precise, unambiguous, yet intuitive) 定义。
• 以少数的无争议的原始的概念 (uncontroversial primitive concepts) 为单位，进行定义。
• 类似地，为类型，表达式有类型的观点，和可以推断一个给定的表达式有给定的类型的观点，都给出定义。
• 适合于简洁的符号表示，比起描述 “一个表达式由应用 (apply) 第一个表达式到第二个表达式构成，类型为一个函数，这个函数输入值为字符串，返回值为一个当前上下文下我们不关心的类型”，我们可以简单地表示为 e1 (e2): String -> t。
• 容易翻译成计算机可以理解和实现的形式，最终可以自动推断类型。

3. 需要准备哪些积木

• 一种形式化的方法来表示表达式。需要满足上面列举的标准。因此我们采用 λ演算 (Lambda Calculus)。
• 一种形式化的方法来表示类型，及一同表示表达式和类型。毕竟， HM 算法的目的是推断 “表达式 e 的类型为 t”这种形式的声明。
• 一个形式化的规则集，用于从一些表达式类型声明派生 (derive) 出其它声明。规则基本是这样的形状：“如果可以论证一个表达式为X类型，另一个表达式为Y类型，因此第三个表达式为Z类型”。
• 一个算法，可以聪明地使用推断规则，从一个起点开始，推断出一个想要的结论声明：“我感兴趣的表达式 e 为类型 t”。

---

[wangwangwar]

http://akgupta.ca/blog/2013/06/07/so-you-still-dont-understand-hindley-milner-part-2/ Part2

这部分里，我们讲形式化积木的第一块和第二块，即一种形式化的方法来表示表达式，和一种形式化的方法来表示类型，及一同表示表达式和类型。

1. 一种形式化的方法来表示表达式

我们会给出表达式是什么的递归定义。换种方式来说，我们会声明表达式最基本的形式是什么，如何用已知的表达式创造新的，更复杂的表达式，以及以何种方式创造出来的表达式是合法的 (valid)。

• 变量 (variables) 是合法的表达式。
• 如果 e 是表达式， x 是变量，那么 λx.e 是表达式。这样有助于理解：假设 e 是 (但不是必要的) 一个包含 x 的更复杂的表达式，如 e^2 + 2，那么 λx.e 是一个接受输入 x，用 x 的值对表达式 e 求值然后返回结果的匿名函数。像是 function (x) { return x^2 + 2; }。
• 如果 f 和 e 是合法的表达式，那么 f(e) 是合法的表达式。这称为应用 (Application)。
• 如果 x 是变量，e1 和 e0 是合法的表达式，那么把 e1 中每一处 x 都替换为 e0后，仍是合法的表达式。比如，如果 e1 是表达式 x^2 + 2，e0 是表达式 y/3，那么如果让 e1 中 x = e0，我们得到表达式 (y/3)^2 + 2。 (最后一条是冗余的，并不是 λ 演算中表达式定义的官方构成。把 e1 中每一处 x 都替换为 e0 相当于应用抽象 λx.e1 到 e0。这是为了支持所谓的受限多态 (let-polymorphism)。)

除此之外都是非法的表达式。

旁白：如果你密切关注的话会想，如何 (从以上表达式的定义中) 创造一个有用的表达式？我如何得到 x^2 + 2，或者说，实际上最重要的 2？0 呢？定义中没有任何关于 明显 生成表达式 0 的规则。解决办法是，在 λ 演算中创造和 0, 1, ..., +, *, -, / 的表现一样的表达式。换句话说，我们必须把数字，数值运算，字符串等都编码成 λ 语法。这篇博客 ref1 很好的介绍了如何用 λ 演算编码数字和数值运算。这是 λ 演算一个很好的特性：我们有很简单的语法用来递归定义 4 种简单的条文 (clause)，并且允许我们用 4 个主要步骤归纳 (inductively) 证明很多东西。而语言本身的表达力足以捕捉数字，字符串和所有我们关心的类型和运算。

一种形式化的方法来表示类型

e 是任意表达式，即，e 是我们元语言中的变量，代表我们基本语言 (base language) 中的任何表达式。比如：

x
Math.pow(x,2)
[1,2].forEach ( function(x) { print(x); } )

如果 t 是任意类型，我们可以表达 “e 为类型 t” 为

e : t

像 e 一样， t 是我们元语言中的变量，可以代表基本语言中的任何类型，比如 Int, String 等。就像 e 一样， t 不必非得代表一个类型。

可以形式化地定义什么算作类型，像前面表达式那样。但是这种抽象相当的曲折，所以我们就暂且不表。我就指出两个关键的点：

• 如果 s 和 t 是类型，那么 t -> s 也是，类型为以 t 为输入 s 为输出的函数。
• 如果 r 是由其他类型组成的类型 (比如 t -> s 由 t 和 s 组成，而 t 和 s 也可能由其他类型构成)，而 α 是类型的变量，那么 ∀α.r 是类型。举例：

function (x) { return x; }

这个函数的类型可以为 String -> String，但也可以为 Int -> Int。事实上，对于任意类型 t，函数的类型为 t -> t。我们说它的类型为 ∀t.t→t。每一个如 String -> String, t -> t 的类型，都是 单型 (monotypes)，∀t.t→t 为 多型 (polytype)。上面的恒等函数 (identity function) 的类型为抽象的多型 ∀t.t→t，在实践中，意味着对于每一个具体的类型 t，它都有类型 t -> t。如果对以上都充分理解，我们可以把恒等函数简洁地表示为：

λx.x:∀α.α→α

2. 对类型的声明所作的形式化声明 (Formalizing statements about statements about types)

现在我们想形式化一系列规则，根据这些规则我们可以由表达式的一些知识和它们的类型推导出更多表达式的类型。还记得命题演算 (propositional calculus) 是如何形式化 Modus Ponens 的？我们将要做类似的事情。举例，我们想要把以下的推理形式化：

假设我已经能够推导出变量 duck 的类型为 Animal。 假设进一步我已经推导出 speak 是一个方法，类型为 Animal -> String。 那么我能够推导出 speak(duck) 的类型为 String。 且任何这种形式的推理都是合法的类型推导。

我们将其形式化为：

Γ⊢e0:τ→τ′   Γ⊢e1:τ
−−−−−−−−−−−−−−−−−−−−−
Γ⊢e0(e1):τ′

这个规则称为 [App] (取自 application)。我们将在下一篇讨论这个以及剩下的规则。现在我们来理解上面见到的符号：

• Γ 代表我们已知的或者假设的声明的集合。更普遍来说，Γ代表 (关于表达式和其类型的) 声明的集合。当然，字母 Γ 没有什么特殊的，只是声明的集合通常用大写希腊字母来表示。
• ⊢ (turnstile) 表示可以被推导的东西。比如 Γ⊢x:t 是说，如果我们以 Γ 中的声明为假设 (assumptions) / 公理 (axioms) / 当前知识 (current knowledge)，可以推导出 x 的类型为 t。
• ∈ (epsilon) 表示成员关系 (membership)。 x:t∈Γ 是说声明 x:t 是 Γ 的成员。
• 水平长线表示，如果这根线上面的内容作为论据 (argument) 的前提 (premises)，那么结论就是这根线以下的内容。它让我们能够表达类似 “如果我们可以推导出xxx，那么我们可以推导出yyy” 的东西。举例：

Γ⊢y:σ
−−−−−−−
Γ⊢x:τ

如果我们可以从 Γ 推导出 y 的类型为 σ，那么我们可以从 Γ 推导出 x 的类型为 τ。

---

[wangwangwar]

http://akgupta.ca/blog/2013/06/07/so-you-still-dont-understand-hindley-milner-part-3/ Part3

这篇文章里，我们准备讲解类型推导的推断声明规则 (the rules for deducing statements about type inference)。

类型推导的推断声明规则

[Var]

x:σ∈Γ
−−−−−−−
Γ⊢x:σ

翻译为：如果 “x 的类型为 σ” 这个声明属于声明集合 Γ，那么从 Γ 可以推导出 x 的类型为 σ。在这里，x 是变量 (这条推导规则的名字就是这么来的)。是的，这听起来再明显不过。[Var] 以简洁而神秘的方式，并不是因为它包含一些深刻的，困难的事实。它的简洁是为了让机器理解并且让类型推导自动化。

[App]

Γ⊢e0:τ→τ′   Γ⊢e1:τ
−−−−−−−−−−−−−−−−−−−−−
Γ⊢e0(e1):τ′

翻译为：如果可以推导出 e0 是一个类型为 τ → τ′ 的表达式 (比如根据 Γ，e0 是一个接受类型为 τ 的输入，返回类型为 τ′ 的输出的匿名函数)，而且可以推导出 e1 的类型为 τ，那么可以推断，可以推导出应用 e0 到 e1 的表达式 e0(e1) 的类型为 τ′。直观地说，如果可以推导出一个函数的输入和输出的类型，而且可以推导出某些表达式的类型和函数输入的类型一样，那么当我们应用函数到这些表达式，可以推导出结果表达式的类型和函数输出的类型一样。毫不奇怪。

[Abs]

Γ,x:τ⊢e:τ′  
−−−−−−−−−−−−−−
Γ⊢λx.e:τ→τ′

翻译为：如果允许我们假设 x 的类型为 τ 我们就能推导出 e 的类型为 τ′，那么可以推断，关于变量 x 的抽象 (abstraction) /匿名 (anonymization) e，即 λx.e，的类型为 τ → τ′。比如，我们知道如果 x 的类型为 String，那么表达式 x[0] 的类型就为 Char。现在 [Abs] 允许我们推断 function (x) { return x[0]; } 的类型为 String → Char。

另外，我之前提到过 多型 (polytypes)。为了帮助理解，让我们在这个例子中回顾一下。注意到上面的函数的类型也可以是 Array[Int] → Int。事实上，对于任意类型 t，这个函数的类型都为 Array[t] → t。所以它具有多个不同的类型，String → Char 只是其中一个。每一个形状为 Array[t] → t 的类型都是 单型 (monotype)。我们说这个函数的类型为多型 ∀t(Array[t] → t)，意思是它的类型可以是所有这种单型。读作 “对于所有 t，类型 Array[t] → t" ("for all t, the type Array[t] → t")，并且我们把它当作整体，看成一个单独的而更抽象的类型。所以注意到，当我们推导出某些表达式的类型时，并不意味着这些表达式的类型只能是这种类型。一个表达式可以是多种类型，其中某些类型可以是更抽象类型的 特化 (specializations)。那种最简单的类型就是单型，如：Int，String，String → Char。但我们可以有更抽象/通用的类型叫多型。

[Let]

Γ⊢e0:σ    Γ,x:σ⊢e1:τ
−−−−−−−−−−−−−−−−−−−−−
Γ⊢let x=e0 in e1:τ

容易推理：

如果可以推导出 `e0` 的类型为 `σ`，
并且假设 `x` 的类型为 `σ` 的前提下，那么可以推导出 `e1` 的类型为 `t`，
那么我们推断，让 `x = e0` 替换到 `e1` 中的结果的类型为 `t`。

刚才的 4 条规则把我们的直觉形式化了，即当我们有变量，创建匿名函数，应用函数，替换表达式到另外的表达式时，我们可以做怎样的类型推导。我们作为程序员可以凭直觉做出那样的类型推导。这里想说的是，我们大脑中的活动不全都是很神秘的，仍然可以被形式化地描述出来。值得注意的是，这 4 条规则分别对应 λ 演算中定义什么是合法的表达式的 4 条规则。这并不是巧合。

[Inst]

Γ⊢e:σ′    σ′⊑σ
−−−−−−−−−−−−−−
Γ⊢e:σ

这是关于 实例化 (instantiation) 的。你可以认为单型 Array[Int] → Int 是多型 ∀t.Array[t] → t 的一个实例。换句话说，这是 “特化” (specialization)：Array[Int] → Int 比 ∀t.Array[t] → t 更特化 (specialized/specific)。倒过来说，我们用 ⊑ 表示类型 “更不那么特化” 的关系。所以

∀t.Array[t] → t  ⊑  Array[t] → t

所以 [Inst] 的直接翻译是：如果可以推导出 e 的类型为 σ′，而 σ 是 σ′ 的特化/实例，那么我们推断，可以推导出 e 的类型可以为 σ。你可以认为 σ 和 σ′ 分别是 Array[t] → t 和 ∀t.Array[t] → t。

[Gen]

Γ⊢e:σ    α∉free(Γ)
−−−−−−−−−−−−−−−−−−
Γ⊢e:∀α.σ

这是最难理解的部分。这个只有在用这些规则进行类型推导的上下文中才会有意义。它并没有非常具体的类比，因为它非常依赖 可变类型 (variable type) 的概念。而这个概念在编程语言中是没有的，但是在元语言中讨论任意实际编程语言中的类型时，却是不可或缺的。可以在这个 “例子” 中管窥一二：

假设有变量 x 和 y，暂时假设它们的类型都为 α，α 是代表类型的变量。然后遇到了一个表达式，这个表达式在这个上下文中 (即假设变量 x 和 y 的类型都为 α 的上下文) 可以被推导出类型为 α→α。问题来了，这个函数的类型可以为 ∀α.α → α 吗？也就是说，这个函数是通用地映射对象到同样类型的对象，还是说，只会发生在假设变量 x 和 y 的类型都为 α 的情况下？

因为 α 是一个可变类型，也就是说，它代表任意类型，我们可能会这样认为，因为已经推导出 e 的类型为 α → α，所以它的类型为 ∀α.α → α。但是在充分了解 e 和 x，y 有怎样的联系之前，我们不能这样肯定地做出这种 泛化 (generalization)。特别是，如果表达式的类型为 α → α 这个推导是和之前关于 α 的假设紧密联系的，那么我们不能得出结论说它的类型为多型 ∀α.α → α。

这里是翻译：

如果在我们当前上下文 (current context)/知识集 (set of knowledge)/假设 (assumptions) 中没有 “自由地 (freely)” 提及可变类型 α，而我们可以推导出表达式 e 的类型为 σ，那么可以推导出，无论 α 最终变成什么样，e 的类型都为 σ。更专业地来说，e 的类型为多型 ∀α.σ。

好了，但是什么是 “自由地提及 (freely mentioned)” 呢？在多型 ∀α.α → α 中，α 并没有被 “真正地” 提及。那个类型和这个类型是一模一样的：∀β.β → β。都是表示，表达式的类型为从任意类型到它本身的函数 (An expression with either type is just that of a function that sends any type to itself)。另一方面，x:α “真正地” 提及了 α。

x:α
y:β

和

x:α
y:α

并不一样。后者是说 x 和 y 绝对是相同的类型 (虽然类型还未确定)。前者并没有告诉我们 x 和 y 有什么联系。区别在于，当 α 在 ∀ 的范围内被提及，比如 ∀α.α → α 的情况，α 只是一个 名义变量 (dummy)，可以被替换为任意其他的类型变量而不管上下文的其他部分。所以我们可以把声明 “α 没有在上下文 Γ 中被自由地提及” 解释为，“α 要么从来没有被提及，要么以名义变量的身份被提及，可以被替换为完全不同的东西，而不会改变上下文中的假设/知识的语义 (semantics)“。

[MarisaKirisame]

👍

[wangwangwar]

帅气可爱魔理沙！

[MarisaKirisame]

喵喵喵？ 其实我推荐看SPJ的the implementation of functional programming language

[MarisaKirisame]

里面也有讲algorithm W，我看了就懂了 不过整本书都很好

[wangwangwar]

谢谢！我去看。