ds-kanren: A subset of the miniKanren language
ds-kanren is an implementation of the miniKanren language.
What's in ds-kanren?
- Try the left and the right and gather solutions that satisfy either one.
- Create a fresh logical variable
- Equate two terms. This will backtrack if we can't unify them in this branch.
- Actually run a logical computation and return results and the constraints on them.
In addition to these core combinators, we also export a few supplimentary tools.
- The opposite of
===, ensure that the left and right never unify.
The Classic Example
We can define the classic
appendo relationship by encoding
lists in the Lisp "bunch-o-pairs" method.
appendo :: Term -> Term -> Term -> Predicate appendo l r o = conde [ program [l === "nil", o === r] , manyFresh $ \h t o -> program [ Pair h t === l , appendo t r o , Pair h o === o ]]
Once we have a relationship, we can run it backwards and forwards as we can with most logic programs.
let l = list ["foo", "bar"]
map fst . runN 1 $ \t -> appendo t l l[nil]
map fst . runN 1 $ \t -> appendo l t l[nil]
map fst . runN 1 $ \t -> appendo l l t[(foo, (bar, (foo, (bar, nil))))]
Some good places to start learning about miniKanren would be
|Versions [RSS]||0.2.0.0, 0.2.0.1|
|Dependencies||base (>=4 && <5), containers (>=0.4), logict [details]|
|Source repo||head: hg clone http://bitbucket.org/jozefg/ds-kanren|
|Uploaded||by jozefg at 2014-10-09T04:15:36Z|
|Downloads||1725 total (12 in the last 30 days)|
|Rating||(no votes yet) [estimated by Bayesian average]|
|Status||Docs uploaded by user
Build status unknown [no reports yet]