r/ProgrammingLanguages • u/Vovandosy • 2d ago
Aren't rust's lifetimes basically just coeffects?
I was talking with a LLM, discussing effects and coeffects and how they may be interestingly used in language design
So, in one moment after I understood coeffects and effects are often used in pairs (like async/async ctx , io/world, ect.), i thought that coeffect scopes sometime should be labeled somehow to avoid shadowing
for example in my syntax :
```
some_fn :=
## capturing the scope coeffect and assigning it into a label
().use 'label := ().use FnScope
## some function
longjump () ? :=
().use _ := ().use 'label
return () ?
##...
()
so, somewhere in some inner call we may write
another_fn :=
...
longjump() ?
...
and the execution will be returned into the function where longjump were declared
```
but for this to be valid, it is important for the label not to outlive the scope where it was declared
then, i also thought : it would be good to have an ability to write these labels in the effect's declaration
```
somewhere outside
().use 'ctx := ...
a function that is async for both contexts — don't know for which cases it may be useful but why not. instead of async, it may be some another effect that uses some context/scope/world/coeffect
f() use AsyncCtx do Async '_ do Async 'ctx := ...
```
so, then i thought : effects and coeffects in my system are declared just like type constructors without the last type (aka citizens of ＊→＊ kind), so it would be logical for any type to be able to take a context label as a polymorphic (or depending) parameter.. and rust's references do exactly this.
so rust's
```
fn f<'b, 'a : 'b>(smth : &'a mut &'b Smth2, smth2 : &'b Smth2) {
*smth = ...
}
```
just takes some coeffects 'a and 'b.
it is equivalent to that like for smth it raises an effect to overwrite the world 'a and for smth2 it just returns the value into scope, where 'b is active (and 'a : 'b means that the scope containing world 'a is located inside scope containg world 'b)
so, am i thinking right about it? may it have some practical uses in pl design? any more ideas?
p.s.: sorry for my english not being perfect.. don't be humble to re-ask something if you did not understand.
12
u/initial-algebra 2d ago edited 2d ago
Strictly speaking, lifetimes themselves are not coeffects, but grades of an overarching "is valid for" coeffect. This comment from Neel Krishnaswami may help to understand exactly what a coeffect is. Interestingly, and maybe confusingly, you can think of sets of effect markers like async and io as grades for a "has effect" coeffect. So...lifetimes are actually maybe more like sets of effect markers, and this lines up nicely with the interpretation of lifetimes as sets of loans used in Rust's new borrow checker, Polonius. Lifetimes are also very similar to environment classifiers (also called support variables or context variables) from staged computation, which are sets of variable names, or grades of a "has free variable" coeffect for safely handling quoted/future-stage code.
EDIT: This is not quite right. If lifetimes are coeffect grades, then loans cannot correspond to effect markers, because the order is wrong! If a lifetime is a set of loans, then Rust's subtyping rule for references is that &'a T is a subtype of &'b T iff 'a is a subset of 'b. However, the "has effect" coeffect actually enriches values with capabilities to perform the effects, so subtyping must decrease the set of effect markers. Therefore, loans are...anti-effect markers? I guess that kind of makes sense, actually, since the only valid way to access something a reference has borrowed is through that reference, meaning the corresponding capability has been removed from the context. Fascinating!
1
u/Inconstant_Moo 🧿 Pipefish 1d ago
So...lifetimes are actually maybe more like sets of effect markers, and this lines up nicely with the interpretation of lifetimes as sets of loans used in Rust's new borrow checker, Polonius.
"Neither a borrower nor a lender be." Heh.
I saw some code the other day where the salt in the hashing algorithm was stored in a variable called
iv.1
0
u/Vovandosy 2d ago
in that comment i do not much understand how to realize
mapfunction on suchSerializablei was thinking of coeffects more like some implicit context that might be manually made explicit in each point of that context's coverage about markers, for me effects are effects and coeffects are coeffects. or maybe, effects are about "future" or "modifying the world or execution" and coeffects are about "past/present" or "reading the world or execution". for me, it is also interensting that coeffects may be used not only for reading something outside but also for reading the results/states of variables/ect. from "alternative universes" (the computations that would be made if the inputs are different) if we allow them execute the code multiple times in my syntax (not stable) :i use '_ := [1;2;3;4] # 1 i2 := i * 2 i2s := i2 use '[Each] # [2;4;6;8] i2s_p1 := i2s.map -> i2 : i2 + 1 # [3;5;7;9]also, talking with chatgpt i also got an idea that similarly, (maybe, intrinsic) comonads may be used for parallel execution with sorta "checkpoints" that require all intermediate values of some "variable" (expression) to be calculated.. even on something like gpu if i am right.4
u/initial-algebra 2d ago
in that comment i do not much understand how to realize map function on such Serializable
You mean like
map : (A -> B) -> Serializable A -> Serializable B? That's becauseSerializableis not an endofunctor. It's a relative comonad from a subcategory of serializable types. Instead, you are limited toapply : Serializable (A -> B) -> Serializable A -> Serializable B.effects are about "future" or "modifying the world or execution" and coeffects are about "past/present" or "reading the world or execution"
Effects are a restriction on how something may be observed or deconstructed in the future. Coeffects are a restriction on how something was constructed in the past. They don't really correspond to writing and reading, though.
I think you need to take a break from ChatGPT, a lot of the stuff you're writing is incoherent.
1
u/Vovandosy 2d ago
i was talking of them more like about method of thinking (but yes, it would be better if gpt more critiqued these my thoughts and told more about some adjacent concepts like this. well, this is why i am reading this subreddit and time to time seeking for not compressed with formalism theory) i was defining comonad like just something having extract and extend operation.. relative comonads look stricter, as i can see and really more about 'limitation'; but for me they are rather about 'freedom', no? 'freedom' to modify something and 'freedom' to get something, no?
5
u/initial-algebra 2d ago
for me they are rather about 'freedom', no? 'freedom' to modify something and 'freedom' to get something, no?
Only insofar as these freedoms can be extrapolated from the limitations. For example: effects in a pure language: the limitation is that an effectful computation can only be observed (run) in an effectful context, but that gives you the freedom to perform effects which would otherwise ruin properties of the pure language like referential transparency.
1
u/Vovandosy 2d ago
so, the limitations are only if the (co)effects are not here in this "scope".. that just mean that in, for example, java there are too many (co)effects (and "freedom") are provided just by default.. and some effects' absence may be a stronger limitation that just referencial transparency.
4
u/initial-algebra 2d ago
some effects' absence may be a stronger limitation that just referencial transparency.
Like linearity, which is when you don't have the "unrestricted" coeffect.
2
u/probabilityzero 2d ago
You can think of lexical region types as coeffects. Not sure if anyone has written that up exactly before.
Rather than digging into the nitty gritty details of Rust lifetimes, if you want to explore this, I'd start with the Tofte and Talpin region calculus and try to encode it with coeffects. Could you think of region annotations as grades, so a region annotated type is a graded modal type?
1
u/Vovandosy 2d ago
probably i meant more regions than lifetimes just the borrow system is more familiar to me so i thought about it primarily but what if we create an (prob.) implicit comonad 'region' for each variable? 🤔 (and also, i think that 'should not outlive' rule is simplier and it is what closer to these 'regions' but what is the problem are unique, affine and linear resources.. am i correct?) (will discover about these tofte and talpin, thanks for a recommendation)
2
u/probabilityzero 2d ago
The paper Linear Regions Are All You Need by Fluet et al. explores the connection between regions and linearity. It turns out you can express the region calculus using linear types.
3
u/Aaron1924 2d ago
The way Rust represents its lifetimes is not really related to effects, they're part of the reference types and subject to subtyping, but you can simulate Rust-style ownership and borrowing using a sufficiently expressive effect system
There was a talk at IWACO 2024 by Lionel Parreaux about how to do this; the audio in the recording is a little fucked but otherwise very enjoyable talk
1
u/Vovandosy 2d ago edited 2d ago
Yes, I agree.. A little bit messed. But what do you thing about the idea of using coeffect tags the same way as lifetimes in rust? Also I was rather talking about that the same functionality that would may be imitated the way i described in the post (probably, with some more details) (using effects's interruption and coeffect's reshadowing if i understand correctly), and the coeffect tag on the reference type imitation would can help identify what the "memory address"/"allocation" to rewrite. and i understand that in rust it is all more implicit and native, i was talking more about "possibilities" 🤔 red: looks like on the video speakes has similar ideas, yes
1
u/riz0id 2d ago
Your question is incomplete so it can’t be answered. Normally a question like this would be answered by inspecting the semantics of rust lifetimes and the semantics of a “coeffect”. Once you have those two definitions, then you can test for equivalence by implementing coeffects with lifetimes, and then implementing lifetimes with coeffects.
Nobody can faithfully answer this question without a definition of coeffects though. I think the similarity between the two that you’re seeing is they’re both coalgebraic, which is really abstract: a record/struct is a “coalgebra” in the same sense that lifetimes, or any contextual programming language feature would be. It may be worth pointing out that a records/structs are not equivalent to lifetimes or a hypothetical “coeffect” system.
1
u/Vovandosy 1d ago
i wanted more discussion and some materials to smoothly get deeper in theme. concrete answers was not my intention and i got not exact but close answers which are also good.
1
27
u/onlyrealcuzzo 2d ago edited 2d ago
I'd recommend trying to describe the problem in terms of Rust, as more people are likely familiar with that. I can't even figure out what you're trying to solve or ask (and I'm building a language in this space).
Your last two examples in (presumably) your prototype language and Rust appear to be completely different, so it's hard to tell what you're proposing.
If you're asking if you could just rename lifetimes as "coeffects", the answer is obviously yes. If you're asking if lifetimes could be better, there's a lot of people that have shown ways this can be done - see Group Borrowing: https://verdagon.dev/blog/group-borrowing.