 # Logic programming in PureScript

I’m currently exploring logic programming as defined in the LogicT.pdf paper. There is a package purescript-logic 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
• `<|>` and `interleave` is disjunction of goals
• `>>=` and `>>-` is conjunction of goals

## Basic usage

The `MonadLogic` type class represents non-deterministic 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 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.

3 Likes