% Constraints for Call-Time Choice
% Sebastian Fischer ([sebf])
% October, 2008
This module implements a choice construct in a constrained monad. This
construct allows to implement functional-logic programs lazily because
shared choices are constrained to take the same branch. Internally, we
use a constraint store that associates unique identifiers to integers.
This module 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 #-}
>
> module Control.Monad.Constraint.Choice (
>
> module Control.Monad.Constraint.Choice, UniqSupply
>
> ) where
>
> import Control.Monad
> import Control.Monad.State
> import Control.Monad.Constraint
> import Data.IDSupply
~~~
We borrow unique identifiers from the GHC sources. You need to include
the package ghc-6.8.3 or similar to be able to import the necessary
modules.
~~~ {.literatehaskell}
> import Unique
> import UniqSupply
> import UniqFM
~~~
The `choice` function takes a supply of unique identifiers and yields
a choice in a monad that is constrained by `Choice`s.
~~~ {.literatehaskell}
> choice :: ( IDSupply is, MonadC m, Constraint (Store m) ~ Choice is )
> => is -> [m a] -> m a
> choice is xs = foldr1 mplus (mzero:zipWith ((&>).Choice i) [0..] xs)
> where i = idFromSupply is
~~~
GHC's `UniqSupply` is an instance of IDSupply.
~~~ {.literatehaskell}
> instance IDSupply UniqSupply
> where
> type ID UniqSupply = Unique
>
> initSupply = mkSplitUniqSupply 'x'
> splitSupply = splitUniqSupply
> idFromSupply = uniqFromSupply
~~~
The constraint store `Choices` is a `UniqFM` of choices. Constraints
are modeled as values of type `Choice`.
~~~ {.literatehaskell}
> newtype Choices (m :: * -> *) = CS (UniqFM Int)
>
> data Choice is = Choice (ID is) Int
~~~
The type `Choices` is an instance of the class `CStore`
and `Choice` is the associated type of constraints.
The function `assert` fails to insert a conflicting choice in the
store and possibly updates the store if the given choice constraint is
consistent.
The function `labeling` does not modify the store, as there are no
ambigous constraints in a store of choices.
~~~ {.literatehaskell}
> instance MonadPlus m => CStore (Choices m)
> where
> type Constraint (Choices m) = Choice UniqSupply
> type Solver (Choices m) = m
>
> noConstraints = CS emptyUFM
>
> assert (Choice u n) = do
> CS cs <- get
> case lookupUFM_Directly cs u of
> Nothing -> put (CS (addToUFM_Directly cs u n))
> Just n' -> guard (n==n')
>
> labeling = return ()
~~~
~~~ {.literatehaskell}
~~~