build status

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

  • conde
  • ===
  • =/=

As a brief demonstration, the classic appendo relation.

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
>>> map fst . runN 1 $ \t -> appendo l t l
>>> 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 Logic monad.