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
Ohh right! What if the term includes variables?
1
1
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`
Which is how glambda (github.com/goldfirere/gla) and Stitch (cs.brynmawr.edu/~rae/papers/20; #HaskellPDF) do it if we have (|-) = Exp
Var EZ :: a:ctx |- a
Abs (Var EZ) :: ctx |- (a -> a)
1