Hacker News Reader

Comment by mden | Hacker News Reader

I'm assuming parent is thinking of Rust. And more generally type systems relying heavily on linear types (I believe).

Rust's borrow checker isn't a type system, is it? Sure, its benefits are similar to a linear type system, but actually it's a separate compiler pass whose internals are described imperatively and don't look type-based to me: https://github.com/rust-lang/rust/blob/master/src/librustc_b...

If anything, I agree with zzzcpan and disagree with swsieber. Types are nice but people oversell them. OO languages appeared at the same time as ML family languages, but one got successful and the other got stuck in the realm of "new ideas".

It wouldn't be possible without an affine (at least) type system such as Rust's.

Affine logic rejects contraction, i.e.

     Γ, A, A ⊢ B
    -------------
      Γ, A ⊢ B

My intuition (so take a liberal dose of salt) is that this pretty directly translates to disallowing reuse: we can't see a type twice and continue (inference) as if we saw it once.

Of course, that's very hand-wavy, and doesn't say (as I believe is the case) that there wouldn't be some other way to proceed through a combination of other rules.

Reply on news.ycombinator.com