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

问题描述

现在我找不到它了，但我发誓曾经有一件T恤出售不朽的字眼：

---

你不懂吗？

---

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

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

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

我想，SO不是一个好地方解释整个Milner Hindley算法。但是如果有人能够告诉我从哪里开始寻求理解这个符号之海意味着什么，这将会有所帮助。 （我确信我不能成为唯一想知道的人...）

解决方案

• 横条表示[above] 隐含 [below]。


• 如果有 / em>在[above]中，然后将它们一起考虑 anded ;所有[above]必须为true才能保证[below]。
/ strong>

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


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


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


• ，是在环境中包含特定的附加假设Γ。
  
  因此，Γ，x：τ⊢e： τ'意味着环境Γ，带有额外的重载假设，即 x 类型为τ ，证明 e 的类型τ'。

I can't find it now, but 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.)

I imagine SO is not a good place to be explaining the entire Milner Hindley algorithm. But if somebody could at least tell me where to start looking to comprehend what this sea of symbols means, that would be helpful. (I'm sure I can't be the only person who's wondering...)

解决方案

• 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 τ'.

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