Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

[WIP] Initial draft of engine book #326

Merged
merged 8 commits into from
Mar 2, 2020

Conversation

jackh726
Copy link
Member

@jackh726 jackh726 commented Feb 7, 2020

No description provided.

book/src/engine/logic.md Outdated Show resolved Hide resolved
Copy link

@jonas-schievink jonas-schievink left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Great docs! Thanks for writing this up.

book/src/engine/logic.md Outdated Show resolved Hide resolved
book/src/engine/major_concepts.md Outdated Show resolved Hide resolved
book/src/engine/major_concepts.md Outdated Show resolved Hide resolved
book/src/engine/major_concepts.md Outdated Show resolved Hide resolved
Copy link
Contributor

@nikomatsakis nikomatsakis left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This is awesome. I included some thoughts below but in my opinion you should feel free to merge when you feel ready.

book/src/engine/logic.md Outdated Show resolved Hide resolved
book/src/engine.md Show resolved Hide resolved

## Overview

`chalk-engine` solves a `Goal` using a depth-first search. When asked to solve a
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This isn't strictly true. We don't use depth-first search. If we did, we would always fully explore one strand before starting on another. The docs I wrote before claimed we use a breadth-first search but this isn't really true either. I'm actually not sure if our current search algorithm can be cleanly characterized. It's one of the things I've been wondering about -- we might want to think about how to specify the behavior more rigorously. The kind of "disconnected" way that our current solver works makes it a bit less obvious to me how to do that.

The minikanren algorithm is quite interesting in that (by the nature of its design) winds up spending a lot more time traversing and working with answers that have "gotten farther" in the process than it does with those that haven't. Or at least so it was explained to me. To be honest, I have to kind of review how it works, and maybe it'd be good for us to spend some time trying to characterize and work through how our own solver would behave.

Anyway for now let's just not say depth-first search, since to me that suggests something very specific (prolog-style solving) which is not the case. Maybe something like "using a hybrid search strategy with elements of depth- and breadth-first search"?

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yeah, true, it's not depth- or breadth-first. It would be good to characterize exactly what we do, but I think that will be more useful when we have benches and can check how different search schemes perform.

book/src/engine/logic.md Outdated Show resolved Hide resolved
book/src/engine/logic.md Show resolved Hide resolved
book/src/engine/logic.md Show resolved Hide resolved
On the other hand, `Context::Goal` represents an opaque goal generated
externally. As such, it may contain any extra information or may be interned.
When solving a logic predicate, Chalk will lazily convert `Context::Goal`s
into `HHGoal`s.
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I intend to add some chapters to the type section describing the sorts of goals that appear in our logic etc in a more "semantic way", so maybe we should link over there eventually I guess.

Copy link
Contributor

@nikomatsakis nikomatsakis left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'm happy to merge as is and update as we go

@jackh726
Copy link
Member Author

jackh726 commented Mar 2, 2020

I'm happy to merge as is and update as we go

Works for me

@nikomatsakis nikomatsakis merged commit 177d713 into rust-lang:master Mar 2, 2020
@jackh726 jackh726 deleted the engine_book branch March 2, 2020 21:12
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

4 participants