←back to thread

Tree Borrows

(plf.inf.ethz.ch)
572 points zdw | 2 comments | | HN request time: 0.416s | 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 #
ChadNauseam ◴[] No.44513568[source]
> affine types (what Rust uses)

I'd just like to interject for a moment. What you’re referring to as "affine types", is in fact, Uniqueness Types. The difference has to do with how they interact with unrestricted types. In Rust, these "unrestricted types" are references (which can be used multiple times due to implementing Copy).

Uniqueness types allow functions to place a constraint on the caller ("this argument cannot be aliased when you pass it to me"), but places no restriction on the callee. This is useful for Rust, because (among other reasons) if a value is not aliased you can free it and be sure that you're not leaving behind references to freed data.

Affine types are the opposite - they allow the caller to place a restriction on the callee ("I'm passing you this value, but you may use it at most once"), which is not something possible to express in Rust's type system, because the callee is always free to create a reference from its argument and pass that reference to multiple functions..

replies(2): >>44513701 #>>44514995 #
1. caim ◴[] No.44514995[source]
Yeah, that makes sense. The Rust type system isn't "affine" as in affine logic. Rust allows different forms of contraction, which affine logic strictly prohibits.

And some people like to claim that the Curry-Howard correspondence proves something about their type system, but this is only true for dependently typed languages.

And the proofs aren't about program behavior.

See, https://liamoc.net/forest/loc-000S/index.xml

replies(1): >>44518268 #
2. ralfj ◴[] No.44518268[source]
> Rust allows different forms of contraction, which affine logic strictly prohibits.

That's just wrong. Affine logic totally can have contraction for some propositions.

Also, CH totally exists for non-dependently-typed languages -- for instance, there is a beautiful correspondence between the simply-typed lambda calculus and propositional logic. Please stop repeating claims that you apparently do not understand.