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.
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
Show replies