Minor updates to the "Context Constrained Computation" abstract by me and . Fixed typos, band elimination rule, and author-year citations! bentnib.org/context-constr
Conversation
Random thought I've been having: how viable do you think tracking regions (lifetimes in Rust) using these quantitative-coeffecty things would be? Could one use the partial ordering for that? Also wondering about static arguments/constexprs as well: docs.idris-lang.org/en/latest/refe
I think tracking regions may be feasible, but it involves a mixture of effects (the actual mutation of stuff) and the coffect annotations, so it needs more work. Static args or multi-staging is definitely on our list to do: I think that the (max,+) semiring over nat+infinity.
1
1
So cool! Yeah I was wondering about that - iirc, separation logic has been used to model Rust's lifetimes as well - is this another way of looking at that? Ie. coeffect is the precondition, and the effect is the postcondition? Or am I a little off here?
1
Show replies