verdagon

Good to see some more uses of linear types! Very few languages can use linear types, and their potential is huge IMO.

OP shows the benefits of a linear RC that tracks references dynamically, and one can even imagine a version where the compiler tracks the references instead.

For example (for those who are more familiar with Rust) imagine that it had linear types and that we used them for matthieum's static-RC [0] (like suggested by frank-king at [1] to prevent leaks) and you'd have a pretty good idea of linear static RC.

I also talked about a possible alternative linear static RC at [2] and [3] (I didn't explain it well at all, happy to elaborate), though lately I suspect that one would need to add a GhostToken-ish [4] substance to allow safely reading/writing the shared value, or perhaps a RefCell.

I suspect that something like GhostToken could also solve OP's restriction that types be opaque, if Haskell has something like GhostToken... I could be wrong on that though.

[0] https://github.com/matthieu-m/static-rc

[1] https://github.com/matthieu-m/static-rc/issues/7

[2] "Linear reference counting" in https://verdagon.dev/grimoire/grimoire#the-list

[3] https://www.reddit.com/r/rust/comments/1d06gjo/comment/l61qm...

[4] https://www.reddit.com/r/rust/comments/p5f78s/ghostcell_sepa...

I've been looking into this, and I suspect that one actually needs surprisingly little to interoperate safely with Rust.

TL;DR: The lowest common denominator between Rust and any other memory-safe language is a borrow-less affine type.

The key insight is that Rust is actually several different mechanisms stacked on top of each other.

To illustrate, imagine a program in a Rust-like language.

Now, refactor it so you don't have any & references, only &mut. It actually works, if you're willing to refactor a bit: you'll be storing a lot of things in collections and referring to them by index, and cloning even more, but nothing too bad.

Now, go even further and refactor the program to not have any &mut either. This requires some acrobatics: you'll be temporarily removing things from those collections and moving things into and out of functions like in [2], but it's still possible.

You're left with something I refer to as "borrowless affine style" in [1] or "move-only programming" in [0].

I believe that's the bare minimum needed to interoperate with Rust in a memory safe way: unreference-able moveable types.

The big question then becomes: if our language has only these moveable types, and we want to call a Rust function that accepts a reference, what then?

I'd say: make the language move the type in as an argument, take a temporary reference just for Rust, and then move-return the type back to the caller. The rest of our language doesn't need to know about borrowing, it's just a private implementation detail of the FFI.

These weird moveable types are, of course, extremely unergonomic, but they serves as a foundation. A language could use these only for Rust interop, or it could go further: it could add other mechanisms on top such as & (hard), or &mut (easy), or both (like Rust), or a lot of cloning (like [3]), or generational references (like Vale), or some sort of RefCell/Rc blend, or linear types + garbage collection (like Haskell) and so on.

(This is actually the topic of the next post, you can tell I've been thinking about it a lot, lol)

[0] "Move-only programming" in https://verdagon.dev/grimoire/grimoire#the-list

[1] "Borrowless affine style" in https://verdagon.dev/blog/vale-memory-safe-cpp

[2] https://verdagon.dev/blog/linear-types-borrowing

[3] https://web.archive.org/web/20230617045201/https://degaz.io/...

Just did, thanks for the suggestion!

Thanks! And yeah I get that a lot >_> You're always welcome to swing by the discord where I can give a less arcane explanation! (https://discord.gg/SNB8yGH)

Hah I like this one!

PS. Congrats! https://verdagon.dev/blog/easter-egg-notes

It could, but then that List would have to be linear itself, and then the program would make sure that you eventually drain the list and destroy each element.

(One caveat is for linears in globals, which aren't implemented in Vale yet. We haven't decided which strategy we're going with there, but TFA talks about some)

A really good question. In short, a linear List (or array, or hash map, etc) will only have two available destroyer functions:

1. drop_into(list, func): It consumes the list, calling the given `func` for each element.

2. expect_empty(list): Consumes the list, panicking if the list isn't empty.

I've got some weird plans for variants. Basically, we'd represent an enum as a non-heap-allocated sealed interface with a struct for each "case". Basically, think of a Scala case class. Then, depending on where we put it (heap vs local/member/element), it will be compiled differently (a traditional interface vs a tagged variant, respectively). ...I don't expect that to make any sense.

Alas, I haven't started on sealed interfaces yet. Right now I'm occupied with the Rust interop; I'm hoping we can be able to seamlessly e.g. `import rust.std.collections.Vec<i32>;` and have it work. A lot of pieces have to fall into place for that to work though, especially since that's generic and Rust doesn't even have a stable ABI. It's kicking my ass, and I'm having a lot of fun with it!

Almost, but see the replies to IcyWindows' comment for why this unfortunately doesn't work in C++. Also, I would love it if C++ had a way to actually move. That would unlock all sorts of interesting possibilities.

You're exactly right, and that's kind of what Vale's `destruct` is, if you squint.

They almost work like this. std::move doesn't actually move an object; it leaves an intact instance... which we still don't know how to destroy (because its destructor is private). This also means that if we have an e.g. Outer struct whose constructor takes some kind of linear type, that Outer has no way to ever relinquish it again, which is a prerequisite of all those desirable linear type / higher RAII patterns.

This godbolt hopefully illustrates: https://godbolt.org/z/qqMnnKbnd though apologies if it's not too clear.

If C++ didn't have its quirks, you'd fundamentally be correct. Higher RAII can almost completely be implemented by this one sentence: make destruction private. (In fact, that's why Vale's `destruct` keyword is file-private)

There are a couple technical reasons:

1. In RC and tracing GC languages, a linear object would need exactly one special "linear" reference to it, which would be responsible for eventually "consuming" (though not deleting) the object by handing it to its final destination function. (You can tell, I'm trying real hard to not say destructor here)

2. In single-ownership languages like C++, Rust, etc. we've been conflating the destructor to handle two things: fulfilling the object's final purpose, and handling exceptions/panics. It seemed convenient at the time, but it also prevented linear types.

But honestly, I think we were just stuck in a local maximum. There was no reason to change those points because we didn't know about higher RAII, and we didn't know about higher RAII because those two points prevented linear types.

But with more of us exploring this new area (Vale, Austral, maybe even Mojo!), I daresay we'll one day see linear types and higher RAII entering the mainstream. Especially if someone can come up with a better name!

I'm glad you brought inheritance up! This rule has solved it nicely in my experience: if a struct is linear, then it can only inherit linear interfaces. And implementation inheritance works because it's really just a combination of interface inheritance + composition + method forwarding, none of which seem to have any particular trouble with linear types.

Even if a language really wanted to have linear types in reference-counted objects, I don't think we'd see cycles in practice. Generally, for a reference-counted object to contain a linear type, we'd need exactly one reference to be the special "linear reference" (think a linear flavor of unique_ptr) which has ultimate responsibility for "consuming" (albeit not deleting) the contents. Making a unique_ptr cycle is much harder than making a regular RC cycle, so I'm not too worried, even if it is theoretically possible.

Re: trivial moves, I'm not sure what you mean. The system works through the entire program, not just local variables. Also, the `onException` method would also handle panics. Hope that helps!

Thank you, my friend =) So glad to hear you enjoy the articles!

Cool to see this on HN!

This is my favorite part of language design: you get to play with weird ideas and see how the implications cascade through the rest of the program. It kind of blew my mind when a linear type solved a caching problem.

Now it's kind of a curse, because any time I code in a normal language (even the modern ones like Scala and Rust) I see places (concurrency, coroutines, etc) where we could have statically prevented these bugs.

Perhaps. The problem space's difficulty can bring some inherent complexity, yes... but I often hear that fact used to justify adding complexity that isn't actually necessary.

Biggest example I've seen: wanting to use Java for a web server where a 10-line node server did wonderfully. Or similarly, wanting to use async/await in Rust when threads are more than sufficient.

Sometimes I think we make our problems unnecessarily complex by chasing efficiency perfection.

This PumpkinOS project is pretty incredible. I can't imagine how much effort it would take to be compatible with all the system calls that the average Palm app would expect. I remember Palm did some truly weird things with memory: anything moderately large would need to be put into a special memory block that the OS could rearrange at will, and one would need to lock the block's handle to keep it stable while accessing it. Stuff like that must have been challenging (and fun) to implement in PumpkinOS.

This brings me back. I used to make little games for Palm OS, and I was so excited for the next version of the OS which would let one use the (then new) Palm OS Development Suite to make programs. It was also the last OS I've used where an app had a central event loop. Everything else today has UI frameworks that handle it for you. Things are easier now, but I still miss it.

It makes me wonder if there are any language constructs that can make this a reasonable feature. One idea I've been tossing around is having the ability to roll back any changes to mutex-guarded data if an exception drops a mutex guard. It should be possible with the right language constructs and bookkeeping.

Perhaps there are other mechanisms out there too.

I feel like the ability to destroy another thread isnt inherently bad, just... bad with today's languages. Just a feeling though.

Why's that?

I made no assumption like that, though do let me know if I've said something that could be interpreted that way.

Rather, I think that the static analysis we see in today's languages just isn't powerful/flexible enough to reason about safety in a lot of the patterns that we know are safe. I'm also uncertain if it can _ever_ catch up to what we know to be safe, but I wouldn't be surprised if we get there in a few hundred years.

For example, borrow checking is a step forward and can guarantee safety, but does nothing about the other half of correctness, specifically liveness. [0]

Linear types (like in Austral [1] and Vale's higher RAII [2]) can help guarantee liveness, but we still have further to go.

Both are based on single-ownership (in the C++ sense) like Rust, which introduces errors that e.g. Haskell would not.

But even Haskell (and LiquidHaskell which has linear types) don't go far enough; Coq goes even further.

So yes, like you say, we have a long way to go w.r.t. correctness, even past the borrow checker though it is a big step forward.

To my original point though, even all of these tools put together will put restrictions on a program such that it sometimes won't be allowed to take the most optimal approach. Perhaps someday we'll get there!

[0] https://en.wikipedia.org/wiki/Safety_and_liveness_properties

[1] https://austral-lang.org/linear-types

[2] https://verdagon.dev/blog/higher-raii-7drl

I don't think the article made that conclusion? I see this in there:

> As seen in the benchmarks, the current Rust standard library unstable sort implementation outperforms the C++ standard library counterparts

And I can't find any generalizations like that from the author, though I may have missed it.

> Often safety and performance are characterized as a set of zero sum tradeoffs, yet often it's possible to find better tradeoffs who's holistic properties improve upon a previously seen "either or".

There is truth in this, but I'm not sure whether the reader can/should extrapolate this to larger situations (not that the author implied we should, but it was my first interpretation).

We know that in certain situations, borrow checking works really well and allows us to guarantee safety with minimal friction and no overhead.

But there are other cases where safety and performance _are_ in contention, and we must choose one or the other. Anyone who has been forced to satisfy the borrow checker by using a .clone(), using Rc, or refactoring objects into a hash map and referred to them by an ID (that must be hashed to exchange with a reference), has felt this contention. In https://verdagon.dev/blog/myth-zero-overhead-memory-safety, I concluded that there's no general approach that always has zero overhead, at least not yet.

So perhaps the best interpretation from this study is that often, for small enough programs/areas, there is no conflict between safety and performance.

For larger programs with more complex requirements and data interrelationships, the question becomes much more interesting.

> I see no reason why a straight port from Rust to C++ wouldn't have been possible while satisfying their requirements.

Like the author, I also don't see a reason for this, but I've never tried myself. I've always thought that with the restrict keyword, one could make any C++ as performant as any Rust code. Perhaps something else got in the way there.

> Often safety and performance are characterized as a set of zero sum tradeoffs, yet often it's possible to find better tradeoffs who's holistic properties improve upon a previously seen "either or".

There is truth in this, but I'm not sure whether the reader can/should extrapolate this to larger situations (not that the author implied we should, but it was my first interpretation).

We know that in certain situations, borrow checking works really well and allows us to guarantee safety with minimal friction and no overhead.

But there are other cases where safety and performance _are_ in contention, and we must choose one or the other. Anyone who has been forced to satisfy the borrow checker by using a .clone(), using Rc, or refactoring objects into a hash map and referred to them by an ID (that must be hashed to exchange with a reference), has felt this contention. In https://verdagon.dev/blog/myth-zero-overhead-memory-safety, I concluded that there's no general approach that always has zero overhead, at least not yet.

So perhaps the best interpretation from this study is that often, for small enough programs/areas, there is no conflict between safety and performance.

For larger programs with more complex requirements and data interrelationships, the question becomes much more interesting.

> I see no reason why a straight port from Rust to C++ wouldn't have been possible while satisfying their requirements.

Like the author, I also don't see a reason for this, but I've never tried myself. I've always thought that with the restrict keyword, one could make any C++ as performant as any Rust code. Perhaps something else got in the way there.

Sometimes, having a quick, inaccurate, but easily-verifiable answer is better. For example, when you're trying to remember the name of that one function to call, or ideas on where to travel next month.

Also, not super relevant, but in e.g. combat situations one is often better off running now in any direction rather than pondering which direction is absolutely optimal for running from the lion. You'll know soon enough whether it was the right direction. There's probably a metaphor somewhere in there.

I believe coroutines are mostly unrelated to RAII. One can still have coroutines in a single ownership world and guarantee destructors are called.

(If not, I have a lot of redesigning to do for Vale!)

Also, doesn't your mentioned problem also happen for full threads? I'd imagine they'd contend for those 10 connections no matter how you did your concurrency.

I'd love to hear more on this, what are some problems we don't see? And what do you mean by effective?

ELI5 layers? Could someone like me see when I've used one layer as opposed to another, when using ChatGPT?

Austral is still alpha, so this kind of thing is expected. It's heading in a good direction, give it some time.

Amazing article! I especially like the distinction between resource safety and memory safety. I think a lot of folks don't realize that a memory safety approach can help or hurt one's resource safety.

The only mainstream language today that really nails resource safety IMO is C++. Ironically, Rust takes a bit of a step backward on this dimension, e.g. an AVL tree will likely need to be backed by a Vec and be more prone to "leaking" nodes, since the Vec owns the node, not the parent. Now imagine a program has actual resources instead of an AVL tree having nodes, and one can see the problem. A logical owner often needs to give up ownership to the central collection, losing resource safety.

That could be fixed by blending borrowing with linear types just like Austral did. [0] The logical owner (parent in AVL tree example) could wrap the child ID in a linear type, and thus can't accidentally drop() it, and must consume it by removing its referred node. I sometimes call this pattern of linear types "Higher RAII" [1].

> [Regions] do not address concurrency and data race freedom.

This is true of today's languages, but I hope to soon have a prototype of immutably borrowing an entire region at once to allow multiple threads to access it without data races.

[0] https://austral-lang.org/linear-types

[1] https://verdagon.dev/blog/higher-raii-7drl (am author)

Yep, then today's Vlang got to that name first, so we had to call it Vale instead!