6 ms·

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.

deleted 9y ago

[deleted]

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