hoo boy. No idea how to cleanly integrate these with modules.
Definitely gonna need to look at Zig and see how this works there.
This also interacts with move semantics/linear types and whatever our version of Copy is, which will be its own adventure.
I guess the place to start is to make linear types and then go from there.
Oh, I think you could implement Rust-like
Dropwith modular implicits like so:type MyThing = ... const DropMyThing = Drop(MyThing) { .drop = fn(t MyThing) = ... end } fn drop(|T| drop_impl: implicit Drop(T), thing T) = drop_impl.drop(thing) end fn foo() = let droppable_thing = MyThing ... do_stuff_with(droppable_thing&) -- droppable_thing goes out of scope, the compiler inserts this: drop(droppable_thing) -- and implicits find the matching drop impl. endIt... feels weird. But it would work, at least as well as anything else with modular implicits.
are affine types not enough?
There's rare but significant cases where you Actually Need some context to destroy a type; my personal example is Vulkan resource handles. You can't really expect the compiler to figure out that context on its own, so you need a way to call destructors with an argument and make sure that all code paths lead to a destructor being called. There's solutions to this, but few pretty ones; basically comes down to "handle it at runtime" by smuggling
Rc<Context>into your objects or something.
For a different point of view on Linear vs Affine: Splat considers linearity as the inability to
mem::forgetthe value (Rather,trait Affine { fn forget(self); }). Resources like vulkan resource handles are perfectly safe to forget, so they're Affine. Whenever values go out of scope, the language callsDrop::drop(that_value), and naturally complains if the trait isn't implemented for a type.T: Dropis unrelated to linearity - linear types can implement Drop, and normal types dont have to.Linearity is only used for types that require it in the strictest sense:
OutPointer<T>has made a type-level guarantee that the pointer will be written to, and its required for soundness, butforgetwould break that guarantee: It's linear.
Resources like vulkan resource handles are perfectly safe to forget...
Safe but not correct, so that's an interesting distinction to think about. I guess "safe" means "it doesn't break the assumptions the compiler makes about the program", while "correct" means "it doesn't break the assumptions the programmer makes about the program".
To transcribe our interesting but incomplete talk about it on discord:
{} /s /j — 07/14/2024 6:43 PM but wat is forgetting? is that not the same as dropping? (posting here cuz i dont wanna create an account pollute the thread with my skill issues) Plecra — 07/14/2024 6:44 PM um do you rust? {} /s /j — 07/14/2024 6:44 PM not enough to say im seafood yet Plecra — 07/14/2024 6:44 PM bc no, theyre completely different {} /s /j — 07/14/2024 6:44 PM so uhhh maybe its just a skill issue Plecra — 07/14/2024 6:44 PM fn forget(v: T) is a function in the standard library that does exactly nothing fn drop(v: T) is a function in the standard library (this is not accurate) that deallocates all the resources in v {} /s /j — 07/14/2024 6:45 PM hmmm so wats the point of forget? to move a value "out of scope" but not destruct its resources? Plecra — 07/14/2024 6:46 PM yep. it disappears. maybe you have a Vec<T> and deallocating it would be too slow 😁 but really, it comes up in cases where you're needed to do lower level stuff eg sometimes you want to write fn File::close(f: File) -> Result<_> By default, rust will Drop your file but you've already closed it, because that's what this function is for so you need to mem::forget() it {} /s /j — 07/14/2024 6:48 PM so if u forget something that holds resources, would those resources become dangling pointers? assuming nothing else has access to said resources? say u dont close the file, but u forget it, wat happens? the file just remains open until the OS decides to clean up ur process? Plecra — 07/14/2024 6:50 PM leaked pointers (im being pedantic bc) dangling pointers are something else :) {} /s /j — 07/14/2024 6:50 PM ah fuck i always get them confused Plecra — 07/14/2024 6:50 PM yea the file just remains open youve leaked it {} /s /j — 07/14/2024 6:50 PM hmmm ok...so its using move semantics to say "hey this thing isnt usable anymore" but not going through the hoops of drop Plecra — 07/14/2024 6:51 PM btw this is often the name used in linear typing literature - some values are able to be "forgotten" from the typing context they're the affine vals Plecra — 07/14/2024 6:51 PM sure, yeah Plecra — 07/14/2024 6:52 PM Its important to remember that a basic type with no features in a linearly typed system has no functions you can call on it and MUST NOT go out of scope meaning if you let x = that_basic_value, there's no way to write a valid program: It'll go out of scope and youll get a compile error In a PL you need to define things that the value is capable of it's fine to do that with some bundle of functions my_very_special_task(that_basic_value, metadata) would remove it from scope drop is a special function that the compiler will automatically call, but that's it {} /s /j — 07/14/2024 6:52 PM hmmm interesting...so forgetting a value is considered a use of a value? {} /s /j — 07/14/2024 6:53 PM thats wack using a value to forget it just makes my brain hurty hurty but it does make sense Plecra — 07/14/2024 6:54 PM :) Yeah, lots of types can be forgotten it's valid to stop using a u8 because you "forget" it {} /s /j — 07/14/2024 6:54 PM so if u forget a value...how does that differ from just saying it was affine or is forgetting a value a way to reget affine behavior Plecra — 07/14/2024 6:54 PM Imo it's the definition of it being affine {} /s /j — 07/14/2024 6:55 PM oh i see Plecra — 07/14/2024 6:55 PM The ability to forget a value of a type means that the type is affine {} /s /j — 07/14/2024 6:55 PM so in a linear type system, if a value is forgotten in scope, its considered a use, this would be no different semantically from that value being introduced under an affine type system instead basically saying { // affine let x = some_value(); } is equivalent to { // linear let x = some_value(); forget(x); // fuck it } ? Plecra — 07/15/2024 6:09 AM sure. x in both examples must be an affine type, and these have the same semantics sorry I didnt reply last night! Think I fell asleep 😋 icefox — 07/15/2024 10:18 AM Forgetting a value leaks it That's what it does Saying "it does nothing" is useful from a formal sense but not a practical one. Uuuuugh lemme catch up for real I like the idea of inverting the definition but lemme try to figure out what that actually implies... Hmm, almost anything is safe to leak, but many things are not correct to leak... Locked mutexes and file handles without flushed buffers come to mind. To me the only really important advantage of linear over affine is "force the user to clean up correctly in the 10% of cases where the compiler can't" The out pointer example confuses me, how does that work at all? If you consume the out pointer, won't that consume the underlying value as well? Reliable destruction in general is actually really interesting, cause it's impossible to guarantee. You can do all the clever design you want but something can always pull the plug on your program. The programs that are actually resilient are not the ones that do all destruction correctly, they're the ones that recover from stopping in a bad state -- databases and filesystems with a write-ahead log are the ones I am most familiar with. Plecra — 07/15/2024 10:44 AM (&out T).write() : &mut T is a consuming op :) yeah, a pragmatic model treats linear types as "if the program still exists, this is still true" icefox — 07/15/2024 10:45 AM So it aliases the value? Plecra — 07/15/2024 10:45 AM mm no? Im not sure what you mean Im treating &out T as a &mut T that must be written to icefox — 07/15/2024 10:45 AM Idk I slept like shit I'm sure it makes sense Plecra — 07/15/2024 10:45 AM by writing to the &out T, we have fulfilled that obligation icefox — 07/15/2024 10:45 AM Right how do you access the written value outside of that obligation? Plecra — 07/15/2024 10:46 AM and yeah! I totally agree :) I would normally call it "leaking" but {} said they werent confident with what "leaking" meant icefox — 07/15/2024 10:46 AM I guess if it's always a function param that's just how it goes Ooooh Plecra — 07/15/2024 10:48 AM soo let mut a = uninit; // (made up syntax) // out_ref is a reborrow of initialized // when we get access to `initialized`, its guaranteed to be init let (out_ref, initialized: &mut T) = (&out a, &mut a); let someone_inits_the_out_ref: &mut T = write(out_ref); // borrow still held: `initialized` unusable drop(someone_inits_the_out_ref); // `initialized` is now usable Plecra — 07/15/2024 10:50 AM fwiw I dont view this as the "inverted" definition. It's kinda necessary if you want the type system to work well: If we treat linear types as Not(Affine), we get problems stemming from the fact that type systems behave badly with negation When looking at the type checker's role, it needs to identify "well typed terms", and affine types can be used for strictly more things that linear types Plecra — 07/15/2024 10:53 AM Locked mutexes are a particularly unique case, yeah. I'm a big fan of poisoning - I have a special class of DestructiveDrop that can be used when you want to really force the value to be consumed and its ok to break some correctness Leaking the mutex is really bad, but its not an actual correctness issue on its own - most code will just lock up but stay well-typed. You can certainly have a MandatoryForwardProgressMutex with a Linear MutexGuard icefox — 07/15/2024 10:54 AM Idk why affine types would be fine forgetting a value though, that seems like an orthogonal problem Plecra — 07/15/2024 10:55 AM Hm. The definition of affine is being able to be forgotten affine types have no more properties why do you think theyre orthogonal? icefox — 07/15/2024 10:56 AM I thought they were types where the place they are consumed can always be inferred by the compiler, vs linear where you have to tell it explicitly All I know about affine types is "it's what Rust does", so Plecra — 07/15/2024 10:57 AM Yeah, there are no linear types in rust It's must_use, but that's not enforced by the type system icefox — 07/15/2024 10:57 AM References are certainly able to be forgotten Plecra — 07/15/2024 10:57 AM all types in rust are affine (or "normal" types when they're Copy/Clone) icefox — 07/15/2024 10:58 AM Okay they can all be forgotten then, sure... But there's always an implicit "consume this here" when they go out of scope, unless they're Copy. Plecra — 07/15/2024 10:59 AM yeah! And it's lovely, its very handy syntactic sugar imo it's most useful to just view that as a normal trait though its unrelated to linearity Types can provide a default function that the compiler's allowed to use to consume them at the end of blocks icefox — 07/15/2024 11:00 AM That has nothing to do with the type being affine though, then? Plecra — 07/15/2024 11:00 AM yep icefox — 07/15/2024 11:00 AM Fml Plecra — 07/15/2024 11:00 AM because a linear, Drop type makes perfect sense it's something that must be dropped (or passed to some other consuming method, if it has one) Plecra — 07/15/2024 11:03 AM unflushed buffers are imo acceptable. in most cases, if I accidentally create an Rc cycle and leak it, im ok with the BufWriter not flushing. In cases when it's a major error, you can create a LinearBufWriter, but you always have to decide whether its worth the inconvenience of ensuring youre using it linearly I think linearity is best to be really conservative with. it's a strong property icefox — 07/15/2024 11:04 AM Eeeh Writing out part of an important value to a file is not really good. Plecra — 07/15/2024 11:05 AM hm that's probably just how I approach writing files, then? I normally prefer to explicitly flush to checkpoint various states of the file icefox — 07/15/2024 11:05 AM Yeah I just close the file when I'm done with it :p Anyhoo So if affine isn't just "linear but a bit weaker" then what is Rust? Plecra — 07/15/2024 11:06 AM What do you mean? Rust supports affine types + borrowing icefox — 07/15/2024 11:06 AM And almost linear types Plecra — 07/15/2024 11:06 AM What is that? #[must_use] is lint-level linear types yeah icefox — 07/15/2024 11:07 AM Every value gets cleaned up at a place known at compile time Plecra — 07/15/2024 11:07 AM no, any value is valid to forget (from the pov of the type system) rust doesn't implicitly forget your values which is nice, but imo a language design feature. it doesnt change the type system icefox — 07/15/2024 11:08 AM From the pov of the type system but not the runtime Plecra — 07/15/2024 11:08 AM from the pov of the type system, it's just straightforward affine types icefox — 07/15/2024 11:08 AM There's more to a language design than the type system :p Plecra — 07/15/2024 11:08 AM exactly :) this is a non-type system language design point so lets not call it "linear types" icefox — 07/15/2024 11:09 AM Ahhhhh Fukkin hell I hate words Plecra — 07/15/2024 11:09 AM Id say RAII is the most common term for it (whether or not its 'good' is up to u :P) scope-based desctructors used on all variables rust kinda just calls it Drop icefox — 07/15/2024 11:13 AM It's funny cause Drop is *almost* fine-grained enough Plecra — 07/15/2024 11:17 AM oh, how do you mean 😮 I had been kinda assuming its perfect do you want it to drop sooner? icefox — 07/15/2024 11:22 AM No, I meant more in terms of its functionality It can't quite handle contexts, can't quite handle different allocators, stuff like that. Plecra — 07/15/2024 11:27 AM ahhh totally :) I've got a solution I really like to that icefox — 07/15/2024 11:27 AM Oho? Plecra — 07/15/2024 11:27 AM It's not a single fix, but my Drop is allowed to be effectful and it covers async Drop + fallible Drop v nicely impl Drop for TcpConnection { fn drop(self) <NetworkWait> { self.socket.close().await // this is ok :> } } icefox — 07/15/2024 11:30 AM Aha Can you get other values into the drop function? Hmm, how does fallible drop work? Plecra — 07/15/2024 11:41 AM can you gimme an example? (yes with caveats) impl Drop for File { // this will be called and raised at the end of scope // **if** the caller scope is error-compatible // // for ~low level code, the compiler will insist you // explicitly `drop(file : File).try` // or `drop(files : Vec<File>).try` fn drop(self) <Os.Error> { self.fd.close().try } } "error compatible scopes" can be things like script { par-for file in walkdir() { print("`file` has `file.count_lines()` lines") // in a script, the language will allow implicit `drop(file)` } } the other case is with catch(Os.Error(e)): return task.bail(e) // `Os.Error` doesn't need to be explicitly handled here let a = open_file(stuff) // without the handler, this line would need .try a.write(header) data_generator.fill(a) icefox — 07/15/2024 11:57 AM Sorry, RL is kicking my butt I'll have to come back to this later
Okay so, to try to rephrase my rambling, the fundamental way I think about ownership is "who has to destroy/clean up this value?" The basic assumptions are that every value must be cleaned up in a particular place, the cleanup must happen (within the life of the program, barring an abort or something), and it must happen only once. Ownership/linear typing is a way of determining automatically where the cleanup should happen. I suppose what you then do with this information is up to the language designer: Rust inserts the cleanup code automatically, Austral yells at you to do it yourself. I just want Garnet to do it the Rust way 90% of the time and let you require the Austral way when necessary.
(Actually it's interesting to think of other memory management in these terms. Refcounting relaxes "cleanup must happen only once", tracing GC relaxes "the value must be cleaned up in a particular place", and arenas/just-never-free relaxes "the cleanup must happen". Huh!)
Cleaning up a value can cause side-effects. In fact, I can't think of any case where it has to happen that doesn't 'cause side effects, 'cause by definition it's the last thing that will ever touch that value. So phrasing it as effect handlers actually sounds pretty reasonable. I just kinda don't want effect handlers in general 'cause I am not convinced they're a good way to handle side effects. :-P
So with affine values, they don't have to be cleaned up. In reality, the cleanup still occurs, but consists of popping the stack or overwriting registers or something that the language user can't observe. It just happens anyway in the background the same way that a GC does. However, because of this it means that you then can't clean up the value, because adding a destructor means it would perform side-effects. So that would break the "cleanup only happens part" of the ownership system. This also means you can copy these values freely since, well, the language doesn't need to figure out where to clean them up. Rust also makes this require that copying/cloning the value has no side-effects; ie, the value is
Copy.It's interesting to think of the possibilities you could have for a copy constructor to run as long as it For Realsies has no side effects outside the value it's copying, but probably not actually very useful. You could make a counter that increments itself on each copy but... that's kinda it? You almost certainly don't want to try to guess where the compiler might or might not need to run the copy constructor. Best not to bother.
Aborts are interesting to think about 'cause they're an opportunity for a liminal state to exist. Even if you're not unwinding the stack and can't stop the abort from happening, it's a really tempting place to try to do some last-ditch actions. "Okay, this program is in an inconsistent state so we're kinda fucked, but at least before it dies forever we can..." The problem is of course that the program is in an inconsistent state, so your last-ditch actions may fail too and you get the software equivalent of a double-fault. This doesn't make it useless, backtraces are the best thing in the world, but does mean you can never rely on it. (Now I'm wondering if you can do something Clever like have the memory containing your last-ditch code and data not even mapped while the program is executing, and only mapping it when starting the abort, but that won't save the rest of your program's state that you might want to do something with, so.) Doing this naively just gets you C's
atexit()function though, which I'm sure is full of footguns.Threads kinda screw this up though 'cause they violate the assumptions of how processes work in all sorts of ways. Unlike Plecra I don't think that locked mutexes are a particularly unique case, more like they're a very general symptom of a very gnarly problem. A poisoned mutex says at runtime "oh shit this program is in an inconsistent state", costing a level of indirection to do so (I think?). It's the same sort of cover-your-ass measure that that a call stack canary or a tombstone value left by a debugging allocator is.
Unlike Plecra I don't think that locked mutexes are a particularly unique case, more like they're a very general symptom of a very gnarly problem
What are other examples of this problem? Ime poisoning is a highly specific solution to the problem of having a
&mut Tto something that will be visible after a panic (other cases have eg aBox<T>on the stack that gets immediately deallocated). I've never needed another construct like it, and keep locking to a minimum anyway.