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.

Brendan Zabarauskas

@brendanzab

Jun 21, 2018

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?

Brendan Zabarauskas

@brendanzab

Jun 21, 2018

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!

Bob Atkey

@bentnib

Jun 22, 2018

I'm aware of it thanks :) Rust's effects are more complex, because they involve interactions with the separation of memory, inplace update, and ownership transfer. I have done a bit of work on simpler systems, and want to combine them with coeffects: bentnib.org/dpia.html

Replying to

and

Yeah, baby steps I guess! Thanks again to you and your students for all your hard work! 🥰

10:35 AM · Jun 22, 2018Twitter Web Client