Oh man, this blog post is great and I sincerely hope they succeed in bringing these enhancements to Rust's type system. Yes, Rust is already a lot, but on the occasion that I have use for the things covered here, they're incredibly helpful. Having worked on embedded systems with MTBF of 10 years, writing panic-free Rust is not particularly easy (mostly because of all the places you forget can panic, like addition). The refinement types would be really helpful for building complex datastructures on top of plain arrays.
Oh wow, very good timing, I've been working on a very similar post for the upcoming blog carnival (albeit with dependent instead of refinement types).
On substructural types: don't forget uniqueness types! Unique references in a concurrent setting give you the particularly nice guarantee that you can treat data in a single-threaded manner, without fear of data races (see the paper Data Race Freedom à la Mode from the OxCaml team).
As a long-time rust user and big fan of the language, the possibility of adding this kind of complex type theory stuff to the language worries me.
Yes, I'm well aware that Rust's foundations are heavily based on functional programming and pulls a lot of inspiration from languages like Haskell and Ocaml. But in my opinion, Rust has done a great job of folding these technical and academic concepts into simple and intuitive language-level constructs. You don't have to think about monads or applicative functors to get value out of the patterns and concepts they provide.
The article points out that Rust already has function colors, but they're very much tied to real implications tied to how a function is executed rather than just enforcing some kind of additional constraints on what you can do in it. Maybe there's a way to introduce some of these things in a way where it's opt-in and doesn't leak out of the places it's explicitly used, but that seems very difficult.
For the record, I definitely see the value in these kinds of additions and would probably end up making use of some of them myself. However, I feel like it's yet another step in increasing Rust's complexity and making it less approachable for "average" software developers.
The baseline cost of learning the ownership/borrowing system is already high, and then learning the async ecosystem with all of its quirks and footguns is very hard as well. Forcing Rust devs to reason about effect systems and complex meta type-level stuff in addition to all that and the actual application logic itself seems like a great way to send Rust the way of other niche academic languages which are rarely used outside of enthusiast or hobbyist circles.
As a bit of a meta note here, I realized while writing that this article is exactly the kind of thing that would get me really excited and interested in the past. Maybe it's just my sharply growing cynicism for everything in software and tech over the past several years, or maybe it's just the natural progression of a wide-eyed and eager young dev getting older.
Quippy responses like these are perhaps better suited to Reddit/HN than to Lobste.rs? It would've been a different thing had you written "For folks interested in playing with these kinds of features, highly recommend checking out ATS2 <elaboration>"
If any of the stated features were added to Rust, there's an implicit expectation that the overall usability of the language (e.g. the famed error messages) should not degrade as much as possible. No such expectation exists for research languages like ATS2.
You are right… much better framing. Yes, you can test out there these features yesterday in a language that compiles to C—so equally as “low-level”. I know I learn a lot getting something to compile with these sort of type-level features.
I'm not familiar with AST2, but most languages which are proclaimed to be "equally low level" to C are not actually close once you examine their hooks into hardware intrinsics and type attributes, including even Rust.
was going to say, ATS lets you do all this, but with really bad ergonomics. would be awesome to see these things on a language like rust or ocaml, which have had a lot more work put into developer experience.
ngp | 6 hours ago
Oh man, this blog post is great and I sincerely hope they succeed in bringing these enhancements to Rust's type system. Yes, Rust is already a lot, but on the occasion that I have use for the things covered here, they're incredibly helpful. Having worked on embedded systems with MTBF of 10 years, writing panic-free Rust is not particularly easy (mostly because of all the places you forget can panic, like addition). The refinement types would be really helpful for building complex datastructures on top of plain arrays.
jjw | 11 hours ago
Oh wow, very good timing, I've been working on a very similar post for the upcoming blog carnival (albeit with dependent instead of refinement types).
On substructural types: don't forget uniqueness types! Unique references in a concurrent setting give you the particularly nice guarantee that you can treat data in a single-threaded manner, without fear of data races (see the paper Data Race Freedom à la Mode from the OxCaml team).
aldantanneo | 11 hours ago
How are uniqueness types different from what's already provided by ownership and the borrow checker? Genuinely asking
Halkcyon | 8 hours ago
Yeah, if you make everything
&mut, there's your uniqueness right there.ngp | 6 hours ago
Or just an owned
Box<T>? If you splatter&muts everywhere you'll have some pretty gnarly lifetimes to deal with.Ameo | 38 minutes ago
As a long-time rust user and big fan of the language, the possibility of adding this kind of complex type theory stuff to the language worries me.
Yes, I'm well aware that Rust's foundations are heavily based on functional programming and pulls a lot of inspiration from languages like Haskell and Ocaml. But in my opinion, Rust has done a great job of folding these technical and academic concepts into simple and intuitive language-level constructs. You don't have to think about monads or applicative functors to get value out of the patterns and concepts they provide.
The article points out that Rust already has function colors, but they're very much tied to real implications tied to how a function is executed rather than just enforcing some kind of additional constraints on what you can do in it. Maybe there's a way to introduce some of these things in a way where it's opt-in and doesn't leak out of the places it's explicitly used, but that seems very difficult.
For the record, I definitely see the value in these kinds of additions and would probably end up making use of some of them myself. However, I feel like it's yet another step in increasing Rust's complexity and making it less approachable for "average" software developers.
The baseline cost of learning the ownership/borrowing system is already high, and then learning the async ecosystem with all of its quirks and footguns is very hard as well. Forcing Rust devs to reason about effect systems and complex meta type-level stuff in addition to all that and the actual application logic itself seems like a great way to send Rust the way of other niche academic languages which are rarely used outside of enthusiast or hobbyist circles.
As a bit of a meta note here, I realized while writing that this article is exactly the kind of thing that would get me really excited and interested in the past. Maybe it's just my sharply growing cynicism for everything in software and tech over the past several years, or maybe it's just the natural progression of a wide-eyed and eager young dev getting older.
gignico | 7 hours ago
What's the status of the work on pattern types? The post mentions they are "experimenting" with them. Are they on track for stabilization?
toastal | 17 hours ago
You could do these in ATS2 for a decade :)
typesanitizer | 17 hours ago
Quippy responses like these are perhaps better suited to Reddit/HN than to Lobste.rs? It would've been a different thing had you written "For folks interested in playing with these kinds of features, highly recommend checking out ATS2 <elaboration>"
If any of the stated features were added to Rust, there's an implicit expectation that the overall usability of the language (e.g. the famed error messages) should not degrade as much as possible. No such expectation exists for research languages like ATS2.
toastal | 13 hours ago
You are right… much better framing. Yes, you can test out there these features yesterday in a language that compiles to C—so equally as “low-level”. I know I learn a lot getting something to compile with these sort of type-level features.
Lilian | 37 minutes ago
I'm not familiar with AST2, but most languages which are proclaimed to be "equally low level" to C are not actually close once you examine their hooks into hardware intrinsics and type attributes, including even Rust.
zem | 2 hours ago
was going to say, ATS lets you do all this, but with really bad ergonomics. would be awesome to see these things on a language like rust or ocaml, which have had a lot more work put into developer experience.