Is there something—maybe in dependent-types land—for making contexts explicit in types? Say, in a lambda rule:
Γ, x:A ⊢ y : B
⇒
Γ ⊢ (λx:A. y) : A → B
The premise could be thought of as:
Γ ⊢ y : {x:A} ⊦ B
Where ‘Δ ⊦ T’ = “‘T’ with free variables ‘Δ’”. Feels coeffecty…
Conversation
I believe you are right that it feels coeffecty - the contextual modal type theory that Beluga uses is some sort of generalisation of the box modality?
1
3
Show replies