Introduction or explanation at all?

[Phlosioneer]

I know this is supposed to be more-or-less a typesystem for rust.
I know this is a Prolog-like language.
I know how to use Prolog decently well.
I want to help.
I especially want to help write documentation.

But:

• There's no documentation on how to use the command line interface. No help command or anything.
• The --help option mentions a .chalk file, but there's no explanation anywhere of how that file is formatted, what it contains, or anything.
• There's no example .chalk files anywhere.
• There's no way I can tell to generate .chalk files from rust code or anything like that.
• The rustdoc doesn't mention any of this.
• The main binary file (bin/chalki.rs) has no comments, so I can't tell where the real work is done, so I have no idea where to look for hints or comments about the command-line-interface / contents of .chalk files.

Could someone give me some pointers, maybe a quick summary of what this project does and how to use it? I can totally start documenting this stuff, it looks really cool, I just need a place to start.

[Phlosioneer]

Oh, I've found libstd.chalk. It's a start, I guess, but some answers to the above would still save me a lot of time and print statements.

[tweerwag]

chalk implements the trait system of Rust in a different (and cleaner?) way than the Rust compiler itself. Since it is a complex and non-trivial part of the compiler, it is good to have a separate "reference" implementation.

A .chalk file is a stripped down version of Rust code where only types, traits and impls are declared (without actual code). Given the .chalk file, chalk can answer questions about the program like "does this type implement this trait" or "does this parameterized type implement this trait for each possible parameter" et cetera. The complete grammar can be found in the .lalrpop file in this repository. (Sorry, I am typing this on my phone so can't easily lookup the exact name.)

Another use case for chalk is to be able to test how certain additions (higher kinded types, etc) to the type system impact the whole system. It is probably much easier to implement experimental changes here, than in the Rust compiler. And hence, weird edge cases, inconsistencies, etc can be found earlier.

I think it is a good idea to have a tool which extracts a .chalk file from an actual Rust source file. However, no such tool exists at the moment as far as I know.

Hopefully, I can take a look on my computer this evening to give you more pointers.

[Phlosioneer]

Alright, awesome! I'll take a look at the .lalrpop file (that extension is a mouth-full XD). I've already put up a PR for the first file I tackled, bin/chalki.rs. Feedback is welcome!

The one major thing I don't understand yet is how to specify parameterized types as goals. Normally for something like prolog, I can type in property(1, 6, A, B) and it'll spit out all values of A and B that make the statement true. I tried to do that here with Vec<Box<T>>: Clone, and it tells me "Invalid type name T". That makes sense, but what placeholder can I use so that it spits out a list of possible types for T?

If I understand the format correctly, generating a .chalk file shouldn't be TOO hard... at least, a naive approach will get pretty close.

• Any enum gets copied over completely.
• Any global or default trait function is stripped of parameter names and function body.
• Any trait function is stripped of parameter names.
• Any struct has its field names stripped.
• Any trait impl is stripped of functions (leaving associated types intact)
• No idea how to deal with macros.

That might be a fun project eventually. Documentation and user-friendliness is my prime concern, though. Let's see if we can get more than just 11 contributors!

[tweerwag]

Prolog implicitly places quantifiers around your statements (universal ones around rules and existential ones around questions). In chalk you need to explicitly specify them. For example,

?- exists<T> { Vec<u32> = Vec<T> }
Unique; substitution [?0 := u32], lifetime constraints []

Note that although Prolog normally tries to find all possible solutions, chalk tries to find a unique solution. I am not sure about this, but I think chalk never finds a non-unique solution. This is by design, since the compiler doesn't just choose a possible type, but errors if there are multiple solutions.

You can find a lot of examples in src/solve/test/mod.rs.

[fabric-and-ink]

Well I think Nico's blog posts which are linked in the Readme are a good start. I work on a glossary of important terms. So I would not say there is nothing, it is just a bit scattered. After I finish the next iteration of the glossary I will start a "book" where everything will be gathered. It's a young crate so there is a lot to do. And I'm slow because I am overworked. But that is another thing :)

[Phlosioneer]

Thanks for your help. I think I've got a hang of this now, and am working on more documentation, which I'll be pushing to my PR in the next few days.