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.