Assignment 2, Unify Two Tree-Structured Terms

{-# LANGUAGE InstanceSigs #-}
module Lib where

Haskell and Prolog both rely on unification to work. How does unification work? Let’s build it and find out!

For this assignment, you will create a unification framework in Haskell capable of flexibly performing unification in many different contexts, including Prolog expressions and lists.

Briefly, for this assignment, you’ll submit Haskell code that defines:

• return :: a -> PExpr a and (>>=) :: PExpr a -> (a -> PExpr b) -> PExpr b to describe how to manipulate values inside a Prolog Expression (PExpr)
• walk :: (Monad m, Eq a) => Substitution m a -> Expr m a -> Expr m a to expand an expression (of any type) by substituting variables inside of it for their values
• unify :: (Eq a) => Substitution PExpr a -> Expr PExpr a -> Expr PExpr a -> [Substitution PExpr a] and also unify :: (Eq a) => Substitution [] a -> Expr [] a -> Expr [] a -> [Substitution [] a] to compute what substitutions can make two Prolog Expressions or two lists look like each other.
• splits :: [a] -> [([a], [a])], a helper function for the second unify that gives back all the ways to break a sigle list into left and right parts

The pieces you need to finish are marked with todo:

todo :: a
todo = undefined

Here is a Lib.hs starter file, but note that it lacks a tremendous amount of useful information that you’ll find below!

1 Relational Programming

A function maps its argument to a value. Given an argument, the function can produce a value. A relation instead decsribes a relationship between arguments and values that may or may not hold. So, the function + takes two numbers and adds them together to produce a result. The relation + describes what addition means so that we can tell which two numbers sum to a third.

In this context, the distinction between “argument” and “result” is no longer particularly clear, which is part of where the power of relational programming comes from! Indeed if we have a relational + like +(a1, a2, sum), then (in an ideal implementation) we get relational - for free. If -(s1, s2, difference) means s2 - s1 = difference, we can just note that that also means s2 = difference + s1 and use it to define -(s1, s2, difference) as +(difference, s1, s2).

As another example, we might define p(x, y) to mean that y is either the same as x or is the number 42. If we ask under what conditions p(x, y) holds, we should learn that it holds when x is anything and y has the same value as x but also when x is anything and y is 42. If we ask under what conditions p(x, 20) holds, however, we should learn that it holds when x is 20 and under no other circumstances.

Prolog is a relational programming language. We’ll get to it soon!

At its core are two key ideas:

1. Automatic search through goals that define whether a relation holds or not. (In Prolog, this is depth-first search.)
2. Unification to determine whether two structures that may contain variables (unconstrained parts) can be made identical through appropriate assignment to the variables.

In this assignment, we’ll build the unification piece in Haskell while exploring some powerful Haskell typeclasses and making our own. Unification is also what Haskell uses to put together its “detective work” to piece together the type constraints it finds for each expression in your program. (When you’re done with this assignment, you might be able to envision how that works!)

2 Data Types

We need a few data types to build our relational programming engine.

2.1 Variable Identifier

A “variable” names an unspecified value in our relational programs. An unconstrained variable can be anything at all. Later, we might constrain it, as with y above when we said it had to be equal to x or later when we said x had to be 20, specifically.

We represent a variable simply as a number. Rather than making a brand new type, we use type to make VarId a synonym for Integer:

type VarId = Integer

2.2 General Expressions

We can constrain a variable to equal a value or expression, but what is an “expression”? We build it in two parts in a way that lets us represent Prolog predicates, Haskell types, or many other structures!

Simple values can be any Haskell type that we can compare for equality, like the numbers we used above (20, 42, etc.), or Strings, or something more complex like SparseLists.

An expression is a structure built up from simple values in some way. We represent an expression as Expr u a. That’s a type constructor with two arguments. a is the type for simple values. u is the structure of expressions. We’ll insist u is “unifiable” (with our own typeclass) and that it is a “monad” (with the builtin Monad typeclass).

We can think of a Monad as a container. Critically for us, we can “splice” values into a Monad, which will let us “peek” inside an expression to replace its variables with new expressions or simple values when we need to.

We play one more trick: since our u container can contain any type, we force it to make room for either an a or a variable through the power of polymorphism!!!

type Expr u a = u (Either VarId a)

(Haskell defines Either as: data Either a b = Left a | Right b.)

To define a unifiable container, we need “substitutions”. The full definition is below, but briefly a substitution is a collection of constraints on variables.

Unifying two u expressions produces a list of substitutions each of which can make the two expressions look the same. (An empty result means the two expressions cannot be made to look the same.) We actually start unification with a substitution as well (representing initial constraints). To ensure we can compare simple values for equality, we put an Eq a constraint on:

class Unifiable u where 
  unify :: (Eq a) => Substitution u a -> 
                       Expr u a -> 
                       Expr u a -> 
                         [Substitution u a]

2.3 Substitutions

A substitution is a mapping from VarIds to Exprs: the constraints on the variables. A legal substitution can never have two mappings for the same variable. That makes it a “partial function” from VarId to Expr.

A new typeclass would be the awesome way to represent this. We just use an “association list” instead: a list of tuples of a variable and the expression it must equal.

type Substitution u a = [(VarId, Expr u a)]

(We’re not going to impose the “occurs check” on these substitutions since Prolog doesn’t either.)

2.4 Specific Expressions

An expression can be anything that sastisfies the rules above, but let’s focus on simulating Prolog expressions:

data PExpr a = Value a
             | Term String [PExpr a]
  deriving (Show, Eq, Ord)

A Prolog expression can be an atom (effectively a string), a number, a variable, or a compound term. A compound term (a “predicate” or relation) has a name and a (non-empty) list of arguments.

We’ll use:

• a Term with no sub-expressions for an “atom”
• a Value with some numeric type inside for a number
• a Value with a VarId inside for a variable
• a Term with sub-expressions for a “compound term”

Let’s use Prolog’s append as an example of how PExprs can represent Prolog predicates:

append([], X, X).
append([X|Xs], Y, [X|Zs]) :- append(Xs, Y, Zs).

There are three uses of append there: + append([], X, X): if X is the variable 1, and the empty list is the term named "[]", then this is: Term "append" [Term "[]" [], Value (Left 1), Value (Left 1)]. + append([X|Xs], Y, [X|Zs]): numbering the variables left to right as 1, 2, 3, and 4, and choosing a sensible representation for list construction, this is: Term "append" [Term "|" [Value (Left 1), Value (Left 2)], Value (Left 3), Term "|" [Value (Left 1), Value (Left 4)]]. + The last one doesn’t really introduce anything new. Give it some thought!

Now we need to make this a monad and make it unifiable.

The monad typeclass has two functions to implement. First is return to put a regular value inside a PExpr, typically in the most trivial way you can for your monad (which is not much like Java’s return!):

instance Monad PExpr where
  return :: a -> PExpr a
  return = todo

We also need to say how to “splice” new values into a PExpr with the “bind” operator, written >>=. It takes an original PExpr a and a function to “splice” out any a in the PExpr with something new (a PExpr b). bind puts these together into a value representing the PExpr b built by applying the function on each a value in the old PExpr a.

So, for example, we could replace each value with a term named after the value and place the original value and its successor inside as strings (changing the type of values):

  -- >>> (Value 4) >>= (\a -> Term (show a) [Value (show a), Value (show (succ a))])
  -- Term "4" [Value "4",Value "5"]

For (Value 4), we get a Term with two arguments, one the original value as a string, the other one larger than that.

For a more complex term, we apply our “splicing” anywhere there is a value. Note that exactly what is spliced in depends on the value it replaces:

  -- >>> Term "More complex" [Value 4, Term "atom" [], Value 12] >>= (\a -> Term (show a) [Value (show a), Value (show (succ a))])
  -- Term "More complex" [Term "4" [Value "4",Value "5"],Term "atom" [],Term "12" [Value "12",Value "13"]]

In PExpr, as live only in the Value case. In that case, we just pull out the a and give back the PExpr b the function produces with it. However, we need to recursively splice inside the Term case as well:

  (>>=) :: PExpr a -> (a -> PExpr b) -> PExpr b
  (Value a) >>= f         = todo
  (Term s pexprs) >>= f   = todo  -- Hint: map is your friend!

P.S. Applicative and Functor are superclasses of Monad; so, we need to make PExpr instances of them, too. Though you can skip these, they are very much worth learning! If we already have a Monad instance, there are standard formulas we can use for these two:

instance Functor PExpr where
  fmap :: (a -> b) -> PExpr a -> PExpr b
  fmap f pa = pa >>= return . f

instance Applicative PExpr where 
  pure :: a -> PExpr a 
  pure = return

  (<*>) :: PExpr (a -> b) -> PExpr a -> PExpr b 
  pf <*> pa = pf >>= (\f -> pa >>= return . f)

2.5 Some Sample Expressions

To test and play, you’ll want some sample expressions! We’ll focus on PExpr String.

It’s convenient to be able to make a VarId or an a into an Expr m a easily. Left or Right transform VarId or a into Either VarId a, and return transforms that into m (Either VarId a), also known as Expr m a:

-- | Turn a variable into its corresponding expression.
pureVarId :: Monad m => VarId -> Expr m a
pureVarId = return . Left

-- | Turn a simple value into its corresponding expression.
pureA :: Monad m => a -> Expr m a
pureA = return . Right

Here are a bunch of simple values, some variables, and a value for “empty”:

one, two, three, four :: Expr PExpr String
one = pureA "1"
two = pureA "2"
three = pureA "3"
four = pureA "4"

x, y, z, xs, ys, zs, empty :: Expr PExpr a
x = pureVarId 1
y = pureVarId 2
z = pureVarId 3
xs = pureVarId 4
ys = pureVarId 5
zs = pureVarId 6
empty = Term "[]" []

We can form “cons cells” by putting two expressions together into a | term:

cons :: Expr PExpr a -> Expr PExpr a -> Expr PExpr a
cons a as = Term "|" [a, as]

We can take advantage of cons and empty to easily make whole lists:

list :: [Expr PExpr a] -> Expr PExpr a
list = foldr cons empty

Here are some sample lists:

l12, l34, l1234 :: Expr PExpr String
l12 = cons one (cons two empty)
l34 = cons three (cons four empty)
l1234 = list (map pureA ["1", "2", "3", "4"])

3 Reasoning with Substitutions

We want to be able to perform some operations on substitutions.

3.1 Looking Up a Variable

The most basic is to take a variable and look it up in our list of substitutions to find the associated expression. This is a partial function; so, it will return a Maybe (Expr u a). Happily, this is built into Haskell’s Data.List module as lookup :: Eq a => a -> [(a, b)] -> Maybe b.

3.2 Fully “Looking Up” an Expression

What is a variable in a substitution really constrained to equal? Of course, the substitution maps it to an expression, and it equals that expression. But, that expression could itself contain variables that are also mapped under the substitution. We want to replace those with what they are mapped to, and so on.

To make this work, we’ll take advantage of the built-in function either:

either :: (a -> c) -> (b -> c) -> Either a b -> c
either f _ (Left a) = f a
either _ g (Right b) = g b

It pastes together a function for left values and a function for right values into a function for an Either.

Now, let’s replace each variable in the expression with its value. We can do that with >>=. Remember, that lets us splice things in wherever we find a value. For variables, we splice in the result of trying out the substitution on the variable. For values, we just give the value back as an expression.

-- | For each variable in s, walk replaces it anywhere it appears in
-- expr with its value. It then continues these replacements until there
-- are no more to do.
--
-- Note that we really only have >>= available to operate on expr
-- because all we actually know about it is that it's a Monad!
--
-- As examples, nothing happens when we walk with an empty substitution:
--
-- >>> walk [] (Term "Hello" [Value (Right "World!")])
-- Term "Hello" [Value (Right "World!")]
--
-- Just substituting out a variable gives us that variable's value:
--
-- >>> walk [(7, Value (Left 3))] (Value (Left 7))
-- Value (Left 3)
--
-- But walk will do all the substitutions it finds anywhere inside
-- an expression, even if those create more substitutions to perform in turn:
--
-- >>> walk [(1, Value (Left 2)), (2, Value (Right "Two")), (3, Term "Three" [Value (Left 1), Value (Left 4)])] (Value (Left 3))
-- Term "Three" [Value (Right "Two"),Value (Left 4)]
walk :: (Monad m, Eq a) => Substitution m a -> Expr m a -> Expr m a
walk s expr = todo -- splice replacements in for expr's values
                   -- use either to build a single function out of a left and right one

So far, we’re splicing something in at each variable-or-simple-value in expr. If it’s a simple value, we just want to turn it back into an Expr m a (a m (Either VarId a)), meaning we do nothing in the end.

If it’s a variable, we use tryS that tries to do a substitution on the variable. If the variable is not in the substitution, we again just transform it straight back into an Expr m a. Otherwise, we found another substitution to do! We recursively walk it.

  where tryS v = case lookup v s of 
                   Nothing -> todo
                   Just e -> todo

(Since Haskell is lazy, this does the full set of substitutions as needed, not instantly.)

3.3 Building Substitutions

We also want to be able to extend a substitution with new bindings for variables. Caution: you should not be remapping something that is already mapped, even though our implementation as written does allow that.

extendSub :: Substitution u a -> VarId -> Expr u a -> Substitution u a
extendSub s v e = (v, e):s

To make this work, it would be handy to have an easy way to make an empty substitution:

emptySub :: Substitution u a
emptySub = []

4 Unification

We’re ready for unification! Two expressions in a relational program unify if we can make them equal with appropriate substitutions for the variables in the expressions. In other words, given two expressions and a substitution that constrains their variables, what substitutions that extend the given one can make the two expressions equal?

instance Unifiable PExpr where
  unify :: (Eq a) => Substitution PExpr a -> Expr PExpr a -> Expr PExpr a -> [Substitution PExpr a]
  unify s u v = helper (walk s u) (walk s v)
    where

Two variables may already be equal, in which case there is nothing to be done to the substitution:

      helper (Value (Left v1)) (Value (Left v2)) | v1 == v2 = todo

Otherwise, given a variable and anything, just map the variable to the value. This includes the case where both are variables (but not the same variable):

      helper (Value (Left v)) e = todo
      helper e (Value (Left v)) = todo

Otherwise, if these are Values, then they’re simple values, and we can only insist they are equal to each other. We don’t have the ability to look inside them. If they’re equal, our existing substitution works. If not, no substitution works:

      helper _ _ = todo

If one expression is a Term and one a (non-variable) Value, then we cannot unify them. In that case, we’ll fail (no substitutions work).

      helper _ _ = todo
      helper _ _ = todo

If these are both terms, we need to check that their top-level parts are shaped appropriately to be equal (same string, same number of subexpressions) and then recursively unify them:

      helper (Term s1 us) (Term s2 vs) | s1 /= s2 || (length us /= length vs) = todo
                                       | otherwise = unifyAll [s] us vs

To unify all of those pairs, we need to “roll them up”, building up substitutions via unification as we go. (We can’t unify them separately with map because a substitution for one may conflict with a substitution for another.)

If the lists are empty, then we are done and give back all the substitutions found so far. Otherwise, we unify the heads of the list with each available substitution, collapsing the result down into a single list of substitutions, and then hand the resulting substitutions off to the recursive call.

Be sure to call unify recursively and not helper. That’s forces us to “walk” the terms we’re unifying. Otherwise, we could get one substitution for a variable from one part of the term, a different substitution from another part, and accept both into our list.

Note: you can think of concat as having the type [[a]] -> [a]: appending together all the individual lists in a nested list into a single list.

      unifyAll ss [] [] = todo
      unifyAll ss (u':us) (v':vs) = unifyAll (concat (map todo ss)) us vs
      unifyAll _ [] _ = error "Only use with equal length lists."
      unifyAll _ _ [] = error "Only use with equal length lists."

(We will actually never get a result with more than one substitution! Can you see why not?)

4.1 Good Work! Try Some Unification

You’ve built one of the two core pieces of Prolog. Try it out!

How about these? What substitutions do they produce, and why?

unify [] one one -- success
unify [] one two -- failure
unify [] x x
unify [] x y
unify [] x l12
unify [] (cons x (cons y empty)) l12
unify [] (cons x (cons y ys)) l12
unify [] (cons x (cons (pureA "10") empty)) (cons (pureA "11") (cons y empty))
unify [] (cons x (cons (pureA "10") empty)) (cons (pureA "11") (cons x empty))

Note that an empty list indicates failure, but a list containing an empty list is success (with no new constraints added). We can also add initial constraints in the first argument:

unify [(1, one)] one x
unify [(1, one)] two x

5 Other Expressions

PExpr is not the only type of expression we can have! We can make plain old lists into Exprs. To do that, we need them to be instances of Unifiable and Monad, but lists are already Monad instances.

5.1 Unification with Lists

How do we unify lists with variables inside? To get there, we need to understand how lists implement Monad. What does it mean to build from a [a] and a a -> [b] to produce a [b] by “splicing in” values? In this case we concatenate together a single long list of bs from all the individual [b]s we create from each a. For example:

([1,2,3] >>= (\x -> [x*10, x*10 + 5])) == [10,15] ++ [20,25] ++ [30,35]

Here’s a more complex example:

([0,1,2] >>= (\n -> replicate n (show n))) == [] ++ ["1"] ++ ["2", "2"]

That means each of our variables can “expand” to be a list of values (or variables). It can even “contract” to become the empty list and disappear from our list.

So, for example, if we unify [Right "a", Right "b", Left 1, Right "e"] with [Right "a", Right "b", Right "c", Right "d", Right "e"], we should get a substitution that says variable 1 is [Right "c", Right "d"]. If we instead unify against [Right "a", Right "b", Left 1, Right "e"], then variable 1’s value is []. Unifying against [Right "a", Right "x", Left 1, Right "e"] should fail, however.

Even more interesting, if we unify [Left 1, Left 2] against [Right "a"], there are two solutions. It could be that variable 1 is [] and 2 is [Right "a"], or it could be that variable 1 is [Right "a"] and variable 2 is [].

How should this strange unification work out?

unify [] [Left 1, Right "a", Left 1] [Right "a", Left 2, Right "a", Left 1]

5.2 Implementation

instance Unifiable [] where
  unify :: (Eq a) => Substitution [] a -> Expr [] a -> Expr [] a -> [Substitution [] a]
  unify s u v = helper (walk s u) (walk s v)
    where

Two empty lists unify, with no further substitutions:

      helper _ _ = todo

Hm.. I have an eerie feeling we forgot a pair of cases here, realized we forgot it in testing, but then forgot it again when distributing the assignment. What could they be?

      helper _ _ = todo
      helper _ _ = todo

Two lists that begin with simple values either cannot unify if the values are not equal or unify if the rests of the lists do:

      helper _ _ = todo

Much like two matching simple values, two matching variables already match with no change to the substitution:

      helper _ _ = todo

After that, we can create a substitution to let a variable at the front of the left list match with any number of elements (including zero) from the start of the right list. However, we won’t allow it to match with anything that includes itself. (elem will help.)

      helper (Left n:xs) ys = concatMap applyChoice (splits ys)
        where applyChoice (start,rest) = todo

A variable at the start on the right side works similarly:

      helper _ _ = todo

Finally, the splits helper function that gives you every possible way to break a single list into a left and right part is key to help with those cases:

-- | splits xs returns a list of tuples (left, right)
-- such that left ++ right == xs. The lists come back in
-- order of increasing length of left, beginning with ([], xs).
splits :: [a] -> [([a],[a])]
splits = todo

6 What We Won’t Do: Making and Resolving Goals

The other power of Prolog is to express and explore different ways of satisfying a relation. Prolog actually does depth-first search through the space of goals, looking for a way to satisfy them. (Depth-first search tends to be memory efficient. But, it can also get stuck exploring infinite branches and never give a result. Haskell makes it straightforward to replace this with breadth-first search and find every solution in a finite set in a finite number of steps.)

Sadly, we’re not going to get there. It might make a cool project. If you’re interested, check out the microKanren paper we have been loosely following up to now!