"Context Constrained Computing", an extended abstract submitted to TyDe by myself and . Linear types, monotonicity types, sensitivity types, information flows types, all in a unified framework! bentnib.org/context-constr
Conversation
What's your elimination rule for !_rho? ...
maybe I should just send you an email.
1
It's like pattern matching for tensor products, but instead of binding two new variables of 1-resource, bind one variable of ρ-resource. I'll try some ASCII art if you want.
1
1
Γe ⊢ e ∈ !_ρ S Γs, x :^ρ S ⊢ T ∋ s[x] Γ ≤ Γe + Γs
------------------------------------------------------
Γ ⊢ bm_T(e, {x}s[x]) ∈ T
1
2
Ah, of course! And I wouldn't be surprised if this unifies the elim rules for both necessity *and* possibility from Pfenning-Davies! Very nice.
2
This is basically Plenty o' Nuttin, but simply typed and also working. See Bob's Syntax and Semantics of Quantitative Type Theory for the comparison.
1
1
Yeah, I was curious about how 0-annotated stuff works in places like: github.com/edwinb/Blodwen
map : {0 a b : Type} -> (a -> b) -> List a -> List b
You want to say `map` is parametric over `a` and `b` (not used in the body), but you still want to use it in the types… 🤔
1
I can also kind of imagine `a` and `b` being used in the body of the function too, but just for type annotations. Of course you then want to prevent them from being passed to non-parametric functions.