“米尔纳 – 辛德雷的哪一部分你不明白？

我现在找不到，但我发誓曾经是一件以不朽名言为特色的T恤衫：

---

什么部分

你不明白吗？

---

就我而言，答案就是……所有这一切！

特别是，我经常在Haskell的论文中看到这样的符号，但是我不知道它的意思。 我不知道它应该是什么math分支。

我当然认识到希腊字母的字母，象“∉”这样的符号（通常意味着某些东西不是集合中的一个元素）。

另一方面，我从来没有见过“⊢”（ 维基百科声称它可能意味着“分区” ）。 我也不熟悉在这里使用的vinculum。 （通常它表示一个分数，但在这里似乎不是这种情况。）

我想，SO不是解释整个Milner Hindleyalgorithm的好地方。 但是如果至less有人能告诉我从哪里开始去理解这个符号之海意味着什么，这将是有帮助的。 （我相信我不能是唯一想知道的人…）

Answer 1

• 横条意味着“[above] 意味着 [below]”。
• 如果[上面]有多个expression式 ，那就把它们考虑在一起; 所有的[上述]必须是真实的，以保证[下]。
• :意味着有types
• ∈意味着在 。 （同样∉表示“不在”）。
• Γ通常用于指代环境或上下文; 在这种情况下，可以将其视为一组types注释，将标识符与其types配对。 因此x : σ ∈ Γ表示环境Γ包括x具有typesσ的事实。
• ⊢可以看作是certificate或确定的。 Γ ⊢ x : σ意味着环境Γ确定x具有typesσ 。
• 是一种将具体的附加假设包含在环境中的方法。
  因此， Γ, x : τ ⊢ e : τ'意味着环境Γ ， 附加的重写假设x具有typesτ ，certificatee具有typesτ' 。

Answer 2

这个语法虽然看起来很复杂，但其实很简单。 基本思想来自逻辑：整个expression式是一个含义，上半部分是假设，下半部分是结果。 也就是说，如果您知道顶部expression式是真实的，那么您可以得出结论，底部expression式也是真实的。

符号

另外要记住的是，一些字母具有传统意义， 特别是，Γ代表你所处的“背景” – 也就是说，你所看到的其他事物的types是什么。 所以像Γ ⊢ ...这样的东西就意味着“expression式...当你知道Γ中每个expression式的types。

这个符号本质上意味着你可以certificate一些东西。 所以Γ ⊢ ...是一个声明，说：“我可以certificate...在上下文Γ 。这些陈述也称为types判断。

另外要记住的是：在math中，就像ML和Scala一样， x : σ意味着x具有typesσ 。 你可以像Haskell的x :: σ一样阅读它。

每条规则的含义

因此，知道这一点，第一个expression式变得容易理解：如果我们知道x : σ ∈ Γ （即x在某些情况下Γ具有某种typesσ ），那么我们知道Γ ⊢ x : σ （也就是说，在Γ ， xtypes为σ ）。 所以真的，这不是告诉你任何超级有趣的东西; 它只是告诉你如何使用你的上下文。

其他规则也很简单。 例如，拿[App] 。 这个规则有两个条件： e₀是从某种typesτ到某种typesτ'的函数， e₁是typesτ'一个值。 现在你知道把e₁ e₀应用于e₁将会得到什么types！ 希望这不是一个惊喜:)。

下一个规则有更多新的语法。 特别地， Γ, x : τ只意味着由Γ和判断x : τ组成的上下文。 所以，如果我们知道variablesx有一个τtypes，并且expression式e有一个typesτ' ，我们也知道函数的types，它带有x并返回e 。 这只是告诉我们该怎么做，如果我们已经找出了一个函数的types和它返回的types，所以它也不应该是令人惊讶的。

下一个只是告诉你如何处理let语句。 如果知道只要x有一个typesσ ，那么expression式e₁就有一个typesτ ，那么一个局部地将x与σtypes值相联系的letexpression式将使得e₁的types为τ 。 真的，这只是告诉你一个let语句实际上可以让你用一个新的绑定扩展上下文 – 这正是let做的！

[Inst]规则处理子分类。 它说，如果你有一个typesσ'的值，它是σ'一个子types（ ⊑表示一个偏序关系），那么这个expression式也是typesσ 。

最后的规则涉及泛化types。 快速抛开：一个自由variables是一个variables，不是由let语句或lambdaexpression式引入的; 这个expression式现在取决于上下文中自由variables的值。规则是说，如果在你的上下文中有任何variablesα 不是 “自由”的，那么可以肯定地说，知道e : σ将具有该types的任何 α值。

如何使用规则

所以，现在你明白了这些符号，你对这些规则做了什么？ 那么，你可以使用这些规则来找出各种值的types。 要做到这一点，看看你的expression式（比如fxy ），并find一条与你的语句相符的结论（底部）。 让我们称之为你试图find你的“目标”的东西。 在这种情况下，你会看e₀ e₁结尾的规则。 当你发现这一点时，你现在必须find规则来certificate这条规则之上的一切。 这些东西通常对应于子expression式的types，所以你基本上是recursionexpression式的一部分。 你直到你完成你的certificate树，这给你一个你的expression式types的certificate。

因此，所有这些规则都是精确地指定的 – 而且在通常的math迂腐细节中：P – 如何计算expression式的types。

现在，如果你曾经使用过Prolog，那么这应该听起来很熟悉 – 你基本上是像人类的Prolog解释器那样计算certificate树。 Prolog被称为“逻辑编程”是有原因的！ 这也是重要的，因为我介绍HM推理algorithm的第一种方法是在Prolog中实现它。 这实际上是令人惊讶的简单，使得事情变得清晰。 你当然应该尝试一下。

注意：我可能在这个解释中犯了一些错误，如果有人指出，我会很喜欢它。 实际上我会在几个礼拜内在课堂上讲这个，所以我会更有信心的：P。

Answer 3

如果有人能够告诉我从哪里开始去了解这个符号之海所蕴涵的意义

参见“ 编程语言的实践基础 ”，第2章和第3章，通过判断和推导逻辑的方式。 整本书现在在亚马逊上。

第2章

归纳定义

归纳定义是编程语言研究中不可或缺的工具。 在这一章中，我们将开发归纳定义的基本框架，并举例说明它们的用法。 归纳定义由一系列用于推导各种forms的判断或断言的规则组成。 判断是关于指定sorting的一个或多个语法对象的陈述。 这些规则为判断的有效性规定了必要和充分的条件，从而充分确定了其含义。

2.1判决

我们从判断的概念开始，或者从句法对象的断言开始 。 我们将利用多种forms的判断，包括这样的例子：

• n nat – n是一个自然数
• n = n1 + n2 – n是n1和n2之和
• τ types – τ是一种types
• e ： τ – expression式e的types为τ
• e⇓v – expression式e具有值v

一个判断表明，一个或多个句法对象有一个属性或者彼此有某种关系。 财产或者关系本身被称为判断forms ，并且判断一个或者多个物体在该关系中具有该财产或者站在这个关系上的判断被认为是该判断forms的一个实例 。 判断forms也称为谓词 ，构成实例的对象是其主语 。 我们为判断J写了一个 J。 当强调判断的主题并不重要时，（文中断）

Answer 4

符号来源于自然演绎 。

⊢符号被称为旋转门 。

这6条规则非常简单。

Var规则是相当平凡的规则 – 它说，如果标识符的types已经存在于你的types环境中，那么推断出你只是从环境中取出types。

App规则说，如果你有两个标识符e0和e1并且可以推断它们的types，那么你可以推断应用程序的typese0 e1 。 如果你知道e0 :: t0 -> t1和e1 :: t0 （同样的t0！），那么这个规则是这样读的，那么应用程序的types是好的，types是t1 。

Abs和Let是规则来推断lambda抽象和let-in的types。

Inst规则说，你可以用一个较不Inst的typesreplace。

Answer 5

我想，SO不是解释整个Milner Hindleyalgorithm的好地方。

如果你正在寻找对algorithm的一个很好的解释，那么迄今为止我所发现的最好的是在Shriram Krishnamurthi的编程语言：应用和解释 （CC许可！）的第30章。 这是一个很好的理由，这是一个很好的解释：例子！

Answer 6

有两种方法可以考虑e：σ。 一个是“expression式e具有typesσ”，另一个是“expression式e和typesσ的有序对”。

查看Γ作为关于expression式types的知识，实现为一组expression式和types对，e：σ。

旋转门⊢意味着从左边的知识中，我们可以推断出右边的内容。

因此可以读取第一条规则[Var]：
如果我们的知识Γ包含对e：σ，那么我们可以从Γ推导出e有σ型。

第二个规则[App]可以被读取：
如果我们从Γ可以推出e_0的typesτ→τ'，并且我们从Γ可以推出e_1的typesτ，那么我们从Γ可以推论出e_0 e_1的typesτ'。

通常写Γ，e：σ而不是Γ∪{e：σ}。

第三条规则[Abs]可以这样理解：
如果我们从Γ扩展到x：τ可以推出e有τ'types，那么我们从Γ可以推导出λx.e的typesτ→τ'。

第四条规则[Let]留作练习。 🙂

第五条规则[Inst]可以阅读：
如果我们从Γ可以推出e有typesσ'，而σ'是σ的子types，那么我们从Γ可以推论出e有typesσ。

第六和最后一个规则[Gen]可以阅读：
如果我们从Γ可以推出e有σ型，并且α不是Γ中任何types的自由型variables，那么我们从Γ可以推出e有types∀ασ。

Answer 7

我如何理解Hindley-Milner规则？

Hindley-Milner是一组连续演算forms的规则，说你可以从程序的构造中推导出（最一般的）types的程序，而不需要明确的types声明。

符号和符号

首先，我们来解释这些符号

• 𝑥是一个标识符（非正式的，一个variables名称）。
• ： means是一种（非正式的，实例或“is-a”）。
• σ （西格玛）是一个variables或函数的expression式。
• ∈意味着是一个元素
• Γ（伽玛）是一个环境。
• ⊦ （断言符号）意味着断言 （或certificate，但内容上“断言”更好。）
• Γ⊦⊦ ： σ因此被读取Γ声明𝑥， σ
• 𝑒是typesσ的实际实例（元素）。
• τ （tau）是一种types：基本的，可变的（ α ），函数τ→τ'或乘积τ×τ'
• τ→τ'是τ和τ'是types的函数types。
• λ𝑥.𝑒表示λ （lambda）是一个匿名函数，它接受一个参数𝑥并返回一个expression式𝑒 。
• 在 𝑒1中 𝑥 =𝑒0意味着expression式𝑒1 ，在出现where的地方代替𝑒0 。
• ⊑表示先验元素是后一元素的子types（非正式 – 子类别）。
• α是一个typesvariables。
• ∀α.σ是一个types，∀（全部）参数variablesα ，返回σexpression式
• ∉free （Γ）表示不是在外部上下文中定义的Γ的自由typesvariables的元素。 （绑定variables是可替代的。）

上面的一切都是前提，下面的一切都是结论（ Per Martin-Löf ）

这里接下来是逻辑陈述的英文解释，然后是解释。

variables

给定𝑥是σ（sigma）的一种，Γ（Gamma）的一个元素，
结论 Γ断言𝑥是σ。

这基本上是一个重言式 – 标识符名称是一个variables或函数。

function应用

给定Γ断言𝑒0是一个泛函型，Γ断言𝑒1是τ
结论 Γ断言应用函数𝑒0到𝑒1是一个typesτ'

这意味着如果我们知道一个函数返回一个types，并将其应用于一个参数，那么结果就是我们知道返回的types的一个实例。

函数抽象

给定τ的Γ和asse断言𝑒是一个types，τ'
结论 Γ断言一个匿名函数，返回expression式的λ，是τ→τ'的types。

这意味着如果我们知道τ是τtypes的，并且因此expression式τ'是τ'types，那么返回expression式的函数是τ→τ'的types。

让variables声明

给定Γ表示typesσ的σ0，以及typesσ的Γ和，，表示τ的typesτ1
结论 Γ断言in τtypes的𝑒1 in let 𝑥=𝑒0

这意味着，如果我们有一个expression式σ（σ是一个variables或函数），某个名称𝑥也是一个σ，并且τ是一个expression式𝑒1，那么我们可以用𝑒0代替𝑥 𝑒1。

实例化

给定Γ表示σ'的types，而σ'是σ的一个子types
结论 Γ断言𝑒是σ型的

这就是说，如果一个实例的types是另一个types的子types，那么它也是这个超types的一个实例。

这允许我们使用更一般意义上的types实例化，即expression式可以返回更具体的types。

概括

给定Γ断言𝑒是σ 并且 α不是Γ的自由variables的元素，
结束 Γ断言type，input返回σexpression式的所有参数expression式α

这意味着我们可以推广一个程序来接受所有types的参数，这些参数尚未被绑定在包含范围内（variables不是非本地的）。 这些绑定variables是可替代的。

结论

这些规则相结合使我们能够certificate断言程序的最普通types，而不需要types注释，允许将各种types正确接受为input（参数多态）。