chalk

Chalk is a library that implements the Rust trait system, based on Prolog-ish logic rules.

See the Chalk book for more information.

FAQ

How does chalk relate to rustc? The plan is 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.

Blog posts

Here are some blog posts talking about chalk:

• Lowering Rust Traits to Logic

• Explains the basic concepts at play
• Unification in Chalk, Part 1

• An introduction to unification
• Unification in Chalk, Part 2

• Extending the system for associated types
• Negative reasoning in Chalk

• How to prove that something is not true
• Query structure in chalk

• The basic chalk query structure, with pointers into the chalk implementation
• Cyclic queries in chalk

• Handling cyclic relations and enabling the implementation of implied bounds and other long-desired features in an elegant way

REPL

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 []

Contributing

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.