As you may or may not know, one of the big work items we are focusing on is overhauling our trait system implementation. The main goals are to be more correct and blisteringly fast. =) Oh, and add a bunch of new features. I am on the lookout for people who want to take part in making this happen. My plan is to periodically post announcements in this thread. I’ll also try to keep the roadmap issue up to date. If you don’t see anything, and you’d like to get involved, please do contact me (e.g. via posting in this thread, or privmsg on IRC or Gitter).
In a nutshell, my plan is to achieve three big goals:
Factor out trait operations so we can cache them much more effectively.
Generalize our engine to elegantly handle a wider range of predicates.
For example, our handling of higher-ranked stuff is quite limited, which not only means that associated types don’t work that well, it also blocks fancy features like Associated Type Constructors.
Optimize how we handle trait operations internally, maybe even eventually compiling impls and trait definitions into bytecode and executing trait operations in a VM, similar to the Prolog WAM.
I would like to assist! Any tips on how to prepare? I am not yet experienced with the compiler internals but I find the topic highly interesting. Right now I am reading through all READMEs I can find and try to understand the RFC proposals.
I am interested in persuing this. There are a few annoyances in the current system and it would be great to put things on a more logical foundation.
There should probably be a canonical list of test cases for this project, including many of the higher-ranked trait bound-related issues (I know I have submitted a few) - as well as some other things (I think there are still some problems relating to opt-in built-in traits).
I have a question also - I think you mentioned you were going to do a blog post, but how do lifetimes fit into the whole chalk project? The way I see lifetimes being modelled, is as traits - something like the following:
trait 'a {}
impl<'a> 'a for () {} // and bool, i32, str etc
impl<'a, 'b: 'a, T: 'b> 'a for &'b T {} // and &'b mut T
impl<'a, T: 'a, U: 'a> 'a for T + U {} // all enums
impl<'a, T: 'a, U: 'a> 'a for T * U {} // all structs, tuples etc
Does this look anything like your model/plans for this new improved trait system? Or am I way off?
I am not sure but as I understood the situation, the lifetime problem is treated seperately (in mir) from the trait system and should not be worried about in this context. Right?
Briefly (because this is an extensive topic & I am not as well-educated as Niko or Aaron), a part of the work of chalk is minimizing the interaction between traits and lifetimes. Chalk just returns lifetimes constraints that need to be proven by borrowchecker.
What you've described doesn't really capture all of what borrowck & regionck do. They validate that concrete lifetimes actually have the subtyping relationship we require of them, and that values live for the entirety of lifetimes they are referenced in. Trait implementation can't be analogized to this kind of analysis.
I would like help! As part of my efforts to learn rust, I’ve implemented (and re-re-re-reimplemented) a protocol parser for an existing 3rd party protocol. In my own view, I’ve hit a large number of quirks and corner cases in the current type (and trait) system, which has resulted in a few issue reports on github.
I’m excited about helping if I can. I have a degree in cs, where I’ve been working with languages and machine architecture, among other things. I’m not particularly good at areas closer to formal logic, like logic-based programming, though.
I plan to be posting issues here! Sorry, maybe I jumped the gun in creating the topic, in that I've not had much time to write up the follow-up issues I had planned on posting immediately.
In the interest of not letting the perfect be the enemy of the good, here are a few links that I've gotten started on -- but none of these are (yet) actionable. Will post updates!
Ah but Niko says he wants to handle higher-ranked stuff better as goal #2
Thanks for the link, this is good info. I am interested in how the higher-ranked stuff will be improved... specifically, if I have the following impl:
trait Trait<'a> {}
impl Trait<'static> for () {}
fn hrtb<'a>(_: &'a ()) where for<'b: 'a> (): Trait<'b> {}
The current logic would say -
Skolemize the obligation, this means we obtain something like
(): Trait<'0>, '0: 'a
Match the impl against the skolemized obligation, yielding
'0 == 'static
Check for skolemization leaks
The taint set is {'0, 'static}
This contains 'static, and so fails the leak check
But this is not correct, because if 'a == 'static, then there is only one lifetime that outlives 'a, namely 'static itself. And clearly, (): Trait<'static> - so the function hrtb<'static> should be able to be called.
In fact this does currently fail to compile - probably due to the logic outlined above (though, I may have something wrong of course :).
I don't have a clue what the proposal to fix this logic would be
Ah I see, so much more like "what scope is this variable in" and using type information from functions to establish which scopes need to be inside others - assuming that the bounds have been proven to be valid at an earlier stage.
Sorry for being so absent on this thread! I had hoped this week to fill in a bunch of issues and explanations but somehow didn’t quite get the time to write out my thoughts. Will try to rectify over weekend and/or next week. =)
The short version is that I hope to improve the region constraints, more along the lines of what chalk has, so they can express higher-ranked things and carry around a richer environment (in terms of what we know about lifetimes). Chalk already forms such constraints, but doesn’t solve them right now. Chalk also has a much smarter way of dealing with normalization etc where we can introduce forall-like things at any point and still do normalization, so we don’t have problems around the interaction of associated types and higher-ranked lifetimes (or types).
