-
Notifications
You must be signed in to change notification settings - Fork 124
Search customization & instrumentation
Currently if you want search different from miniKanren search, you're out of luck. Jamie Brandon has done some work to make this more flexible but I think we can take it a step further.
The key insight is that search is completely driven by data structures. The problem is that what data structures we produce is hard coded to a particular type, Substitution
. Instead Substitution
should contain a new field, call it st
for "strategy" which is an ISearch
(a protocol) instance. We could imagine that ISearch
looks something like the following:
(defprotocol ISearch
(conjunct [_])
(disjunct [_])
(commit [_])
(cut [_]))
We should of course be skeptical of commit
and cut
, perhaps better to put those in a separate protocol.
(defprotocl IMKSearch
(commit [_])
(cut [_]))
Eventually we should see if these could be constructed on lower level primitives such as described in Search Combinators.
Going down this route would also free us to experiment with instrumenting search for debugging, performance analysis, etc. This could be done cleanly without mucking around with the basic search behavior.
The main thing to be concerned with here is degrading search perfomance, but seeing as it's only one more inline protocol dispatch I'm pretty confident that this can perform well.
We will leave ITake
mostly alone for now. We want search to be completely pluggable - so we should remove the monadic terminology entirely from the concrete types. IConjunct
, IDisjunct
and -conjuct
, -disjunct
might be better names for the protocols. For now it's probably ok if we just implement IMKPrune
which will require -commit
and -cut
. This means that every data structure involved will need to have search information. This means that we probably need a real failure type Fail
. But that also opens the door for a search strategy which does not discard failures.
Fail
would contain the failed substitution.
I believe it's enough if the substitution has strategy which is delegated to - this strategy will return data structures Choice
, Fail
which themselves will implement the search protocols. One question is thunks. Perhaps we should return these as Step
.
Then say we want to debug failures. We would create a search strategy which does not eliminate them.
(-conjuct a-failure g)
a-failure
would have a substitution which has the strategy, and this strategy would simply pass the failure along. The implementation for Fail
might look something like this:
(-conjunct (:st a-failure) a-failure)
This way people can reuse Fail
. The story is similar for Choice
and Step
. This does mean the instance of the search protocols looks like something like the following:
(deftype MKSearch []
IConjunct
(-conjuct [_ x]
(cond
(fail? x) ...
(unit? x) ...
(step? x) ...
(choice? x) ...)))
The approach which is more verbose, but perhaps a bit more flexible / efficient is just for each search strategy to always provide its own types. miniKanren search would involve a very small number of types and implementations so perhaps it not a big deal.
Also looking again at Search Combinators, the paper does seem a bit more relevant for the CLP(FD) portion of cKanren. For better or worse we're pretty married to the Prolog w/ rich constarints approach