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.

## Best Solution

horizontal barmeans that "[above]implies[below]".multiple expressionsin [above], then consider themandedtogether; all of the [above] must be true in order to guarantee the [below].`:`

meanshas type`∈`

meansis in. (Likewise`∉`

means "is not in".)`Γ`

is usually used to refer to anenvironmentor 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 asprovesor determines.`Γ ⊢ x : σ`

means that the environment`Γ`

determines that`x`

has type`σ`

.`,`

is a way ofincludingspecific additional assumptions into an environment`Γ`

.Therefore,

`Γ, x : τ ⊢ e : τ'`

means that environment`Γ`

,with the additional, overriding assumption that, proves that`x`

has type`τ`

`e`

has type`τ'`

.As requested: operator precedence, from highest to lowest:

`λ x . e`

,`∀ α . σ`

, and`τ → τ'`

,`let x = e0 in e1`

, and whitespace for function application.`:`

`∈`

and`∉`

`,`

(left-associative)`⊢`