Constrained Monadic Computations

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

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)