Idris 2: Quantitative Type Theory in Practice

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

[ Parent | on HN ]

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.

[ Parent | on HN ]