haskell - Hindley-Milner 的哪一部分是你不明白的？

Question

我发誓曾经有一件T恤出售，上面写着不朽的文字:

<小时/>

哪一部分

你不明白吗？

<小时/>

就我而言，答案是......全部!

特别是，我经常在 Haskell 论文中看到这样的符号，但我不知道它的含义。我不知道它应该是数学的哪个分支。

我当然认识希腊字母表中的字母和诸如“∉”之类的符号(这通常意味着某物不是集合的元素)。

另一方面，我以前从未见过“⊢”( Wikipedia claims it might mean "partition" )。我也不熟悉这里 vinculum 的使用。 (通常，它表示分数，但这里的情况似乎并非如此。)

如果有人至少能告诉我从哪里开始理解这堆符号的含义，那将会很有帮助。

Answer 1

• 水平条表示“[上方]暗示[下方]”。
• 如果[上面]中有多个表达式，则将它们并考虑在一起；为了保证[下面]，所有[上面]都必须是真实的。
• : 表示有类型
• ε 表示在。 (同样，∉ 表示“不在”。)
• Γ 通常用于指代环境或上下文；在这种情况下，它可以被认为是一组类型注释，将标识符与其类型配对。因此，x : σ ∈ Γ 意味着环境 Γ 包含 x 具有类型 σ 的事实。<
• ⊢ 可以理解为证明或确定。 Γ ⊢ x : σ 表示环境 Γ 确定 x 的类型为 σ。
• , 是一种将特定的附加假设包含到环境Г中的方法。
  因此，Г, x : τ ⊢ e : τ' 表示环境 Г, 以及附加的、压倒一切的假设，即 x 具有类型 τ，证明 e 具有类型 τ'。

<小时/>

根据要求:运算符优先级，从最高到最低:

• 特定于语言的中缀和混合运算符，例如 λ x 。 e, ∀ α 。 σ，以及 τ → τ'，let x = e0 in e1，以及用于函数应用的空白。
• :
• ε 和 ∉
• ,(左关联)
• ⊢
• 空格分隔多个命题(关联)
• 单杠