% Constrained Monadic Computations
% Sebastian Fischer ([sebf])
% October, 2008

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

[sebf]:       mailto:sebf@informatik.uni-kiel.de
[Pandoc]:     http://johnmacfarlane.net/pandoc/

~~~ {.literatehaskell}

> {-# 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`.

~~~ {.literatehaskell}

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

~~~ {.literatehaskell}

> 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`.

~~~ {.literatehaskell}

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

~~~ {.literatehaskell}

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

~~~ {.literatehaskell}

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

~~~ {.literatehaskell}

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

~~~ {.literatehaskell}

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

~~~