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?
https://gitlab.com/bss03/grtt is my published code. But, I have far more intuitions that I need to write code for than finished code.
While evaluating something well-typed under a context, the heap: does not need to contain a value for a binder with modality 0, must contain a single, strict value for a binder with a modality 1, must contain a single, lazy closure for a binder with a modality of ?, must contain multiple references to a shared, strict value for a binder with a modality n, must contain at least a single reference to a strict value for a binder with a modality of +, must contain at least a single reference to a lazy closure for a binder with a modality of *. Since the typing rules propagate the modalities to subterms precisely, we should be able to identify the exact point a closure must be forced to a value (or dropped) before runtime. That’s in addition to being able to compile linear functions to heap updates, eliminating at least some allocations.
There’s some similarities with both the exact-use-count and relevant-or-erased semirings, but I think some things (e.g. around sums) are hard/awkward/impossible to type and the ?/+/* modalities make some make things easier while still allowing the abstract machine to know exactly when to “optimize the heap” based on a runtime flow that “activates” a particular static analysis.
Of course, it’s still MLTT “compatible” – anything that would type-check in MLTT should type-check in my variation of GRTT by “simply” using the
*modality everywhere – so you get full proofs-as-programs and a total language.I’m probably a bit off in the weeds, but it still makes my brain buzz to think about and occasionally I’ll make progress. I’ve been a little bit distracted with https://gitlab.com/bss03/nested which should allow me to write the abstract machine as a fold, but as proven to be place I can also put a lot of programming time into (again, with sporadic real progress).
Interesting. Do you have some specific goal in mind? Like, implementing a language/library for the GRTT stuff.