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