4 ms·
Another option is affine types that give you "at most once" semantics, in contrast to linear types' "exactly once". If your language has non-termination then af
by mafribe 10y ago
Another option is affine types that give you "at most once" semantics, in contrast to linear types' "exactly once". If your language has non-termination then affine is easier to enforce. (Cf Rust.)
- tupshin 10y agoSure, but rust benefits from must_use annotations, which effectively turn those annotated affine types into linear types. Turns out they are both useful in a very overlapping venn-diagram kind of way.
- mafribe 10y agoHow does this deal with non-termination? Eg. declare x (must_use); P; use(x) (I apologies for the non-Rust-conforming pseudo-code.) The type-checker won't be able to tell if P terminates or not, whence x's use can't be enforced. That's a direct consequence of Rice's theorem (which in turn follows directly form the non-computability of the halting predicate).