6 ms·

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 fo

by clord 9y ago

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.

moosingin3space 9y ago
Rust uses a similar (but significantly weaker) system called "affine types" underlying its borrow checker.
- deleted 9y ago
  [deleted]
- mjhoy 9y ago
  > 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?
  - moosingin3space 9y ago
    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/ https://gankro.github.io/blah/linear-rust/ for a deeper explanation.
    - deleted 9y ago
      [deleted]
    - twic 9y ago
      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=b875377faa6e22b74ba8661ee106d13d&version=stable 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.
- kibwen 9y ago
  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).
  - moosingin3space 9y ago
    Would it be correct to say that the affine type system underlies the ownership paradigm?
    - kibwen 9y ago
      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?))).
  - cwzwarich 9y ago
    It's definitely not orthogonal. Mutable borrows require affine types.
    - kibwen 9y ago
      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.
      - moosingin3space 9y ago
        > 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.
masklinn 9y ago
> 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.
- clord 9y ago
  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.
  - masklinn 9y ago
    > 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.
  - OJFord 9y ago
    > 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 https://en.wikipedia.org/wiki/Substructural_type_system [1]: https://en.wikipedia.org/wiki/Idempotency_of_entailment https://en.wikipedia.org/wiki/Idempotency_of_entailment [2]: https://en.wikipedia.org/wiki/Monotonicity_of_entailment https://en.wikipedia.org/wiki/Monotonicity_of_entailment
- mcguire 9y ago

by clord 9y ago

moosingin3space 9y ago

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

deleted 9y ago
[deleted]
mjhoy 9y ago
> 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?
- moosingin3space 9y ago
  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/ https://gankro.github.io/blah/linear-rust/ for a deeper explanation.
  - deleted 9y ago
    [deleted]
  - twic 9y ago
    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=b875377faa6e22b74ba8661ee106d13d&version=stable 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.
kibwen 9y ago
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).
- moosingin3space 9y ago
  Would it be correct to say that the affine type system underlies the ownership paradigm?
  - kibwen 9y ago
    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?))).
- cwzwarich 9y ago
  It's definitely not orthogonal. Mutable borrows require affine types.
  - kibwen 9y ago
    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.
    - moosingin3space 9y ago
      > 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.

masklinn 9y ago

> 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.

clord 9y ago
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.
- masklinn 9y ago
  > 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.
- OJFord 9y ago
  > 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 https://en.wikipedia.org/wiki/Substructural_type_system [1]: https://en.wikipedia.org/wiki/Idempotency_of_entailment https://en.wikipedia.org/wiki/Idempotency_of_entailment [2]: https://en.wikipedia.org/wiki/Monotonicity_of_entailment https://en.wikipedia.org/wiki/Monotonicity_of_entailment
mcguire 9y ago