---

As you may have known I have been working on some Mercury-related things recently, and from this I somewhat regained my interests in miniKanren. I've followed through the microKanren paper 8 years ago, but back then I didn't really understand why things are how things are, and if you ask sophomore-year me to implement that in other languages I probably wouldn't have much of an idea.

Now, it's different.

You see, for some reasons, the idea of reading about Sokuza Kanren never came across my mind; maybe it's because I dismissed it thinking it's a more complex variant simply because it did not have a simple-sounding name (I have been wondering which Japanese word is spelled like that for years). As it turns out I was very wrong, and Sokuza Kanren is probably easier to understand than microKanren.

The problem with microKanren, at least from my perspective, is probably how it's presented in the original paper. I think it's okay as a paper (although I really have no credentials to judge whether a paper is good or bad whatsoever) but it's just a bit too hard to go through. Many miniKanren variants, including microKanren, are implemented in Scheme, and often lay into the specific idiosyncrasies of the language. This, in my personal experiences, can and has muddle things; are things done this specific way because that's how Kanren works or is it because that how Scheme works? Without actually knowing which is which, you can't reasonably derive from what you have. Sokuza Kanren is a bit better at this in my opinion since it tells you the big idea up front.

After following through Sokuza Kanren and implemented it in both Haskell and Golang, I think I've pretty much got the very essense of miniKanren-like languages:

1. A term is either:
   • A variable;
   • A scalar value;
   • A functor, which has a head and a list of terms as its arguments.
2. A subst is a mapping from variables to terms.
3. A state is technically a subst with a gensym. The gensym is used to generate names for intermediate variables.
4. A program consists of goals, which itself can be composed of many smaller goals.
5. A single subst is a single potential answer to a goal. The program does its thing by trying to calculate the subst that satisfies all the specified goals within the program.
6. A goal is something that transforms a state into a collection of zero to possibly infinitely many states, namely:
   • When the goal fails, it generate zero states;
   • When the goal succeeds with only one possible answer, it generates one state;
   • When the goal succeeds with more than one possible answers, it generates more than one states.
7. Naturally:
   • The states generated by a disjunction of two goals is the union of the states generated by the two subgoals.
     • How you perform this union operation determines your search strategy. If you suspend and interleave them (like how it's described in the microKanren paper), you get breadth-first search; if you don't suspend and concatenate them in order, you get depth-first search.
   • The states generated by a conjunction of two goals are the states generated by the second subgoal from the states generated by the first subgoal.
8. A subst, as it is a mapping, can be extended.
9. Unification is the core mechanism of computation; it matches two terms against each other and extends the "current" subst accordingly.
   • A variable matches with anything;
   • A scalar value only matches with itself or another variable;
   • A functor only matches with another functor with the same hed and the same amount of arguments; the arguments of the functors also need to match with their corresponding ones as well.
10. To execute a goal is to simply run it against the empty state.

The rest of the problem is simply to decide how to manage these things. After understanding how things fit together I have the following minor complaints:

• The use of words like mzero, mplus and bind (and their use in conj and disj).
  • These obviously comes from the fact that both lists and streams are monads, but I find it much more easier to just say how things are done in this case especially when you're teaching yourself. One can have a taste of abstractions when they need it.
• The use of higher-order abstract syntax for call/fresh;
  • By using HOAS you don't have to worry about naming your logic variables. If you do it first-order then you'll have to worry about name clashing. Sokuza Kanren removes this problem in a (for a lack of better word) sneaky manner while staying first-order. I, however, have to do it explicitly. I don't really feel that bad about doing it explicitly, since it seems like it's how other people did it as well.
• The use of eta-expansion, which is required in Scheme to suspend the (normally eager) evaluation;
  • Which seems to be only needed when you implement goals as higher-order functions and your language is call-by-value.

Another big problem is to try to implement such a language in a host language that does not support first-class functions, since its Scheme implementation makes heavy uses of this feature. I doubt there's another way other than defunctionalize manually, which is what I've done in the Golang version. With manually-implemented vtables, I suppose one can rewrite the Golang code into C relatively easily albeit at the cost of having barely any readability when compared with the Haskell version or theoriginal Scheme version.

The full code of my implementations can be found at https://github.com/bctnry/minamoto-kanren .

data Term = Var String | Value String | Functor String [Term] deriving (Eq, Show)
type Subst = [(String, Term)]
type State = (Subst, Integer)
type Goal = State -> [State]

falsify :: Goal
falsify _ = []

succeed :: Goal
succeed x = [x]

disj :: Goal -> Goal -> Goal
disj x y = \s-> (x s) ++ (y s)

conj :: Goal -> Goal -> Goal
conj x y =
  \s -> case map y (x s) of
    [] -> []
    t -> foldl1 (++) t

emptySubst :: Subst
emptySubst = []

emptyState :: State
emptyState = (emptySubst, 0)

extendSubst :: (String, Term) -> Subst -> Subst
extendSubst (k, v) s = (k, v):s

lookupSubst :: Term -> Subst -> Maybe Term
lookupSubst t s =
  case t of
    Value _ -> Just t
    Functor _ _ -> Just t
    Var k ->
      case s of
        [] -> Nothing
        (kk,vv):res -> if k == kk then Just vv else lookupSubst t res
     
fresh :: State -> (Term, State)
fresh (s, k) = (Var ("V_" ++ show k), (s, k + 1))

unify :: Term -> Term -> Subst -> Maybe Subst
unify t1 t2 s = if t1Res == t2Res then Just s else unify' t1Res t2Res s
  where
    t1Res = ofs t1 $ lookupSubst t1 s
    t2Res = ofs t2 $ lookupSubst t2 s
    ofs t Nothing = t
    ofs _ (Just t) = t

unify' :: Term -> Term -> Subst -> Maybe Subst
unify' (Value v) (Value v2) s = if v == v2 then Just s else Nothing
unify' (Var k) v s = Just $ extendSubst (k, v) s
unify' v (Var k) s = Just $ extendSubst (k, v) s
unify' (Functor f1 arglst1) (Functor f2 arglst2) s =
  if f1 /= f2 then Nothing
  else if length arglst1 /= length arglst2 then Nothing
  else unify'' arglst1 arglst2 s

unify'' :: [Term] -> [Term] -> Subst -> Maybe Subst
unify'' [] [] s = Just s
unify'' [] _ s = Nothing
unify'' _ [] s = Nothing
unify'' (a:as) (b:bs) s =
  case unify a b s of
    Nothing -> Nothing
    Just newS -> unify'' as bs newS

(===) :: Term -> Term -> Goal
(===) t1 t2 =
  \(s, k) ->
    case unify t1 t2 s of
      Nothing -> falsify (s, k)
      Just ss -> succeed (ss, k)
     
run :: Goal -> [State]
run g = g emptyState

conjN :: [Goal] -> Goal
conjN [] = succeed
conjN (x:[]) = x
conjN (x:xs) = conj x (conjN xs)

disjN :: [Goal] -> Goal
disjN [] = falsify
disjN (x:[]) = x
disjN (x:xs) = disj x (disjN xs)

lookupN :: Term -> Subst -> Term
lookupN t s =
  case lookupSubst t s of
    Nothing -> t
    Just k ->
      case k of
        Var _ -> k
        Value _ -> k
        Functor f args -> Functor f (map (\t-> lookupN t s) args)