←back to thread

Tree Borrows

(plf.inf.ethz.ch)
565 points zdw | 1 comments | | HN request time: 0s | source
Show context
fuhsnn ◴[] No.44512042[source]
I wonder if Rust or future PL would evolve into allowing multiple borrow checker implementations with varying characteristics (compile speed, runtime speed, algorithm flexibility, etc.) that projects can choose from.
replies(9): >>44512293 #>>44512361 #>>44512426 #>>44512597 #>>44512841 #>>44513554 #>>44513949 #>>44516880 #>>44516995 #
pjmlp ◴[] No.44512426[source]
We already have that by having multiple approaches via affine types (what Rust uses), linear types, effects, dependent types, formal proofs.

All have different costs and capabilities across implementation, performance and developer experience.

Then we have what everyone else besides Rust is actually going for, the productivity of automatic resource management (regardless of how), coupled with one of the type systems above, only for performance critical code paths.

replies(2): >>44512504 #>>44513568 #
1. LelouBil ◴[] No.44512504{3}[source]
I would love some sort of affine types in languages like Kotlin, it just makes cleaner code organization in my opinion.

Doesn't matter if it's purely "syntaxical" because the language is garbage collected, just the fact of specifying what owns what and be explicit about multiple references is great imo.

Some sort of effects systems can already be simulated with Kotlin features too.

Programming language theory is so interesting!