This module defines type classes for constrained computations. It is written in a way that supports the use of Pandoc for rendering.

> {-# OPTIONS_GHC -XTypeFamilies -XFlexibleContexts #-}

>

> module Control.Monad.Constraint where

>

> import Control.Monad

> import Control.Monad.State

Constrained computations are parameterized by a constraint store. A constraint store has an associated type of stored constraints, and defines two functions to manipulate constraint stores.

The function `assert`

adds a constraint to the store. It might

*fail*if the given constraint is inconsistent w.r.t. the store, or*branch*if the given constraint can be split into different alternatives.

The function `labeling`

transforms a store with ambigious constraints into many stores with a unique solution (or none if the store is inconsistent).

Failure and branching of both functions is expressed in the solver monad of the constraint store which is an instance of `MonadPlus`

.

> class MonadPlus (Solver cs) => CStore cs

> where

> type Constraint cs

> type Solver cs :: * -> *

>

> noConstraints :: cs

> assert :: Constraint cs -> StateT cs (Solver cs) ()

> labeling :: StateT cs (Solver cs) ()

Constrained computations support operations for adding and solving constraints in an associated constraint store.

The function `(&>)`

yields a computation that is guarded by a given constraint. The function `solutions`

computes results of a constrained computation and possibly manipulates the constraint store. Therefore, solutions are returned in the solver monad of the constraint store extended by the state monad transformer.

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

> where

> type Store m

>

> (&>) :: Constraint (Store m) -> m a -> m a

> solution :: m a -> StateT (Store m) (Solver (Store m)) a

>

> liftC :: Solver (Store m) a -> m a

We can use `(&>)`

to define a `guard`

operation similar to the `guard`

operation of `MonadPlus`

.

> guardC :: MonadC m => Constraint (Store m) -> m ()

> guardC c = c &> return ()

If we have a constraint solver, we can extend its solver monad with guarded computations, i.e. define a `MonadC`

based on the solver monad.

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

>

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

The `return`

operation of `Constr cs`

lifts the `return`

operation of the corresponding solver monad. The bind operation leaves guards in place.

> 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))

The operations of `MonadPlus`

are simply lifted over the `newtype`

constructor.

> instance CStore cs => MonadPlus (Constr cs)

> where

> mzero = Constr mzero

>

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

Solutions are computed by successively asserting constraints into the constraint store.

> instance CStore cs => MonadC (Constr cs)

> where

> type Store (Constr cs) = cs

>

> c &> x = Constr (return (Guarded c x))

>

> solution x = lift (runConstr x) >>= solve

> where

> solve (Lifted a) = return a

> solve (Guarded c y) = do assert c; solution y

>

> liftC x = Constr (x >>= return . Lifted)