Skip to content

Instantly share code, notes, and snippets.

@msullivan
Created February 26, 2015 22:54
  • Star 7 You must be signed in to star a gist
  • Fork 4 You must be signed in to fork a gist
Star You must be signed in to star a gist
Save msullivan/4223fd47991acbe045ec to your computer and use it in GitHub Desktop.
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)
@andrey-vyatkin
Copy link

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

@msullivan
Copy link
Author

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

@dewshick This response is five years late, but I stumbled back across it when looking back at this while reading https://aphyr.com/posts/354-unifying-the-technical-interview (which is fantastic!), but maybe it will still be useful to someone.

It isn't really an "inverse-eta-delay", since there is no delay and no eta (because laziness obviates the need for those), but we still need to mark recursion in some circumstances in order to guarantee that the entire tree is searched. A simple example of this is the fivesRev case in the snippet, which recurses on the left of the disjunction instead of on the right. Without the zzz, we would infinitely chase down the leftmost branch of the search tree looking for a left that we will never find. With the zzz, we run into the Delay before we expand the recursive search tree and we switch to looking on the RHS for a bit.

@davidar
Copy link

davidar commented May 24, 2021

Note that KList is essentially the Stream monad (updated version here), and Program is the StateT transformation of it. This allows several things to be simplified, notably:

type Program = StateT State Stream
zzz = mapStateT Stream.suspended
callFresh = (fresh >>=)
disj = (<|>)
conj = (>>)
runTest p = Stream.observeAll (execStateT p ([], 0))

which uses the helper function:

fresh :: Program Term
fresh = do
  (s, c) <- get
  put (s, c+1)
  return (Var c)

A side benefit is that it also allows programs to be written a little more haskell-y:

a_and_b = do
  a <- fresh
  equiv a (Atom "7")
  b <- fresh
  equiv b (Atom "5") <|> equiv b (Atom "6")

@saolof
Copy link

saolof commented Jun 18, 2021

Note that KList is essentially the Stream monad (updated version here), and Program is the StateT transformation of it. This allows several things to be simplified, notably:

type Program = StateT State Stream
zzz = mapStateT Stream.suspended
callFresh = (fresh >>=)
disj = (<|>)
conj = (>>)
runTest p = Stream.observeAll (execStateT p ([], 0))

which uses the helper function:

fresh :: Program Term
fresh = do
  (s, c) <- get
  put (s, c+1)
  return (Var c)

A side benefit is that it also allows programs to be written a little more haskell-y:

a_and_b = do
  a <- fresh
  equiv a (Atom "7")
  b <- fresh
  equiv b (Atom "5") <|> equiv b (Atom "6")

Only if you are fine with depth first search. It's very intentionally not the same as the stream monad, because the latter would do DFS and gets stuck in subgoals while a BFS implementation guarentees progress on all subgoals. They are very closely related though, and the better way to do it imho is to generalize to priority streams using a mergable heap type like pairing heaps.

@davidar
Copy link

davidar commented Jun 20, 2021

@saolof Perhaps you're thinking of the Stream monad from the stream-fusion package (which unfortunately shares the same module namespace)? The stream-monad Stream deliberately avoids the pitfalls of DFS, see here for details

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment