PL type theory notation is wrong.
It's not (Γ ⊢ e : A).
It's (e : Γ ⊢ A).
(hills I contemplate from afar but am unwilling to die on, #1)
7
4
38
Conversation
Curious to hear your reasoning on this!
1
2
the type of "e" isn't "A", it's "Γ ⊢ A". the context Γ is as important as the type A, and the two belong together.
for example, it matches more nicely with categorical semantics:
e : Γ ⊢ A, so
⟦e⟧ : ⟦Γ⟧ → ⟦A⟧
1
5
It kind of reminds me of 'Contextual typing' that was brought up in the POPL keynote that I watched last night.
1
1
I guess I've always considered that both the term and the type are well formed under the context `Γ`. So you can have `Γ ⊢ A type` _and_ `Γ ⊢ e : A`
1
1
Show replies