Constraints for Call-Time Choice

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.


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


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


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


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


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


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