Questions
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
<img src="https://i.stack.imgur.com/hZhjl.png" alt="Milner Hindley">
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).
https://en.wikipedia.org/wiki/List_of_mathematical_symbols
https://en.wikipedia.org/wiki/List_of_mathematical_symbols
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...)
Answers
- 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 τ .
Source
License : cc by-sa 3.0
http://stackoverflow.com/questions/12532552/what-part-of-milner-hindley-do-you-not-understand
Related
