Conversation

Minor updates to the "Context Constrained Computation" abstract by me and

. Fixed typos, band elimination rule, and author-year citations! bentnib.org/context-constr

Jun 21, 2018

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

Bob Atkey

@bentnib

Jun 21, 2018

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.

Replying to

and

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?

2:06 PM · Jun 21, 2018Twitter Web Client

Replying to

and

The combination of coeffects and effects reminds me of this paper: cs.kent.ac.uk/people/staff/d (haven't had a chance to get my head around it yet, alas). I'm guessing that's also probably on your radar though!

Brendan Zabarauskas

@brendanzab

Jun 21, 2018

To give some context, I've been planning for a while now to try implementing your quanititative type theory stuff in my silly little dependently typed systems language. I've had my eye on the co-effects and information flow stuff too though, so seeing it integrated is exciting!