Reading club: Linear types

tags: reading-club

Link: https://blog.yoshuawuyts.com/linear-types-one-pager/

Different Designs

// current Rust
fn drop<T>(value: T);

// complete manual system
trait Leak {}
fn drop<T: Leak>(value: T) {..}
fn identity<T: ?Leak>(value: T) -> T {..}

// auto-traits
auto trait Leak;
impl<T> Leak for T {}
fn drop<T>(value: T) {..}                   // `T: Leak` bounds are inferred
fn identity<T: ?Leak>(value: T) -> T {..}

// maybe-leak effect (superset a la `async`)
fn drop<T>(value: T) {..}
!leak fn identity<T>(value: T) -> T {..}

// linear effect (a la `const`)
fn drop<T>(value: T) {..}
linear fn identity<T>(value: T) -> T {..}  // label the entire function
fn identity<linear T>(value: T) -> T {..}  // trait transformers syntax

Note: I (Yosh) don't really like linear as a keyword, so it's more for illustration purposes. Imo leak seems better, but that would imply !leak fn, which maybe is a bit weird - but again idk. Exact syntax is sort of the least important thing here imo.

(eholk) Nice seeing options laid out like this. Opt-in or opt-out. Opt-in would probably be less disruptive.

(yosh) Would be nice if we could start with an empty set of effects (total), and make all other effects opt-in on top of that. But that's not really what we have today, but maybe something to strive for? idk

Koka paper: https://arxiv.org/pdf/1406.2061.pdf

Fork the Compiler?

(eholk) This seems like the kind of language change where (temporarily) forking the compiler makes sense. It means we can have a trial period before adding an insta-stable + ?Leak bound to everything in std, but also would give people a chance to try using the language to get a sense of how usable it is.

(As far as I [eholk] know, no one has shown that true linear types work ergonomically at scale, so this would give us a chance to demonstrate that.)

Yosh: the changes you would need to make to the stdlib is disallow:

• statics
• everything that's ManuallyDrop (mem::forget)
• everything that's UnsafeCell-based (Rc, Arc, Mutex, channels)
• thread::spawn

Eholk: Do we need UnsafeCell for 1:1 channels?
Yosh: that's a good question!

eholk: an implication of channels needing UnsafeCell is that linear types cannot be Send? Maybe we need a linear channel?

Yosh: I think we can make linear types Send, but I don't know if we can create linear channels?

Shared Ownership, Interior Mutability, Guaranteed Destructors - Choose Two

(eholk) If I remember right from the leakpocalypse, the problem was that Rc/Arc combined with interior mutability was how we got in to trouble. It seems like maybe the primary contribution of this type is that it lets us annotate either Rc or UnsafeCell with !Leak to let us choose another side of the triangle, but which one should we pick?

(eholk) Is Interior Mutability + Guaranteed Destructors possible? Yes! Box<RefCell<T>> can't make cycles by itself.

(eholk) Can't make cycles with just Arc, except if you use the cyclic constructors. new_cyclic

Gankra's safe forget code:

fn safe_forget<T>(data: T) {
    use std::rc::Rc;
    use std::cell::RefCell;

    struct Leak<T> {
        cycle: RefCell<Option<Rc<Rc<Leak<T>>>>>,
        data: T,
    }

    let e = Rc::new(Leak {
        cycle: RefCell::new(None),
        data: data,
    });
    *e.cycle.borrow_mut() = Some(Rc::new(e.clone())); // Create a cycle
}

Eholk: you need both Rc and RefCell to make a cycle. That means interior mutability + shared ownership.

Yosh: does that then mean that we can leave Arc alone and only disallow the UnsafeCell-based Mutex etc types?

Eholk: I think so!

Eholk: Do we want just interior mutability without shared ownership? No! If you have unique ownership you can already mutate, so interior mutability is only interesting with shared ownership.

Yosh: There seems to be a connection between tree shaped data and tree shaped computation (structured concurrency) - exactly what that connection is is unclear.

Connection to async drop

Yosh: had a chat with Niko on this a few weeks ago. We sort of settled on that async Drop and linear Drop probably shouldn't be the same feature?

Yosh: we also discussed what a full async drop would look like - if it propagates the way current Drop propagates, then we'd probably need a way to tag structs as async. So if you nest a struct with an async destructor inside of another struct, the destructors are still run.