% Lazy Non-Deterministic Data
% Sebastian Fischer ([sebf])
% October, 2008
This module implements a data type for lazy, non-deterministic
programming. It could be used to implement functional-logic programs
in Haskell.
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 -XFlexibleInstances -XRankNTypes #-}
>
> module Data.LazyNondet (
>
> module Data.IDSupply, MonadPlus,
> MonadC, Constraint, Store, Solver, Constr,
> Choices, Choice, UniqSupply,
>
> Untyped(Cons), -- :: (* -> *) -> *
> Typed(..), -- :: * -> (* -> *) -> *
>
> Narrowable, -- type class
>
> unknown, -- :: (Narrowable a, IDSupply is) => is -> a
>
> failure, -- :: MonadC m => Typed a m
>
> oneOf, -- :: (IDSupply is, MonadC m, Constraint (Store m) ~ Choice is)
> -- => is -> [Typed a m] -> Typed a m
>
> caseOf, -- :: MonadC m
> -- => Store m -> Typed a m
> -- -> (Store m -> Untyped m -> Typed b m) -> Typed b m
>
> eval, -- :: (MonadC m, Monad i)
> -- => Typed a m -> Solver (Store m) (Typed a i)
>
> evalPrint
>
> ) where
>
> import Control.Monad
> import Control.Monad.State
> import Control.Monad.Identity
> import Control.Monad.Constraint
> import Control.Monad.Constraint.Choice
>
> import Data.IDSupply
>
> import Data.Char ( toLower )
~~~
The data type `Untyped` for non-deterministic values is parameterized
by a monad in which arguments of constructors are computed.
~~~ {.literatehaskell}
> data Untyped m = Cons ConsName [m (Untyped m)]
> type ConsName = Int
~~~
Untyped non-deterministic data can be phantom typed in order to be
able to define different instances for the class `Narrowable`.
~~~ {.literatehaskell}
> newtype Typed a m = Typed { unTyped :: m (Untyped m) }
~~~
`Narrowable` types support the operation `unknown` that takes a supply
of unique identifiers and returns a logic variable of the
corresponding type.
~~~ {.literatehaskell}
> class Narrowable a
> where
> unknown :: IDSupply is => is -> a
~~~
There are typed operations for failure, non-deterministic choice, and
pattern matching.
~~~ {.literatehaskell}
> failure :: MonadC m => Typed a m
> failure = Typed mzero
>
> oneOf :: (IDSupply is, MonadC m, Constraint (Store m) ~ Choice is)
> => is -> [Typed a m] -> Typed a m
> oneOf is xs = Typed (choice is (map unTyped xs))
>
> caseOf :: MonadC m
> => Store m -> Typed a m -> (Store m -> Untyped m -> Typed b m)
> -> Typed b m
> caseOf cs x branch = Typed (match cs (unTyped x) ((unTyped .).branch))
> match :: MonadC m
> => Store m -> m (Untyped m) -> (Store m -> Untyped m -> m (Untyped m))
> -> m (Untyped m)
> match cs x branch = do
> (y,cs') <- liftC (runStateT (solution x) cs)
> branch cs' y
~~~
The `eval` function computes the non-deterministic values of an
action in a constrained monad that yields non-deterministic
data.
As arguments of normal forms are deterministic, we usually use the
`Identity` monad for `i` in the type of `eval`.
~~~ {.literatehaskell}
> eval :: MonadC m => Typed a m -> Solver (Store m) (Typed a Identity)
> eval x = do
> (x,cs) <- runStateT (normalForm (unTyped x)) noConstraints
> cs' <- execStateT labeling cs -- cs' may be used later to manipulate x
> return (Typed (return x))
~~~
The function `normalForm` computes the non-deterministic normal forms
of an untyped non-deterministic lazy value. We usually use the
`Identity` monad as parameter to `Untyped` because arguments of normal
forms are deterministic.
~~~ {.literatehaskell}
> normalForm :: (MonadC m, Monad i)
> => m (Untyped m) -> StateT (Store m) (Solver (Store m)) (Untyped i)
> normalForm x = do
> Cons n xs <- solution x
> ys <- mapM normalForm xs
> return (Cons n (map return ys))
~~~
Interactive eval-print loop.
~~~ {.literatehaskell}
> evalPrint :: MonadPlus m
> => (forall b . m b -> [b])
> -> (UniqSupply -> Choices m -> Typed a (Constr (Choices m)))
> -> IO ()
> evalPrint enumerate goal = do
> is <- initSupply
> loop (enumerate (eval (goal is noConstraints)))
> where
> loop [] = putStrLn "No more solutions."
> loop (x:xs) = do
> print x
> putStr "more? [Y|n]: "
> l <- getLine
> if null l || 'y' == toLower (head l)
> then loop xs else return ()
~~~
Ad-hoc `Show` instances for normal forms.
~~~ {.literatehaskell}
> instance Show (Typed a Identity)
> where
> show = show . runIdentity . unTyped
> instance Show (Untyped Identity)
> where
> show (Cons name args) =
> "(C" ++ foldr (++) ")" (show name:map (show . runIdentity) args)
~~~