What part of Hindley-Milner do you not understand?

  • 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

Leave a Comment