Lazy Non-Deterministic Data

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.


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


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


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


> class Narrowable a
> where
> unknown :: IDSupply is => is -> a

There are typed operations for failure, non-deterministic choice, and pattern matching.


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


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


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


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


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