A computation in the relational world.

On its own, a goal performs search in a search tree. It takes some state and transforms it to a stream of new states. But it is better to think of a goal as a relational program. If you want to write a predicate, it will take Terms as parameters and return a Goal.

zeroo :: Term Int -> Goal ()
zeroo x = x === Value 0

A Goal is a Monad, so you can use the do-notation to write relations.

oppositeso :: Term Bool -> Term Bool -> Goal ()
oppositeso x y = do
  x === Value True
  y === Value False

Sequencing two goals performs conjunction. To make a branch, use disjunction.

noto :: Term Bool -> Term Bool -> Goal ()
noto x y = xIsTrue `disj` xIsFalse
 where
  xIsTrue = x === Value True `conj` y === Value False
  xIsFalse = x === Value False `conj` y === Value True

To execute a goal and find its solutions, use run.

>>> run (\x -> noto (Value False) x)
[Value True]

Query for solutions of a goal.

>>> run (\x -> x === Value (42 :: Int))
[42]

You can ask to solve for several variables, or none at all. You can still create intermediate variables inside using fresh, but they will not be returned as solutions.

>>> run (\() -> fresh >>= (\x -> x === Value True))
[()]

Note that there may be several solutions, including infinitely many or zero. If you want to limit the number of solutions, just put it through take.

>>> take 5 $ run (\x -> disjMany (map (\a -> x === Value a) [0 :: Int ..]))
[0,1,2,3,4]

This function will return logical representation of solutions. This matters for complex types which have a separate logical representation. If you want to transform them back to regular representation, use fmap and extract'.

>>> extract' <$> run (\x -> x === inject' [True])
[Just [True]]

Note that the retrived solutions might be subject to constraints, but it is not yet possible to retrieve them.

A goal that always succeeds.

>>> run (\() -> successo ())
[()]

A goal that always fails.

>>> run (\() -> failo)
[]

Unify two terms.

>>> run (\() -> Value 42 === Value (42 :: Int))
[()]
>>> run (\() -> Value 42 === Value (37 :: Int))
[]

Perform conjnction of two goals. If the first goal succeeds, run the second goal on its results.

>>> run (\x -> x === Value 42 `conj` x === Value (42 :: Int))
[42]
>>> run (\x -> x === Value 42 `conj` x === Value (37 :: Int))
[]
>>> run (\(x, y) -> x === Value (42 :: Int) `conj` y === Value True)
[(42,True)]

Note that the do-notation performs conjunction as well, so you will rarely need to use this function directly.

>>> :{
 run (\(x, y) -> do
   x === Value (42 :: Int)
   y === Value True
 )
:}
[(42,True)]

Perform conjunction of several goals, left to right.

>>> run (\(x, y) -> conjMany [x === Value (42 :: Int), y === Value True])
[(42,True)]

Perform disjunction of two goals. Run the first goal, then the second, and combine their results.

>>> run (\x -> x === Value 42 `disj` x === Value (37 :: Int))
[42,37]
>>> run (\x -> x === Value 42 `disj` x === Value (42 :: Int))
[42,42]
>>> run (\(x, y) -> x === Value (42 :: Int) `disj` y === Value True)
[(42,_.0),(_.1,True)]

Perform disjunction of several goals, left to right.

>>> run (\x -> disjMany (map (\a -> x === Value a) [1, 3 .. 11 :: Int]))
[1,3,5,7,9,11]

Consider several possible cases, using syntax similar to conde from faster-minikanren.

>>> :{
  run (\(x, y) -> conde
    [ [ x === Value False, y === Value 0 ]
    , [ x === Value True, y === Value 1 ]
    ])
:}
[(False,0),(True,1)]

However, this might not be the best syntax for Haskell. Using disjMany with the do-notation may be easier to type and less noisy:

>>> :{
  run (\(x, y) -> disjMany
    [ do
        x === Value False
        y === Value 0
    , do
        x === Value True
        y === Value 1
    ])
:}
[(False,0),(True,1)]

In addition, the Match module provides pattern matching over variants, which might better express your intent.

>>> :{
  run (\(x, y) -> x & (matche
    & on _False (\() -> y === Value 0)
    & on _True (\() -> y === Value 1)))
:}
[(False,0),(True,1)]

Put a constraint that two terms must not be equal.

>>> run (\x -> x =/= Value 42 `conj` x === Value (37 :: Int))
[37]
>>> run (\x -> x =/= Value 42 `conj` x === Value (42 :: Int))
[]

It is not yet possible to retrieve solutions along with remaining constraints.

The existential quantifier.

Whenever you need an intermediate variable, fresh will give you one.

>>> :{
  run (\() -> do
    x <- fresh
    x === Value (42 :: Int))
:}
[()]

Creating a lot of variables one-by-one might be tiresome though. This is why fresh is not a standalone function but a method on a type class. Fresh is implemented not only for Term a but for tuples too, so you can ask for several fresh variables at once.

>>> :{
  run (\() -> do
    (x, y) <- fresh
    x === Value True
    y === Value False)
:}
[()]

In fact, run also uses Fresh, so you can choose how many variables you want to solve for.

>>> :{
  run (\(x, y) -> do
    x === Value True
    y === Value False)
:}
[(True,False)]

As an edge case, you can ask for no variables at all using (). While this is not useful inside relations, this is how the first two examples actually work. Fresh is also used for pattern matching from the Match module when the matched value is not known yet.