Hacker News Reader

Comment by clord | Hacker News Reader

I really like the name "Linear Types" better than RAII. C++ ctor/dtor pairs are a sort of primitive linear type system that forces exactly one (implicit) use for each instance created.

Linear types nicely generalizes this so that we don't need RAII wrappers or whatever. Just produce values and pass them around, eventually to be consumed. It feels like this is a powerful language idea.

View on HN

> I really like the name "Linear Types" better than RAII.

They're not the same thing.

> C++ ctor/dtor pairs are a sort of primitive linear type system that forces exactly one (implicit) use for each instance created.

ctor/dtor are closer to what Rust provides which is an affine type system. Linear types must be used exactly once, affine types can be used at most once. You can initialise a C++ object and never use it, that would not be allowed in a linear type system.

I completely agree they're not the same things, but you can sort of see the "linear type" notion of "one and only one use" in RAII. Every construction has exactly one use (destruction.) it's fairly easy to see that RAII is a very limited version of a linear type system.

In an affine type system, every variable is used at most once. But C++ instantiations for RAII are not destructed more than once. Each instantiation has exactly one destruction.

> easy to see that RAII is a very limited version of a linear type system.

You might be interested in [0].

Affine logic rejects only the contraction rule [1]; unlike linear systems still has weakening [2].

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

[1]: https://en.wikipedia.org/wiki/Idempotency_of_entailment

[2]: https://en.wikipedia.org/wiki/Monotonicity_of_entailment

> Every construction has exactly one use (destruction.) it's fairly easy to see that RAII is a very limited version of a linear type system.

Aside from actually having it integrated to the type system, Rust does exactly that. RAII is not linear.

> But C++ instantiations for RAII are not destructed more than once.

That's also what happens in Rust, it's not a linear type system.

I thought the "use" was the destruction or movement of the value, in which case an object is used exactly once.

You may never use a C++ object, but it will be destroyed (under normal circumstances).

> I thought the "use" was the destruction or movement of the value

Implicit behaviour is not use.

> You may never use a C++ object, but it will be destroyed (under normal circumstances).

And that is different from Rust how? https://gankro.github.io/blah/linear-rust/#must-be-used-at-l...

Rust uses a similar (but significantly weaker) system called "affine types" underlying its borrow checker.

Nit: Rust's affine type system is orthogonal to its borrow checker, rather than underlying it (though they're both crucial to Rust's system of memory safety, of course).

Would it be correct to say that the affine type system underlies the ownership paradigm?

Absolutely, I was just trying to avoid using "ownership" in my previous comment because it's more of an abstract concept than the type system and the borrow checker (which have concrete phases in the compiler, typeck and borrowck (though typeck also does more than just enforce linearity (er, affininity?))).

It's definitely not orthogonal. Mutable borrows require affine types.

Maybe not completely orthogonal, but I was thinking specifically of how treatment of immutable borrows show how one could partially tack on borrowing semantics to a non-linear/affine language for at least a modicum of use-after-free protection, and also it's a common misconception that linearity ("ownership") and the borrow checker are synonymous rather than distinct-though-intertwined concepts.

> how one could partially tack on borrowing semantics to a non-linear/affine language

How might that look if you tried to do this in, say a (not compatible with C) C-like language? I thought the ownership system (affine types) was required for the borrow checker to work.

> but significantly weaker

Just curious, could you expand on this? What makes it weaker? Is it that affine types allow either consuming or not consuming a type?

Exactly what you said -- it's not possible to make something that must be used exactly once. See https://gankro.github.io/blah/linear-rust/ for a deeper explanation.

You can't make a type that must be used exactly once, but you can often express that requirement in some other way. One technique is to require that some top-level function returns a value of the terminal type; then you can't accidentally abandon a computation part-way through. Here's a silly example:

https://play.rust-lang.org/?gist=b875377faa6e22b74ba8661ee10...

That little DSL lets you make multi-layer burgers, but only where bacon and patties alternate, and there is a bun on the top.

Reply on news.ycombinator.com