I’m currently exploring logic programming as defined in the LogicT.pdf paper. There is a package purescriptlogic that implements some parts but it is undocumented so I thought I’d use the opportunity to document it while I’m learning. I’ve made some PRs to the package but the author hasn’t responded yet. If He doesn’t respond in a week I’m going to create a new package and try to implement the paper fully if I can.
Anyway I wanted to get some feedback on the main readme in my PR and also any wisdom or experience you can share with logic programming. Here is the contents of the readme:
Logic programming in PureScript
Based on the paper Backtracking, Interleaving, and TerminatingMonad Transformers and the similair Haskell package logict.

empty
is a failed computation 
pure
is a successful computation 
<>
andinterleave
is disjunction of goals 
>>=
and>>
is conjunction of goals
Basic usage
The MonadLogic
type class represents nondeterministic computations.
Logic program with four successful solutions; 10
, 20
, 30
and 41
:
logicNumber :: forall m. MonadLogic m => m Int
logicNumber = pure 10 <> pure 20 <> pure 30 <> pure 41
Logic program with four successful solutions; 11
, 21
, 31
and 42
:
logicNumberSucc :: forall m. MonadLogic m => m Int
logicNumberSucc = logicNumber >>= \i > pure (i + 1)
Logic program resulting in only even integers as valid solutions:
logicEven :: forall m. MonadLogic m => Int > m Int
logicEven i = do
guard (i `mod` 2 == 0)
pure i
A logic program that filters out even integers, multiplies them with 100
. If there are no even integers, the computation succeeds with 1337
:
logicSoftCut :: forall m. MonadLogic m => m Int > m Int
logicSoftCut xs = do
ifte (xs >>= logicEven)
(\i > pure (i * 100))
(pure 1337)
ifte
represents the logic programming paradigm “negation as finite failure”, which performs a logical computation when some other computation fails.
Fair disjunction
Consider the everyOtherInt
computation, it contains infinite solutions:
everyOtherInt :: forall m. MonadLogic m => Int > m Int
everyOtherInt = pure >=> \i > pure i <> everyOtherInt (i + 2)
Note: This could in theory be simplified but PureScript is strict so pure >=>
allows lazy data structures to defer evaluation lest we run out of memory.
oddIntegers :: forall m. MonadLogic m => m Int
oddIntegers = everyOtherInt 1
evenIntegers :: forall m. MonadLogic m => m Int
evenIntegers = (oddIntegers <> pure 2) >>= logicEven
evenIntegers
should in theory succeed with 2
but since oddIntegers
is infinite the computation diverges.
interleave
is a “fair” version of <>
that interleaves solutions in two computations. This is important when one computation is potentially infinite.
evenIntegers :: forall m. MonadLogic m => m Int
evenIntegers = (oddIntegers `interleave` pure 2) >>= logicEven
evenIntegers
now succeeds with 2
.
Fair conjunction
Consider the integers
computation, it contains infinite solutions:
integers :: forall m. MonadLogic m => m Int
integers = (pure 1 <> pure 2) >>= everyOtherInt
The following computation diverges because all even integers are followed by all odd integers:
evenIntegers :: forall m. MonadLogic m => m Int
evenIntegers = integers >>= logicEven
>>
is a “fair” version of >>=
that interleaves resulting solutions.
integers :: forall m. MonadLogic m => m Int
integers = (pure 1 <> pure 2) >> everyOtherInt
evenIntegers :: forall m. MonadLogic m => m Int
evenIntegers = integers >>= logicEven
evenIntegers
now succeeds with even integers.
Full example: Primes
A program that prints the first ten primes to the console:
module Ex.Primes where
import Prelude
import Control.Monad.List.Trans as ListT
import Control.Monad.Logic.Class (class MonadLogic)
import Control.Monad.Logic.Class as Logic
import Control.MonadZero (empty, guard, (<>))
import Effect (Effect)
import Effect.Class.Console (logShow)
integers :: forall m. MonadLogic m => Int > m Int
integers = pure >=> \i > pure i <> integers (i + 1)
range :: forall m. MonadLogic m => Int > Int > m Int
range start stop =
if start > stop then
empty
else
pure start >>= \i > pure i <> range (i + 1) stop
divisors :: forall m. MonadLogic m => Int > m Int
divisors n = do
d < range 2 (n  1)
guard $ n `mod` d == 0
pure d
primes :: forall m. MonadLogic m => m Int
primes = do
n < integers 2
Logic.ifte (Logic.once $ divisors n)
(const empty)
(pure n)
main :: Effect Unit
main = ListT.runListTRec $ ListT.take 10 $ logShow =<< primes
once
is a control structure to prune results. We don’t care about the divisors themselves, only that if there is at least one then n
is not a prime. Calculating the rest of the divisors is wasteful so if we can stop the computation that’s useful as a performance optimization.