Hacker News Reader

Comment by mafribe | Hacker News Reader

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

View on HN

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

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

Reply on news.ycombinator.com