Re:Idris 2: Quantitative Type Theory in Practice
by paavohtl on Monday January 24, 2022 @02:08AM
(#30054455)
As a practical example Rust uses a less powerful version of linear types called affine types for its ownership system. Values are moved by default in assignments and function calls, and they cannot be used (in their original location) after the move.
[ Parent
| on HN ]
Re:Idris 2: Quantitative Type Theory in Practice
by iopq on Monday January 24, 2022 @04:16AM
(#30055131)
Rust already has the ability to make you use the type at most once, so the useful extension for Rust would be "must-use types" which is an extension of linear types (since linear types would be able to represented in this system easily enough)
It would actually solve a lot of issues in Rust, but unfortunately would be an insane amount of work to introduce because they would invade a lot of the current type system
Re:Idris 2: Quantitative Type Theory in Practice
by paavohtl on Monday January 24, 2022 @05:17AM
(#30055643)
There is the #[must_use] attribute for function return values, which throws compiler warnings when results are unused. It is not a real part of the type system though, but it serves as a useful lint.