An implementation and definition of the Rust trait system using a PROLOG-like logic solver
An implementation and definition of the Rust trait system using a PROLOG-like logic solver
[!WARNING] The Chalk project has been sunset in favor of the newer next-generation trait solver. See the following posts for more details on the development of the new trait solver:
- https://blog.rust-lang.org/inside-rust/2023/07/17/trait-system-refactor-initiative/
- https://blog.rust-lang.org/inside-rust/2023/12/22/trait-system-refactor-initiative/
- https://blog.rust-lang.org/2024/06/26/types-team-update/
- https://blog.rust-lang.org/inside-rust/2024/12/04/trait-system-refactor-initiative/
Chalk is a library that implements the Rust trait system, based on Prolog-ish logic rules.
See the Chalk book for more information.
How does chalk relate to rustc? The plan was to have rustc use the
chalk-solve crate (in this repo) to answer questions about Rust programs, for
example, "Does Vec<u32> implement Debug?". Internally, chalk converts
Rust-specific information into logic and uses a logic engine to find the answer
to the original query. For more details, see
this explanation in the chalk book.
Where does the name come from? chalk is named after Chalkidiki, the area where Aristotle was
born. Since Prolog is a logic programming language, this seemed a
suitable reference.
Here are some blog posts talking about chalk:
There is a repl mainly for debugging purposes which can be run by cargo run. Some basic examples are in libstd.chalk:
$ cargo run
?- load libstd.chalk
?- Vec<Box<i32>>: Clone
Unique; substitution [], lifetime constraints []
If you'd like to contribute, consider joining the Traits Working Group. We hang out on the rust-lang zulip in the #wg-traits stream.
See the contributing chapter in the chalk book for more info.
No open issues yet, or sync has not completed.