Amateur question: how are linear types in "practice"? How much of concurrency do they solve? And how are they different from modern HM types?
Sorry for being vague. I'm interested in this subject but layman materials on it are hard to come by.
Sorry for being vague. I'm interested in this subject but layman materials on it are hard to come by.
This removes much of the burden of wondering if you got the resource management right. Especially when maintaining existing applications. If you refactor things the compiler tells you when you got it wrong.
There is overhead since you are managing resource manually - both syntax-wise and mental though.
For concurrency they enable 'solving' shared state by making it difficult to share state. You really have to pass ownership of the resource to the other thread so it can no longer be accessed anywhere else.
If it's not, is it possible to incorporate it into an existing language with e.g. HM types?
Manual resource management is generally a given in functional languages with linear types. Since your types are linear, you need functions which can destroy your linear types, and generally those functions are called manually. There are certain other approaches you could adopt in a new language -- e.g. you could use C++-like "destructors" where if you don't do anything with a value and it falls out of scope, a function to dispose of the value automatically gets called. I haven't seen that implemented in a functional language with linear types, though. I don't know how well it would play with type inference. Generally, though, linearly typed languages don't worry about this.
> Also how is that compare to Rust?
Rust doesn't have linear types -- Rust has unique/affine types. An affine value can be used 0 or 1 times (unlike linear values which can only be used exactly 1 time). So in Rust it's possible to "lose" a value by throwing it away or by creating an RC cycle and leaking it. A linear type system wouldn't let you do that. However, Rust does have those automatic destructors which keep you from having to destroy everything manually.
> If it's not, is it possible to incorporate it into an existing language with e.g. HM types?
HM in and of itself knows nothing about linearity and so you need additional support from the typechecker to implement it. Plenty of languages have extended HM to include linearity, though.
1. How much of a (self-contained vs distributed) system has to be completely written in ATS? 2. How much of the emergent system can be modeled in ATS to take advantage of linear types while letting some other team(s) work in e.g. nodejs 3. What's the onboarding experience like for a dev new to typed systems entirely? How long before they generally grasp the abstract concepts and how to express them? Are there any particularly difficult pieces?
Thanks a ton for sharing your experience! Like Chenglou, I'm very curious about linear logic/session-types/etc., but very new to the domain.
It's a fairly steep learning curve for people new to types. Given exposure to SML it's not too hard to just use that side of things plus linear types. Dependent types and proofs add complexity but hopefully you can avoid it while learning.