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:

---

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

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

---

As requested: operator precedence, from highest to lowest:

• Language-specific infix and mixfix operators, such as λ x . e, ∀ α . σ, and τ → τ', let x = e0 in e1, and whitespace for function application.
• :
• ∈ and ∉
• , (left-associative)
• ⊢
• whitespace separating multiple propositions (associative)
• the horizontal bar