Karen: an implementation of microKanren.

Karen.hs

module Karen where

-- https://github.com/seantalts/hasktrip/blob/master/doc/MicroKanren.md
-- http://webyrd.net/scheme-2013/papers/HemannMuKanren2013.pdf
-- https://gup.ub.gu.se/file/207634

data Term
    = Var Int
    | Atom String
    deriving (Eq, Show)

atom :: String -> Term
atom = Atom

type Subst = [(Int, Term)]

prune :: Subst -> Term -> Term
prune s (Var v) =
    case lookup v s of
        Just t  -> prune s t
        Nothing -> Var v
prune s t = t

unify :: Subst -> Term -> Term -> Maybe Subst
unify s t t' = (++ s) <$> go (prune s t) (prune s t')
    where
    go t t' | t == t' = Just []
    go (Var v) t = Just [(v, t)]
    go t (Var v) = Just [(v, t)]
    go t t' = Nothing

type Pred = (Subst, Int) -> [(Subst, Int)]

(===) :: Term -> Term -> Pred
t === t' = \(s, i) ->
    case unify s t t' of
        Just s  -> [(s, i)]
        Nothing -> []

fresh :: (Term -> Pred) -> Pred
fresh f = \(s, i) -> f (Var i) (s, i + 1)

conj :: Pred -> Pred -> Pred
conj p q = \s -> p s >>= q

disj :: Pred -> Pred -> Pred
disj p q = \s -> p s ++ q s

true :: Pred
true = \s -> [s]

false :: Pred
false = \s -> []

solve :: Pred -> [Subst]
solve p = map fst $ p ([], 0)