Logic programming in PureScript

Feedback
#1

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 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.

3 Likes