Skip to content

Instantly share code, notes, and snippets.

What would you like to do?
MicroKanren (μKanren) in Haskell
import Control.Monad
type Var = Integer
type Subst = [(Var, Term)]
type State = (Subst, Integer)
type Program = State -> KList State
data Term = Atom String | Pair Term Term | Var Var deriving Show
-- Apply a substitution to the top level of a term
walk (Var v) s = case lookup v s of Nothing -> Var v
Just us -> walk us s
walk u s = u
extS x v s = (x, v) : s
-- Try to unify two terms under a substitution;
-- return an extended subst if it succeeds
unify :: Term -> Term -> Subst -> Maybe Subst
unify u v s = un (walk u s) (walk v s)
where un (Var x1) (Var x2) | x1 == x2 = return s
un (Var x1) v = return $ extS x1 v s
un u (Var x2) = return $ extS x2 u s
un (Pair u1 u2) (Pair v1 v2) =
do s' <- unify u1 v1 s
unify u2 v2 s'
un (Atom a1) (Atom a2) | a1 == a2 = return s
un _ _ = mzero
-- MicroKanren program formers
zzz :: Program -> Program
zzz g = \sc -> delay (g sc)
equiv :: Term -> Term -> Program
equiv u v = \(s, c) -> case unify u v s of
Nothing -> mzero
Just s' -> return (s', c)
callFresh :: (Term -> Program) -> Program
callFresh f = \(s, c) -> f (Var c) (s, c+1)
disj :: Program -> Program -> Program
disj g1 g2 = \sc -> mplus (g1 sc) (g2 sc)
conj :: Program -> Program -> Program
conj g1 g2 = \sc -> g1 sc >>= g2
-- I had originally thought that since Haskell was lazy, we didn't
-- need to worry about any of the inverse-eta-delay stuff that the
-- Scheme version does, but that isn't right. We still need some way
-- to force switching when we recur.
-- It is not very burdensome for us, though; we don't actually need
-- to eta-expand, just need to add some sort of marker.
data KList a = Nil | Cons a (KList a) | Delay (KList a) deriving Show
delay = Delay
-- Hm. Is there any reason to preserve the delays?
instance Monad KList where
return x = Cons x Nil
Nil >>= f = mzero
x `Cons` xs >>= f = f x `mplus` (xs >>= f)
Delay xs >>= f = Delay (xs >>= f)
instance MonadPlus KList where
mzero = Nil
Nil `mplus` xs = xs
(x `Cons` xs) `mplus` ys = x `Cons` (ys `mplus` xs) -- swapped per sect. 6
Delay xs `mplus` ys = Delay (ys `mplus` xs)
klistToList Nil = []
klistToList (x `Cons` xs) = x : klistToList xs
klistToList (Delay xs) = klistToList xs
-------------- Test cases
empty_state = ([], 0)
five = callFresh (\x -> equiv x (Atom "5"))
fives_ x = disj (equiv x (Atom "5")) (zzz $ fives_ x)
fives = callFresh fives_
fivesRev_ x = disj (zzz $ fivesRev_ x) (equiv x (Atom "5"))
fivesRev = callFresh fivesRev_
a_and_b = conj
(callFresh (\a -> equiv a (Atom "7")))
(callFresh (\b -> disj (equiv b (Atom "5")) (equiv b (Atom "6"))))
runTest p = klistToList (p empty_state)

This comment has been minimized.

Copy link

@dewshick dewshick commented Mar 13, 2016

I don't understand why do we need to keep inverse-eta-delay, we can recur without any delays, cant we?

fives_ x = x `equiv` ((Atom "5") `disj` (fives_ x) `disj` (sixes_ x))
sixes_ x = x `equiv` ((Atom "6") `disj` (fives_ x))

no problems with switching here, all the results are present

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.