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
Contextual Type Theory has this I think! See Beluga: complogic.cs.mcgill.ca/beluga/
1
1
3
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
Indeed it is. Pfenning&Davies' s modal type theory lets you drop *all* of your current environment inside `box`, and CMTT which was pioneered by Nanevski et. al. (if I'm not mistaken) lets you specify which part of the environment you get to keep.
4