% Lazy Non-Deterministic Data % Sebastian Fischer (sebf@informatik.uni-kiel.de) This module provides a datatype with operations for lazy non-deterministic programming.
> {-# LANGUAGE
>       MultiParamTypeClasses,
>       FlexibleInstances,
>       FlexibleContexts,
>       TypeFamilies
>   #-}
>
> module Data.LazyNondet (
>
>   NormalForm, HeadNormalForm(..), mkHNF, Nondet(..),
>
>   ID, initID, WithUnique(..), 
>
>   Unknown(..), failure, oneOf, caseOf,
>
>   Data, normalForm
>
> ) where
>
> import Data.Data
> import Data.Generics.Twins ( gmapAccumT )
>
> import Control.Monad
> import Control.Monad.State
> import Control.Monad.Trans
> import Control.Monad.Constraint
> import Control.Monad.Constraint.Choice
>
> import Unique
> import UniqSupply
> import UniqFM
We borrow unique identifiers from the package `ghc` which is hidden by default.
> data NormalForm = NormalForm Constr [NormalForm]
>  deriving Show
The normal form of data is represented by the type `NormalForm` which defines a tree of constructors. The type `Constr` is a representation of constructors defined in the `Data.Generics` package. With generic programming we can convert between Haskell data types and the `NormalForm` type.
> data HeadNormalForm m = Cons DataType ConIndex [Untyped m]
> type Untyped m = m (HeadNormalForm m)
>
> mkHNF :: Constr -> [Untyped m] -> HeadNormalForm m
> mkHNF c args = Cons (constrType c) (constrIndex c) args
Data in lazy functional-logic programs is evaluated on demand. The evaluation of arguments of a constructor may lead to different non-deterministic results. Hence, we use a monad around every constructor in the head-normal form of a value. In head-normal forms we split the constructor representation into a representation of the data type and the index of the constructor, to enable pattern matching on the index.
> newtype Nondet m a = Typed { untyped :: Untyped m }
Untyped non-deterministic data can be phantom typed in order to define logic variables by overloading. The phantom type must be the Haskell data type that should be used for conversion. Threading Unique Identifiers ---------------------------- Non-deterministic computations need a supply of unique identifiers in order to constrain shared choices.
> type ID = UniqSupply
>
> initID :: IO ID
> initID = mkSplitUniqSupply 'x'
>
> class WithUnique a
>  where
>   type Mon a :: * -> *
>   type Typ a
>
>   withUnique :: a -> ID -> Nondet (Mon a) (Typ a)
>
> instance WithUnique (Nondet m a)
>  where
>   type Mon (Nondet m a) = m
>   type Typ (Nondet m a) = a
>
>   withUnique = const
>
> instance WithUnique a => WithUnique (ID -> a)
>  where
>   type Mon (ID -> a) = Mon a
>   type Typ (ID -> a) = Typ a
>
>   withUnique f us = withUnique (f vs) ws
>    where (vs,ws) = splitUniqSupply us
We provide an overloaded operation `withUnique` to simplify the distribution of unique identifiers when defining possibly non-deterministic operations. Non-deterministic operations have an additional argument for unique identifiers. The operation `withUnique` allows to consume an arbitrary number of unique identifiers hiding their generation. Conceptually, it has all of the following types at once: Nondet m a -> ID -> Nondet m a (ID -> Nondet m a) -> ID -> Nondet m a (ID -> ID -> Nondet m a) -> ID -> Nondet m a (ID -> ID -> ID -> Nondet m a) -> ID -> Nondet m a ... We make use of type families because GHC considers equivalent definitions with functional dependencies illegal due to the overly restrictive "coverage condition". Combinators for Functional-Logic Programming --------------------------------------------
> class Unknown a
>  where
>   unknown :: MonadConstr Choice m => ID -> Nondet m a
The application of `unknown` to a unique identifier represents a logic variable of the corresponding type.
> oneOf :: MonadConstr Choice m => [Nondet m a] -> ID -> Nondet m a
> oneOf xs us = Typed (choice (uniqFromSupply us) (map untyped xs))
The operation `oneOf` takes a list of non-deterministic values and returns a non-deterministic value that yields one of the elements in the given list.
> failure :: MonadPlus m => Nondet m a
> failure = Typed mzero
A failing computation could be defined using `oneOf`, but we provide a special combinator that does not need a supply of unique identifiers.
> caseOf :: (Monad m, MonadSolve cs m m)
>        => Nondet m a
>        -> (HeadNormalForm m -> cs -> Nondet m b)
>        -> cs -> Nondet m b
> caseOf x branch cs = Typed (do
>   (hnf,cs') <- runStateT (solve (untyped x)) cs
>   untyped (branch hnf cs'))
The `caseOf` operation is used for pattern matching and solves constraints associated to the head constructor of a non-deterministic value. An updated constraint store is passed to the computation of the branch function. Collected constraints are kept attached to the computed value by using an appropriate instance of `MonadSolve` that does not eliminate them. Converting Between Primitive and Non-Deterministic Data -------------------------------------------------------
> prim :: Data a => NormalForm -> a
> prim (NormalForm con args) =
>   snd (gmapAccumT perkid args (fromConstr con))
>  where
>   perkid (t:ts) _ = (ts, prim t)
>
> generic :: Data a => a -> NormalForm
> generic x = NormalForm (toConstr x) (gmapQ generic x)
>
> hnf :: Monad m => NormalForm -> Untyped m
> hnf (NormalForm con args) = return (mkHNF con (map hnf args))
>
> nondet :: (Monad m, Data a) => a -> Nondet m a
> nondet = Typed . hnf . generic
We provide generic operations to convert between instances of the `Data` class and non-deterministic data.
> normalForm :: (MonadSolve cs m m', Data a) => Nondet m a -> cs -> m' a
> normalForm x cs = liftM prim $ evalStateT (nf (untyped x)) cs
>
> nf :: MonadSolve cs m m' => Untyped m -> StateT cs m' NormalForm
> nf x = do
>   Cons typ idx args <- solve x
>   nfs <- mapM nf args
>   return (NormalForm (indexConstr typ idx) nfs)
The `normalForm` function evaluates a non-deterministic value and lifts all non-deterministic choices to the top level. The results are deterministic values and can be converted into their Haskell representation.
> instance Show (HeadNormalForm [])
>  where
>   show (Cons typ idx args) 
>     | null args = show con
>     | otherwise = unwords (("("++show con):map show args++[")"])
>    where con = indexConstr typ idx
>
> instance Show (Nondet [] a)
>  where
>   show = show . untyped
>
> instance Show (Nondet (ConstrT cs []) a)
>  where
>   show = show . untyped
>
> instance Show (HeadNormalForm (ConstrT cs []))
>  where
>   show (Cons typ idx [])   = show (indexConstr typ idx)
>   show (Cons typ idx args) =
>     "("++show (indexConstr typ idx)++" "++unwords (map show args)++")" 
To simplify debugging, we provide `Show` instances for head-normal forms and non-deterministic values.