~icefox/garnet#57: 
Destructors/linear types

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.

Status
REPORTED
Submitter
~icefox
Assigned to
No-one
Submitted
1 year, 9 days ago
Updated
2 hours ago
Labels
T-DESIGN

~icefox 1 year, 9 days ago

I guess the place to start is to make linear types and then go from there.

Oh, I think you could implement Rust-like Drop with 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.
end

It... feels weird. But it would work, at least as well as anything else with modular implicits.

~icefox a month ago*

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.

~plecra 8 days ago*

For a different point of view on Linear vs Affine: Splat considers linearity as the inability to mem::forget the 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 calls Drop::drop(that_value), and naturally complains if the trait isn't implemented for a type. T: Drop is 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, but forget would break that guarantee: It's linear.

~icefox 2 hours ago

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

~icefox 2 hours ago

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.

Register here or Log in to comment, or comment via email.