3 ms·

I can only speak as a user of linear types, not as a type theorist. They are extremely useful in practice. In ATS they enable not just tracking memory but any f

by doublec 11y ago

I can only speak as a user of linear types, not as a type theorist. They are extremely useful in practice. In ATS they enable not just tracking memory but any form of resource that needs to be cleaned up. If you fail to do so you get a compile time error. 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.

chenglou 11y ago
Is manual resource management with linear types a must? Because that's a big bummer. Also how is that compare to Rust? If it's not, is it possible to incorporate it into an existing language with e.g. HM types?
- theseoafs 11y ago
  > Is manual resource management with linear types a must? Because that's a big bummer. 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.
sgrove 11y ago
How do linear types help in distributed systems - you mention sharing (or not sharing) between threads, but I'm also intensely curious re: reasoning about heterogeneous networks. Some rambling questions you might be able to shed some light on - 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.
- doublec 11y ago
  I've not had to do anything distributed with ATS that involved sharing data. I mostly used zeromq to send information around and controlled access to resources via processes. 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.

by doublec 11y ago

chenglou 11y ago

Is manual resource management with linear types a must? Because that's a big bummer. Also how is that compare to Rust? If it's not, is it possible to incorporate it into an existing language with e.g. HM types?

theseoafs 11y ago
> Is manual resource management with linear types a must? Because that's a big bummer. 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.

sgrove 11y ago

How do linear types help in distributed systems - you mention sharing (or not sharing) between threads, but I'm also intensely curious re: reasoning about heterogeneous networks. Some rambling questions you might be able to shed some light on - 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.

doublec 11y ago
I've not had to do anything distributed with ATS that involved sharing data. I mostly used zeromq to send information around and controlled access to resources via processes. 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.