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)