3 ms·
I still not get what is the deal here. So I see the types, but not why making them linear is good.
by mamcx 10y ago
I still not get what is the deal here. So I see the types, but not why making them linear is good.
- Ericson2314 10y agoDo you like Rust? Now you kinda 50% Rust.
- yawaramin 10y agoLinear types guarantee at compile time that you can use each value only and exactly once--so no use after free errors, no memory leaks.
- mamcx 10y agoOk, and know that is not possible with normal types and follow the flow?
- tel 10y agoNo, as it turns out in presence of recursion it's undecidable to know that in general. Inference in a linear logic system can answer when it's possible some of the time. Programmer-written annotations can assert it's the case. Type-checkers can ensure that assertions actually hold.
- tel 10y agoThere are lots of programming styles where the programmer must ensure the invariant that some piece of data (value, reference, pointer, whatever) gets used in exactly one sequence. Normal types can ensure that functions and arguments fit together, but they can't talk about how often and when something gets used. Linear types are an extension to normal types which enable them to talk about how often and when something gets used.