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

~~~