4 ms·

> I think Rust will also get true linear types at some point This somewhat exists as `must_use`: https://doc.rust-lang.org/std/hint/fn.must_use.html https://do

> I think Rust will also get true linear types at some point This somewhat exists as `must_use`: https://doc.rust-lang.org/std/hint/fn.must_use.html https://doc.rust-lang.org/std/hint/fn.must_use.html >One key obstacle to this is that Rust supports panics anywhere-- there's no provision for "panic-free" code as of yet-- and a panic might need to drop values as part of unwinding the stack. Yes, there's a fundamental incompatibility between linear types and traditional exception handling. This was a big question I had to think about and answer in the design. Basically: Rust has "affine" types (a weakening of linear types) where values can be silently discarded. The compiler inserts destructor calls (whose behaviour is customized in the `Drop` trait). The compiler also emits the exception-handling code so that when a panic is thrown the stack unwound and the destructors are called. This approach is incompatible with linear types (linear types don't privilege any one function as the destructor). So linear types are incompatible with traditional exception handling. The choice, then, is: keep linear types or keep traditional exception handling. I decided to keep linear types, because they're simpler. The full rationale is elaborated at length here: https://austral-lang.org/spec/spec.html#rationale-errors https://austral-lang.org/spec/spec.html#rationale-errors

JonChesterfield 4y ago
> So linear types are incompatible with traditional exception handling. Nice to see this spelled out. If the instance can be summarily dropped without error you can throw past it, and ideally call it affine instead of linear. If the instance needs that close() call, you either can't throw past it, or you need to move the live instances into the exception instance as it passes by and deal with them at the catch site. I found a paper discussing that somewhere but didn't keep a reference to it. A possibly interesting compromise is to allow linear types, but their live range cannot contain an unknown function call, or a function call coloured with throws. That models holding on to some handle and not doing anything too hazardous until you can put it away safely.

JonChesterfield 4y ago

> So linear types are incompatible with traditional exception handling. Nice to see this spelled out. If the instance can be summarily dropped without error you can throw past it, and ideally call it affine instead of linear. If the instance needs that close() call, you either can't throw past it, or you need to move the live instances into the exception instance as it passes by and deal with them at the catch site. I found a paper discussing that somewhere but didn't keep a reference to it. A possibly interesting compromise is to allow linear types, but their live range cannot contain an unknown function call, or a function call coloured with throws. That models holding on to some handle and not doing anything too hazardous until you can put it away safely.