A subset implementation of the already small logical language! ds-kanren provides a simple way to write logical relations and queries in Haskell.
The language supports
As a brief demonstration, the classic
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 ]]
Which is just a normal Haskell function mapping 3
Terms to a
Predicate. From here we can run a few different ways
>>> 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))))]
run returns a list of solutions and inequality constraints. The
inequality constraints are things generated from
=/='s. Some of
these might be redundant but none of them will be incorrect.
Some good places to start learning about miniKanren would be
For this implementation in particular, it may be helpful to look at my
blog post explaining