Logic programming
Monadic logic

by Samir Talwar

Wednesday, 24 June 2026 at 09:00 CEST

It is a truth universally acknowledged that a data structure in possession of information, must be in want of an extra type parameter.

In the last couple of posts, we looked at implementing a simple logic DSL in Haskell.

1. I relent
2. Solving the technical interview
3. Solving the technical interview, explained
4. Monadic logic
5. Fairness in disjunctions

It works, but the syntax is a little un-Haskell-like. We can do better, simply by shoehorning in elevating it into a monad.

We start with the basics, except we’ll rename Knowledge to Subst (short for “substitutions”), as is more traditional in µKanren:

{-# LANGUAGE GHC2024 #-}
{-# LANGUAGE BlockArguments #-}

import Control.Applicative
import Control.Monad.State
import Data.Char qualified as Char
import Data.List qualified as List
import Data.Maybe (listToMaybe)
import Prelude hiding (negate)
import System.Environment (getArgs)

newtype Var = Var Int
  deriving newtype (Eq, Enum)

data Term atom
  = TAtom atom
  | TVar Var
  deriving stock (Eq)

type Subst atom = [(Var, Term atom)]

data GoalState a = GoalState Var (Subst a)

emptyState :: GoalState a
emptyState = GoalState (Var 0) []

Consider the Lesson, which we will rename here to its more conventional name, Goal:

type Goal atom = GoalState atom -> [GoalState atom]

We can make it carry an extra value around:

type Goal atom a = GoalState atom -> [(GoalState atom, a)]

If you are a Haskell programmer, you might recognise this as very similar to the State monad, except the return type is a list. It is, in fact, the same as StateT (GoalState atom) []. For example, the Control.Monad.State.runStateT function:

runStateT :: StateT s m a -> s -> m (a, s)

specialises to:

runStateT :: StateT (GoalState atom) [] a -> GoalState atom -> [(a, GoalState atom)]

Except for the order of the tuple, this is a function that takes a StateT (GoalState atom) [] a and returns the exact data type of our Goal. So let’s use it:

newtype Goal atom a = Goal (StateT (GoalState atom) [] a)
  deriving newtype (Functor, Applicative, Alternative, Monad)

And as Goal is now a wrapper around an exisiting monad type, and we can claim all of the benefits with deriving newtype.

Each output of the goal (which you may remember can be zero, one, or many, represented by a list here) also carries a value, which allows us to pass stuff around. This will be useful later.

We also derive Alternative as a replacement for Monoid; we will use empty instead of mempty and (<|>) instead of (<>). For lists, they are equivalent.

We’ll need to modify the combinators to fit the new type signature, starting with the basics:

falsity :: Goal atom ()
falsity = empty

truth :: Goal atom ()
truth = pure ()

negate :: Goal atom () -> Goal atom ()
negate (Goal g) = Goal do
  state <- get
  case evalStateT g state of
    [] -> pure ()
    _ -> empty

Note how it’s much clearer now that negate is working on the current version of the state, and therefore can only negate things that come before, not after.

Equality works the same way except that it wraps the behavior in StateT (and therefore has to pass subst around).

infix 4 ===

(===) :: forall atom. (Eq atom) => Term atom -> Term atom -> Goal atom ()
x === y = Goal $ StateT \(GoalState vars subst) ->
  maybe mempty (\newSubst -> pure ((), GoalState vars newSubst)) $
    unifyTerm (walk subst x) (walk subst y) subst
  where
    unifyTerm (TAtom x') (TAtom y') subst
      | x' == y' = Just subst
      | otherwise = Nothing
    unifyTerm (TVar v) y' subst = unifyVar v y' subst
    unifyTerm x' (TVar v) subst = unifyVar v x' subst
    unifyVar v t subst
      | occurs v t = Nothing
      | otherwise = Just (pure (v, t) <> subst)
    occurs _ (TAtom _) = False
    occurs v (TVar tv) = tv == v

&&& and ||| are almost the same:

infixr 3 &&&

(&&&) :: Goal atom a -> Goal atom a -> Goal atom a
(&&&) = (>>)

infixr 2 |||

(|||) :: Goal atom a -> Goal atom a -> Goal atom a
(|||) = (<|>)

within :: (Eq atom) => Term atom -> [Term atom] -> Goal atom ()
within x = foldr ((|||) . (=== x)) falsity

And fresh (previously consider) is where it gets interesting. Rather than accepting a lambda, fresh can return a value.

fresh :: Goal atom (Term atom)
fresh = Goal do
  GoalState nextVar subst <- get
  put $ GoalState (succ nextVar) subst
  pure (TVar nextVar)

We can do the same for understand, which I am renaming to current (and doesn’t have a name in µKanren):

current :: Term atom -> Goal atom (Term atom)
current term = Goal do
  GoalState _ subst <- get
  pure $ walk subst term

climb and learn get renamed to walk and run, and run is modified to return the value as well as the subst.

walk :: Subst a -> Term a -> Term a
walk _ term@TAtom {} = term
walk subst (TVar v) =
  maybe (TVar v) (walk subst) $ lookup v subst

run :: Goal atom a -> [(a, Subst atom)]
run (Goal goal) =
  map (\(x, GoalState _ subst) -> (x, subst)) $ runStateT goal emptyState

And now that we have a logic system working, we can start defining our solution for the N queens problem.

We start with add, which uses our monadic version of current:

add :: (Eq atom, Num atom) => Term atom -> Term atom -> Term atom -> Goal atom ()
add x y z = do
  x <- current x
  y <- current y
  z <- current z
  case (x, y, z) of
    (TAtom x, TAtom y, z) -> z === TAtom (x + y)
    (TAtom x, y, TAtom z) -> y === TAtom (z - x)
    (x, TAtom y, TAtom z) -> x === TAtom (z - y)
    _ -> falsity

And now we can define queens:

queens :: Int -> Goal Int [(Term Int, Term Int)]
queens n = queens' n []
  where
    valid = map TAtom [0 .. pred n]
    queens' 0 _ = pure []
    queens' m threatened = do
      rank <- fresh
      file <- fresh
      diag1 <- fresh
      diag2 <- fresh
      rank `within` valid
      negate (rank `within` threatenedRanks)
      file `within` valid
      negate (file `within` threatenedFiles)
      add diag1 rank file
      negate (diag1 `within` threatenedDiag1)
      add rank file diag2
      negate (diag2 `within` threatenedDiag2)
      positions <- queens' (pred m) ((rank, file, diag1, diag2) : threatened)
      pure $ (rank, file) : positions
      where
        (threatenedRanks, threatenedFiles, threatenedDiag1, threatenedDiag2) = List.unzip4 threatened

We have rewritten the whole thing in do notation, using bindings to allocate fresh variables. And we’ve lost all the &&& chaining because it’s just >>, which means it can be replaced with a newline.

Check out the new return type. We also return the lists of positions (ranks and files), which we can use for a much more pleasant way of solving this problem.

We define our Position:

data Position = Position Int Int
  deriving stock (Eq, Ord)

instance Show Position where
  show (Position rank file) =
    Char.chr (rank + Char.ord 'a') : show (file + 1)

And now we can rewrite solveQueens to take advantage of our new return value. We have the terms, but they are TVars, so we need to walk over subst to get the actual TAtom values out. We no longer need to guess the variable names.

findQueen :: Subst Int -> (Term Int, Term Int) -> Position
findQueen subst (rankTerm, fileTerm) = Position rank file
  where
    TAtom rank = walk subst rankTerm
    TAtom file = walk subst fileTerm

solveQueens :: Int -> [Position]
solveQueens n = map (findQueen subst) positionTerms
  where
    (positionTerms, subst) = head $ run (queens n)

main :: IO ()
main = do
  args <- getArgs
  let n = maybe 8 read $ listToMaybe args
  print $ solveQueens n

There we go. Add a type parameter, get a free monad, and much more understandable code.

1. I relent
2. Solving the technical interview
3. Solving the technical interview, explained
4. Monadic logic
5. Fairness in disjunctions