5 ms·

Their approach lines up pretty well with how we do regions in Vale. [0] Specifically, we consider the "spine" of a linked list to be its own private "region",

Their approach lines up pretty well with how we do regions in Vale. [0] Specifically, we consider the "spine" of a linked list to be its own private "region", separate from the elements' region. This lets us freeze the spine region, while keeping the elements region mutable. This mechanism is particularly promising because it likely means one can iterate over a collection with zero run-time overhead, without the normal restrictions of a more traditional Rust/Cyclone-like borrow checker. We'll know about this iterating benefit for sure when we finish part 3 (one-way isolation [1]); part 1 landed in the experimental branch only a couple weeks ago [2]. The main difference between the two approaches is that Vale doesn't assume that all elements are self-isolated fields, it allows references between elements and even references to the outside world. However, this does mean that Vale sometimes needs "region annotations", whereas the paper's system doesn't need any annotations at all, and that's a real benefit of their method. Other languages are experimenting with regions too, such as Forty2 [3] and Verona [4] though they're leaning more towards a garbage-collection-based approach, where Vale is more like a memory-safe C++. Pretty exciting time for languages! [0] https://verdagon.dev/blog/zero-cost-borrowing-regions-overview https://verdagon.dev/blog/zero-cost-borrowing-regions-overvi... [1] https://verdagon.dev/blog/zero-cost-borrowing-regions-part-3-one-way-isolation https://verdagon.dev/blog/zero-cost-borrowing-regions-part-3... [2] https://verdagon.dev/blog/regions-prototype https://verdagon.dev/blog/regions-prototype [3] http://forty2.is/ http://forty2.is/ [4] https://github.com/microsoft/verona https://github.com/microsoft/verona

tomas789 3y ago
Honest question. Why many researchers in the area reach for a completely custom language? There is a huge barrier for new language. All the tooling, bindings for OS, tailor made libraries for specific use cases and so on. It all has to be done almost from scratch. Why not to start from what people already know and love and bolt your experiments on top of that? What I do with my DSL AmpLang is to start with Python, throw away parts I don’t like and add the things I’m interested in. It seems to work well enough and my language feels familiar for Python developers. I did not test that but many of existing Python programs would work out of the box in AmpLang. Python grammar is very simple. Even more so for 3.9 which does not have pattern matching.
- justinpombrio 3y ago
  Previous PL researcher here. There are a few reasons for this. First, it's important to distinguish between "positive" features and "negative" features. "Positive" features are where you can do additional things you couldn't do before. I'm guessing your AmpLang is primarily about positive features? Researchers do implement these as libraries or DSLs. For example, the most influential paper in pretty printing is Wadler's pretty printer, which is implemented as combinators in Haskell. However, a lot of research is on "negative" features, where the compiler or type system gives guarantees that certain bad things can't happen. You can't usually add to a language and get negative features. For example, this post's paper is in the "negative" category, so it wouldn't make sense to develop it as a DSL, and furthermore it's about static type systems, so it wouldn't make sense to use anything like Python. Also, existing languages are huge, and when you're doing proofs, you need to fully model the language you're proving things about, so papers would get vastly more complicated if they tried to build on top of an existing language. Instead, the usual approach is to develop a teeny tiny boring language that also has the new feature (in this case, the new type system that handles concurrency). Another thing to realize is that most "languages" in research papers aren't meant to be used. Success for such a language doesn't mean that people start using the little prototype they built (if the language is even implemented); instead success means that someone transfers their ideas into a new or existing language, and builds all of the tooling for that language. The hard problem that the researchers are solving is proving things. This is very hard! Real languages (especially type systems and compilers) are built on top of decades of language research! But it's very different from developing all of the libraries and tooling for a practical language, which is an entirely different process.
- naillo 3y ago
  Probably because they're all compiler geeks and this is a good excuse to learn two birds with one stone
- fweimer 3y ago
  These papers typically contain (semi-)formal descriptions of the type system and various proofs about it. The technical material for this paper is in an appendix: https://www.cs.cornell.edu/andru/papers/gallifrey-types/appendix.pdf https://www.cs.cornell.edu/andru/papers/gallifrey-types/appe... For real-world languages, this is even more involved, and existing formalizations only cover supposedly distinct sub-languages, not the full language (with the risk being that there are unexpected interactions). Most languages also have complicated things like higher-order functions or some form of polymorphism, and the new type system would have to be integrated with that.
Pabloski80 3y ago
Hmm, those regions sound much like a construct from Cyclone language.

tomas789 3y ago

Honest question. Why many researchers in the area reach for a completely custom language? There is a huge barrier for new language. All the tooling, bindings for OS, tailor made libraries for specific use cases and so on. It all has to be done almost from scratch. Why not to start from what people already know and love and bolt your experiments on top of that? What I do with my DSL AmpLang is to start with Python, throw away parts I don’t like and add the things I’m interested in. It seems to work well enough and my language feels familiar for Python developers. I did not test that but many of existing Python programs would work out of the box in AmpLang. Python grammar is very simple. Even more so for 3.9 which does not have pattern matching.

justinpombrio 3y ago
Previous PL researcher here. There are a few reasons for this. First, it's important to distinguish between "positive" features and "negative" features. "Positive" features are where you can do additional things you couldn't do before. I'm guessing your AmpLang is primarily about positive features? Researchers do implement these as libraries or DSLs. For example, the most influential paper in pretty printing is Wadler's pretty printer, which is implemented as combinators in Haskell. However, a lot of research is on "negative" features, where the compiler or type system gives guarantees that certain bad things can't happen. You can't usually add to a language and get negative features. For example, this post's paper is in the "negative" category, so it wouldn't make sense to develop it as a DSL, and furthermore it's about static type systems, so it wouldn't make sense to use anything like Python. Also, existing languages are huge, and when you're doing proofs, you need to fully model the language you're proving things about, so papers would get vastly more complicated if they tried to build on top of an existing language. Instead, the usual approach is to develop a teeny tiny boring language that also has the new feature (in this case, the new type system that handles concurrency). Another thing to realize is that most "languages" in research papers aren't meant to be used. Success for such a language doesn't mean that people start using the little prototype they built (if the language is even implemented); instead success means that someone transfers their ideas into a new or existing language, and builds all of the tooling for that language. The hard problem that the researchers are solving is proving things. This is very hard! Real languages (especially type systems and compilers) are built on top of decades of language research! But it's very different from developing all of the libraries and tooling for a practical language, which is an entirely different process.
naillo 3y ago
Probably because they're all compiler geeks and this is a good excuse to learn two birds with one stone
fweimer 3y ago
These papers typically contain (semi-)formal descriptions of the type system and various proofs about it. The technical material for this paper is in an appendix: https://www.cs.cornell.edu/andru/papers/gallifrey-types/appendix.pdf https://www.cs.cornell.edu/andru/papers/gallifrey-types/appe... For real-world languages, this is even more involved, and existing formalizations only cover supposedly distinct sub-languages, not the full language (with the risk being that there are unexpected interactions). Most languages also have complicated things like higher-order functions or some form of polymorphism, and the new type system would have to be integrated with that.

Pabloski80 3y ago

Hmm, those regions sound much like a construct from Cyclone language.