“你不明白Hindley-Milner的哪部分？” [英] "What part of Hindley-Milner do you not understand?"

问题描述

我发誓曾经有一件T恤出售不朽的字眼： $ b

---

你不懂吗？

---

在我的情况下，答案就是...所有这一切！

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

我当然会识别希腊字母的字母，而符号如∉（通常意味着那些东西不是集合中的一个元素）。另一方面，我从未见过⊢（维基百科声称这可能意味着分区）。我也不熟悉在这里使用vinculum。 （通常它表示一个分数，但不会出现在这里）

如果有人至少可以告诉我在哪里开始寻找理解这个海洋的符号意味着什么，这将是有益的。

em> horizo​​ntal bar 表示[above] 隐含 [below]。如果有多个表达式在[上面]中，然后一起考虑 anded ;所有[above]必须为true才能保证[below]。 / strong>

∈表示在中。 （同样∉表示不在。）

Γ是通常用于指环境或上下文;在这种情况下，可以将其视为一组类型注释，将标识符与其类型配对。因此， x：σ∈Γ意味着环境Γ包含事实 x 有类型σ。

⊢如证明或确定。 Γ⊢x：σ表示环境Γ确定 x 有类型σ。

，是在环境中包含特定的附加假设Γ。

因此，Γ，x：τ⊢e： τ'意味着环境Γ，带有额外的重载假设，即 x 类型为τ ，证明 e 的类型为τ'。

I swear there used to be a T-shirt for sale featuring the immortal words:

---

What part of

do you not understand?

---

In my case, the answer would be... all of it!

In particular, I often see notation like this in Haskell papers, but I have no clue what any of it means. I have no idea what branch of mathematics it's supposed to be.

I recognise the letters of the Greek alphabet of course, and symbols such as "∉" (which usually means that something is not an element of a set).

On the other hand, I've never seen "⊢" before (Wikipedia claims it might mean "partition"). I'm also unfamiliar with the use of the vinculum here. (Usually it denotes a fraction, but that does not appear to be the case here.)

If somebody could at least tell me where to start looking to comprehend what this sea of symbols means, that would be helpful.

解决方案

• The horizontal bar means that "[above] implies [below]".
• If there are multiple expressions in [above], then consider them anded together; all of the [above] must be true in order to guarantee the [below].
• : means has type
• ∈ means is in. (Likewise ∉ means "is not in".)
• Γ is usually used to refer to an environment or context; in this case it can be thought of as a set of type annotations, pairing an identifier with its type. Therefore x : σ ∈ Γ means that the environment Γ includes the fact that x has type σ.
• ⊢ can be read as proves or determines. Γ ⊢ x : σ means that the environment Γ determines that x has type σ.
• , is a way of including specific additional assumptions into an environment Γ.
  Therefore, Γ, x : τ ⊢ e : τ' means that environment Γ, with the additional, overriding assumption that x has type τ, proves that e has type τ'.

这篇关于“你不明白Hindley-Milner的哪部分？”的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！