Recently, I thought about two seemingly different topics which turn out to form a fruitful combination.

One thing I have been thinking about a lot is how to model functional-logic programming in Haskell without using impure features to ensure call-time choice semantics of lazy computations. The other thing is how to integrate constraint solving in a purely functional setting, to improve the performance of test-case generation.

It turns out that a framework for constrained monadic computations is enough to express call-time choice in non-deterministic lazy computations. We can add constraint solving to any instance of the MonadPlus type class and, hence, reuse existing instances of this class to model lazy functional-logic programming in pure Haskell.

This post discusses how to add constraints to any instance of MonadPlus. How to use a constraint monad to model functional-logic programming will be explained elsewhere. A module implementing the ideas described in this post is available as plain literate Haskell file and in a marked-up version for online reference. You can access the most recent version of the module using git by fetching my git repository.

Default implementation of MonadPlus

Let’s start with a simple instance of MonadPlus that implements every operation but (>>=) with a constructor:

data MP a = Return a | MZero | MPlus (MP a) (MP a)

instance Monad MP
 where
  return = Return

  Return x  >>= f = f x
  MZero     >>= _ = MZero
  MPlus x y >>= f = MPlus (x >>= f) (y >>= f)

instance MonadPlus MP
 where
  mzero = MZero
  mplus = MPlus

Guards and Constraint Stores

We want to be able to guard monadic computations with constraints. Specifically, we’d like to have an additional operation

guarded :: Constraint -> m a -> m a

that asserts a given constraint in a given computation. In order to not fix the type of constraints we make it an associated type synonym of a type class for constraint stores. So the actual type of guarded is

guarded :: Constraint cs -> m a -> m a

where cs is a constraint store. Constraint stores are instances of the class CStore declaring an associated type of constraints and an operation for asserting a constraint in a monad.

class MonadPlus (Solver cs) => ConstraintStore cs
 where
  type Constraint cs
  type     Solver cs :: * -> *

  assert :: Constraint cs -> cs -> Solver cs cs

A constraint store has an associated solver monad which must be an instance of MonadPlus and assert may fail (i.e. yield mzero) if the constraint is inconsistent or branch (i.e. call mplus) to split the given constraint into different alternatives.

Constraint Monads and an Instance

The type class for constraint monads is parameterized by a constraint store. Apart from guarded it provides an operation solution that returns pairs of results and constraint stores in the solver monad of the constraint store.

class (MonadPlus m, CStore (Store m)) => MonadC m
 where
  type Store m

  guarded  :: Constraint cs -> m a -> m a
  solution :: m a -> Store m -> Solver (Store m) (a,Store m)

We won’t look at specific constraint stores but simply assume that we have an instance available.

Let’s try to make the datatype MP an instance of MonadC. Following the original design, we can simply add an additional constructor Guarded to the data-type declaration.

data CStore cs => MP cs a
  = ... | Guarded (Constraint cs) (MP cs a)

Before implementing the new operations of MonadC, we need to extend the implementation of (>>=).

instance Monad (MP cs)
 where
  ...
  Guarded c x >>= f = Guarded c (x >>= f)

That was easy! Note that no constraint store is threaded through the computation like in a state monad — the constraints are simply left untouched by the implementation of (>>=).

Now, we can make the extended version of MP an instance of MonadC. The operation guarded is implemented with the corresponding constructor. The interesting part is the implementation of solution.

instance CStore cs => MonadC (MP cs)
 where
  type Store (MP cs) = cs

  guarded = Guarded

  solution (Return x)    cs = return (x,cs)
  solution MZero         _  = mzero
  solution (MPlus x y)   cs = solution x cs `mplus` solution y cs
  solution (Guarded c x) cs = assert c cs >>= solution x

The constraint store is threaded through the computation of solution and constraints are asserted on the fly. An application of assert may fail or branch leading to additional non-determinism and failure compared to the original structure of the computation.

The solutions of a constrained computation are returned in the solver monad of the constraint store which can be an arbitrary instance of MonadPlus — possibly, but not necessarily MP.

Generalization

We have successfully defined an instance of a constraint monad by extending the underlying data type with a constructor for guarded computations. We can do the same for other instances of MonadPlus. However, it seems unfortunate to be forced to do the same work over and over again. For many instances of MonadPlus — like the list monad — it is not even possible to extend the data type, because we cannot change the module where it is implemented.

Hence, we would prefer being able to add constraints to every MonadPlus instance at once without having to change their underlying representation. How can we do this? We need a monad transformer!

We will not exactly define a monad transformer but something very similar. Instead of transforming an arbitrary instance of MonadPlus, we transform the solver monad of a constraint store — which can be an arbitrary instance of MonadPlus.

We define a data type Constr that is parameterized by a constraint store as follows.

newtype Constr cs a
  = Constr { runConstr :: Solver cs (Constrained cs a) }

data Constrained cs a
  = Lifted a
  | Guarded (Constraint cs) (Constr cs a)

Stare at these definitions for a minute and then cut the knots in your brain. The type (Constr cs) adds constraints to the monad (Solver cs) for any constraint store cs. Remember the original definition of the data type MP? Apart from the newtype constructor Constr that won’t be present at run time, values of type (Constr cs a) will have a mixture of MPlus and Guarded constructors as inner nodes just like the extended version of MP if MP is the solver monad of cs! Additionally, we need to add Lifted constructors to returned values and Return constructors around guarded values to satisfy the type checker.

Transforming Monads

If cs is a constraint store, then (Constr cs) is a monad. We only need to define return and (>>=) which is a bit tricky because of the interleaved types but no magic.

instance CStore cs => Monad (Constr cs)
 where
  return = Constr . return . Lifted

  x >>= f = Constr (runConstr x >>= bind)
   where
    bind (Lifted a)    = runConstr (f a)
    bind (Guarded c y) = return (Guarded c (y >>= f))

Just like previously, when extending MP, we leave the Guarded constructor untouched and simply descend into it’s argument.

(Constr cs) is also an instance of MonadPlus. The instance definition is straight forward — we only wrap and unwrap newtype constructors and reuse the operations of the solver monad.

instance CStore cs => MonadPlus (Constr cs)
 where
  mzero = Constr mzero

  x `mplus` y
    = Constr (runConstr x `mplus` runConstr y)

The interesting part of the instance definition for MonadC is again the implementation of the operation solution.

instance CStore cs => MonadC (Constr cs)
 where
  guarded c x = Constr (return (Guarded c x))

  solution x cs = runConstr x >>= solve
   where
    solve (Lifted a)    = return (a,cs)
    solve (Guarded c y) = assert c cs >>= solution y

Apart from translating between the interleaved types it resembles the original definition for the extended version of MP.

With these definitions, we get the functionality that we have implemented for MP for free for every instance of MonadPlus that is used as solver monad in a constraint store.

With the ideas described in this post, we can add arbitrary constraints to arbitrary instances of MonadPlus. As mentioned above, this enables us to express lazy non-deterministic computations with call-time choice semantics reusing existing instances of MonadPlus.

But that is a different story.