haskell - “你不明白欣德利 - 米尔纳的哪一部分？”(“What part of Hindley-Milner do you not understand?”)

Question

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

(我发誓曾经有一件T恤出售，上面写着不朽的话：)

---

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.

(特别是，我经常在Haskell论文中看到这样的符号，但我不知道它的含义是什么。)

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.

(我也不熟悉这里使用的vinculum。)

(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.

(如果有人至少可以告诉我从哪里开始想要理解这个符号海洋的含义，那将会有所帮助。)

  ask by MathematicalOrchid translate from so

Answer 1

• 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 σ .

  (因此x : σ ∈ Γ意味着环境Γ包括x具有类型σ的事实。)

• ? can be read as proves or determines.

  (?可以作为证明或确定。)

  Γ ? x : σ means that the environment Γ determines that x has type σ .

  (Γ ? x : σ表示环境Γ确定x具有类型σ 。)

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

  (因此， Γ, x : τ ? e : τ'意味着环境Γ ， 以及x具有类型τ的附加的超越假设 ，证明e具有类型τ' 。)

---

As requested: operator precedence, from highest to lowest:

(根据要求：运营商优先级，从最高到最低：)

• Language-specific infix and mixfix operators, such as λ x . e

  (特定于语言的中缀和mixfix运算符，例如λx λ x . e)

  λ x . e , ? α . σ

  (λ x . e ， ? α . σ)

  ? α . σ , and τ → τ' , let x = e0 in e1 , and whitespace for function application.

  (? α . σ ，和τ → τ' ， let x = e0 in e1 ，以及用于功能应用的空白。)

• :
• ∈ and ?

  (∈和?)

• , (left-associative)

  (, （左联想）)

• ?
• whitespace separating multiple propositions (associative)

  (分隔多个命题的空格（关联）)

• the horizontal bar

  (横杠)