Are there any projects that are trying to make application-level languages with borrow checkers?
10
3
37
Conversation
Idris 2 and GHC Haskell
2
5
These track linearity, but isn't there a bunch more if you want borrow checking? Like the fractional permission style stuff the borrow checker does goes far beyond linearity IIUC.
1
2
I can't think of anything, but it is Monday morning. Do you have any specifics?
1
Can you model the mutable / immutable borrow stuff with just linear types? Not sure
1
Like, I'm thinking of stuff like how you can lend out a local immutable reference to an owned binding in a scope, which prevents you altering the owned binding. Or stuff like partial borrows, etc.
1
Linear types can model the ownership stuff I think - although it's a bit awkward - ie. I think you need to use CPS to make it work. It's a bit more natural with uniqueness types though (like in Clean).
1
1
Yeah Haskell uses CPS for their mutability with linear types
1
Dunno if you've seen “Oxide: The Essence of Rust” by et. al.? arxiv.org/pdf/1903.00982 - I think it has a good, precise description of things Rust's borrow checker supports, but I admittedly have not got around to sitting down to read it deeply yet. 😅
2
1
I think Section 2 is relevant to this? Compares it to the work on linear logic I think.
6.2 also brings up another kind of feature of the borrow checker, but between that and section 2, I think that should be all of the "borrow checking" functionality.
1