Types that can enter the relational world.

Simple types without fields, such as Bool and Int, can be used in relational programs as is. Instances for such types are as simple as

data Ternary = True | False | Maybe deriving (Eq)
instance Logical Ternary

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

When a type contains other types, this becomes more tricky. Consider the following type:

data Point = Point { x :: Int, y :: Int }

In the relational world, values may be known only partially. For example, we may find out that some equation is true only for a particular value of x, but once that holds, y can be anything. The definition above cannot express this, since Point has to be instantiated with some particular pair of Ints.

To account for this, we'd like to modify the definition slightly, so that each field can possibly contain a variable:

data LogicPoint = LogicPoint { logicX :: Term Int, logicY :: Term Int }

Term a here can either be a Var or a Value for type a.

Now we can specify that a Point becomes a LogicPoint in the relational world:

instance Logical Point where
  type Logic Point = LogicPoint

However, we are not finished here yet. When a type has a different representation in the logical world, we need to show how we can go from a Point to a LogicPoint with inject and go back with extract:

inject (Point x y) = LogicPoint (Value x) (Value y)
extract (LogicPoint (Value x) (Value y)) = Just (Point x y)
extract _ = Nothing

Note that while we can always transform a Point to a LogicPoint, going back to a Point can fail if any field contains a variable.

We also need to show how LogicPoints can be unified. For simple types, unification of terms works in the following way. If both terms are already known, we just check that they are equal. Otherwise, one of the terms is a variable, and we record that it must be equal to the other term.

With complex types, a third case is possible: we can refine an existing value if one of its fields is a variable. We can achieve this by unifying each field separately.

unify (LogicPoint leftX leftY) (LogicPoint rightX rightY) state =
  unify' leftX rightX state >>= unify' leftY rightY

unify takes two values being unified and the current state. If unification succeeds, a new state with acquired knowledge is returned. if unification leads to contradiction (the two values cannot be unified), unify returns Nothing. You do not modify the state yourself — this is handled by unify', a version of unify which works on Terms instead of logic values.

When we find out that a variable must have a particular value, we need not only to add a new entry in the state, but also update existing values which might contain that variable. This is the job of walk, which takes the value being updated and the current state. Just like with unify, the actual job of replacing variables with values is done by walk', and you only need to apply it to each field.

walk f (LogicPoint x y) = LogicPoint (walk' f x) (walk' f x)

You may notice that the logical representation of the type and the Logical instance are suitable for automatic generation. Indeed, the GenericLogical module provides generic versions of Logical's methods. The TH module goes further and provides makeLogic to generate logical representations for your types.

Although you'll see instances for base types below, keep in mind that they're only available from the LogicalBase module.

A variable, which reserves a place for a logical value for type a.

A logical value for type a, or a variable.

Note that a must be the “normal” type, not its logical representation, since Term stores Logic a. For example, Term (Either String (Tree Int)) will correctly use LogicList Char and LogicTree Int deep inside. This way, you do not need to know what the logic representation for a type is named, and deriving the logical representation for a type is trivial.

Treat a type as atomic, i.e. containing no variables inside. This requires a only to have an Eq instance, thus ignoring its logical representation if it exists. Useful when you really don't want to look inside something.

type Symbol = Atomic String

unify, but on Terms instead of Logic values. If new knowledge is obtained during unification, it is obtained here.

walk, but on Terms instead of Logic values. The actual substitution of variables with values happens here.

inject, but to a Term instead of a Logic value. You will use this function in your relational programs to inject normal values.

run (\x -> x === inject' [1, 2, 3])

extract, but from a Term instead of a Logic value. Note that this transformation can fail in the general case, because variables cannot be transformed to values.

You will use this function to transform solutions of a program back to their normal representation.

>>> extract' <$> run (\x -> x === inject' (Left 42 :: Either Int Bool))
[Just (Left 42)]

Add a constraint that two terms must not be equal.

One branch in the search tree. Keeps track of known substitutions and variables.

The initial state without any knowledge and variables.

Create a variable in the given state.