The ATS Programming Language
ats-lang.org
ats-lang.org
1) An ML style language.
2) A linear type based imperative language.
On the plus side it has strong theoretical foundations; compiler code base is small enough to be readable; it transpiles to everything and has top notch performance at least for the C target using the second style. The catch is that I would like to write code in the ML style, which requires GC for long running programs (the ATS compiler itself does use the ML style without GC as memory leak is not a concern for a batch mode application). That makes it hard to start small with a library project. The linear type style is high performance but a lot more challenging to use. Xi encourages users to start with ML style and transition into the linear type only when needed.
I have experience doing proofs (group theory in math) using a dependent type prover (Lean). Tooling is really important. Even with excellent type feedback one really needs a lot of automation (like integrated SAT provers) to make the work practical. My feeling about the linear type is the same. We need the proofs to be mostly automated and a lot of nice feedback when the type checkers fail for it to be practical. Though if safety and efficiency are both critical someone may be willing to pay the price now to use linear types. So maybe it will have good applications in the embedded software domain. In my interest area resource usage is only a (small) part of the concern. Even if one roots out all resource bugs one still has logic bugs to deal with so the the availability of and the ease to use well tested libraries are a lot more important than resource management to me.
This has been a really promising language project. If it gets some well-deserved community love maybe it will really blossom.
They're for the previous version of ATS but are still pretty relevant.
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.