For me it’s probably speech therapy and everything pertaining to that. I’m yet to encounter someone on here who is one apart from me (in training).
What about you?
For me it’s probably speech therapy and everything pertaining to that. I’m yet to encounter someone on here who is one apart from me (in training).
What about you?
I think “graded” in the name is there in contrast to “quantitative” type theory, which doesn’t have modalities/quantities at the type-level.
The “modal” is borrowed from modal logic. If you pick the correct semiring, you can recover linearity and affine-ity and the other substructural logic pieces.
The quantitative semiring I’ve been working with is
0, 1, ?, n, +, *, which I think will let me use static analysis to do very precise non-strictness and precise/early resource tracking/release. (But, my progress is so slow, that if this were an academic project, I don’t think I’d be getting any more grant funding.)I see, having modalities on type level makes sense as a grading, alike the grading of e.g. polynomial rings.
So you are going along the line of linearity and affine-ity? What kind of stuff are you working out?