> "What part of
>
> x : σ ∈ Γ
> ----------
> Γ ⊢ x : σ
>
>
> Γ ⊢ e0 : τ → τ', Γ ⊢ e1 : τ
> -----------------------------
> Γ ⊢ e0 e1 : τ'
>
>
> Γ, x : τ ⊢ e : τ'
> --------------------
> Γ ⊢ λ x . e : τ → τ'
>
>
> Γ ⊢ e0 : σ, Γ, x : σ ⊢ e1 : τ
> -------------------------------
> Γ ⊢ let x = e0 in e1 : τ
>
>
> Γ ⊢ e : σ', σ' ⊑ σ
> --------------------
> Γ ⊢ e : σ
>
>
> Γ ⊢ e : σ, α ∉ free(Γ)
> -------------------------
> Γ ⊢ e : ∀ α . σ
>
> do you NOT understand?"

...In other news, I'm actually kind of impressed that this even renders 
in "plain text". Back in the day, anything that wasn't 7-bit ASCII was 
100% guaranteed to never, ever work in any software application except 
the one that created it. Unicode support has apparently come a long way! 
[With apologies to all the people who can't find a suitable font to 
render this stuff...]

I actually asked one time what all the equations above mean. [Or, more 
exactly, what language they're written in - but several responders went 
all out and exposited the whole thing.] It turns out that what it's 
actually saying is fairly trivial - it just *looks* damned complicated. 
Pretty much like most mathematics, really.

(Then again, open a book written on a foreign language like Korean, and 
it looks complicated too - even though it might just be somebody's 
shopping list or similar.)

Post a reply to this message