Misc.hs

--------------------------------
-- Pretty Printing type class --
--------------------------------

class Pretty a where
  pretty :: a -> String
  pprint :: a -> IO ()
  pprint = putStrLn . pretty 

instance Pretty Int where
  pretty = show

instance Pretty Bool where
  pretty = show

instance Pretty a => Pretty (Identity a) where
  pretty = pretty . runIdentity
  
--------------------------------
-- Tree structure with labels --
--------------------------------
type ID = Int

data Tree a = Failed
            | Leaf a
            | Choice (Maybe ID) (Tree a) (Tree a)
  deriving Show

foldTree :: (a -> b) -> (Maybe ID -> b -> b -> b) -> b -> Tree a -> b
foldTree leafF choiceF e Failed = e
foldTree leafF choiceF e (Leaf x) = leafF x
foldTree leafF choiceF e (Choice ref t1 t2) =
    choiceF ref (foldTree leafF choiceF e t1) (foldTree leafF choiceF e t2)

instance Pretty a => Pretty (Tree a) where
  pretty t = pretty' t 0
   where
    pretty' Failed _ = "_|_"
    pretty' (Leaf x) _ = pretty x
    pretty' (Choice n t1 t2) wsp =
      show n ++ "\n" ++ replicate wsp ' ' ++ "|---- " ++ pretty' t1 (wsp+6)
             ++ "\n" ++ replicate wsp ' ' ++ "|---- " ++ pretty' t2 (wsp+6)

instance Functor Tree where
    fmap f Failed = Failed
    fmap f (Leaf x) = Leaf (f x)
    fmap f (Choice n t1 t2) = Choice n (fmap f t1) (fmap f t2)

instance Applicative Tree where
    pure = Leaf
    Failed <*> _ = Failed
    _ <*> Failed = Failed
    Leaf f <*> Leaf x = Leaf (f x)
    Choice n tf1 tf2 <*> tx = Choice n (tf1 <*> tx) (tf2 <*> tx)
    tf <*> Choice n t1 t2 = Choice n (tf <*> t1) (tf <*> t2)

instance Monad Tree where
    return = Leaf
    Failed >>= _ = Failed
    Leaf x >>= f = f x
    Choice n t1 t2 >>= f = Choice n (t1 >>= f) (t2 >>= f)

SharingDen.lhs

> {-# LANGUAGE GADTs #-}
> {-# LANGUAGE MultiParamTypeClasses #-}
> {-# LANGUAGE FlexibleInstances #-}
> {-# LANGUAGE StandaloneDeriving #-}
> 
> module SharingDen where
> 
> import Control.Applicative (Alternative(..))
> import Control.Monad (MonadPlus(..), ap)
> 
> import Misc hiding (Tree(..))
> import qualified Misc as T (Tree(..))
> import SharingInterface

This implementation strictly follows the laws presented in "Purely Functional Lazy Non-deterministic Programming" by Fischer et al.
They introduce the following laws for a monad with non-determinism (using `mplus`) and sharing (using `share`).

           share (a `mplus` b) = share a `mplus` share b                                    (1)
                   share mzero = return mzero                                               (2)
                     share _|_ = return _|_                                                 (3)
     share (ret (c x1 ... xn)) = share x1 >>= \y1 ...                                       (4)
                                 share xn >>= \yn . return (return (c y1 ... yn))

Ignoring the rule for non-termination (3) for now, we can define a representation for a monad with non-determinism and sharing by having all these constructs explicitly.

> data NDShare a where
>     Failed :: NDShare a
>     Leaf :: a -> NDShare a
>     Choice :: NDShare a -> NDShare a -> NDShare a
>     Share :: NDShare a -> NDShare (NDShare a)

The monad instance for this incarnation then directly follows the rules (1), (2) and (4) above and we use the fact that `Leaf` resembles `return`, `Choice` resemble `mplus` and `Failed` resembles `mzero`.

> instance Functor NDShare where
>     fmap f t = t >>= return . f
> 
> instance Applicative NDShare where
>     pure = return
>     (<*>) = ap
>
> instance Alternative NDShare where
>     (<|>) = choice
>     empty = failed
> 
> instance MonadPlus NDShare where
>     mplus = choice
>     mzero = failed
>
> instance Monad NDShare where
>     return = Leaf
>     Failed >>= f = Failed
>     Leaf x >>= f = f x
>     Choice t1 t2 >>= f =
>       let t1' = t1 >>= f in
>       let t2' = t2 >>= f in
>       Choice t1' t2'
>     Share (Choice t1 t2) >>= f =
>       let t1' = Share t1 >>= f in
>       let t2' = Share t2 >>= f in
>       Choice t1' t2'
>     Share t >>= f = Leaf t >>= f

The smart constructors are then not as smart as the name suggests but rather shortcuts for their corresponding constructors.
 
> share' :: NDShare a -> NDShare (NDShare a)
> share' t = Share t
> 
> choice :: NDShare a -> NDShare a -> NDShare a
> choice = Choice
> 
> failed :: NDShare a
> failed = Failed

We can then implement the `Sharing` type class by utilising rule (4) again that says that we need to apply `share` for all arguments of a constructor.
Wrapping all results into a common tree structure is a simple wrapping from the constructors above with the additional side-condition that all `Share` constructors are already transformed when computing the normal form of an expresion via `nf`.

> instance Sharing NDShare where
>     share ndx = share' (ndx >>= shareArgs share)
>
> instance AllValues NDShare where
>     allValues ndx = toNFTree (nf ndx)
>
> toNFTree :: NDShare a -> T.Tree a
> toNFTree Failed = T.Failed
> toNFTree (Leaf x) = T.Leaf x
> toNFTree (Choice t1 t2) = T.Choice Nothing (toNFTree t1) (toNFTree t2)
> toNFTree (Share _) = error "toNFTree: given tree was not in normal form"


> ----------------------------------------------
> -- type class instances for primitive types --
> ----------------------------------------------
> instance Monad m => Normalform m () () where
>     nf = id
> 
> instance Monad m => Normalform m Bool Bool where
>     nf = id
> 
> instance Monad m => Normalform m Int Int where
>     nf = id

A small example.

> instance Monad m => Normalform m Bool Bool where
>     nf = id
> 
> instance Sharing m => Shareable m Bool where
>    shareArgs _ = return
>   
> coin :: MonadPlus m => m Bool
> coin = return True `mplus` return False
> 
> orM :: Monad m => m Bool -> m Bool -> m Bool
> orM mb1 mb2 = mb1 >>= \b1 ->
>               case b1 of
>                 True -> return True
>                 False -> mb2
> 
> exOrF :: (Sharing m, MonadPlus m) => m Bool
> exOrF = share coin >>= \fx -> orM (return False) (orM fx fx)
> 
> exOrT :: (Sharing m, MonadPlus m) => m Bool
> exOrT = share coin >>= \fx -> orM (return True) (orM fx fx)

  λ> allValues (exOrF :: NDShare Bool) :: T.Tree Bool
  Choice Nothing (Leaf True) (Leaf False)
  λ> allValues (exOrT :: NDShare Bool) :: T.Tree Bool
  Choice Nothing (Leaf True) (Leaf True)

SharingInterface.hs

{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE RankNTypes #-}

module SharingInterface where

import Control.Monad.Trans.State ( State(..), state, get, put )
import Control.Monad (MonadPlus(..))

import qualified Data.Map as Map

import Misc

----------------------------
-- type class for sharing --
----------------------------

class MonadPlus s => Sharing (s :: * -> *) where
    share :: Shareable s a => s a -> s (s a)

class AllValues (s :: * -> *) where
    allValues :: Normalform s a b => s a -> Tree b

class Shareable m a where
  shareArgs :: Monad n => (forall b. Shareable m b => m b -> n (m b)) -> a -> n a

---------------------------
-- Normalform evaluation --
---------------------------

class Normalform m a b where
    nf :: m a -> m b

----------------------
-- Search algorithm --
----------------------
data Decision = L | R
type Memo = Map.Map ID Decision

dfs :: Memo -> Tree a -> [a]
dfs mem Failed = []
dfs mem (Leaf x) = [x]
dfs mem (Choice Nothing t1 t2) = dfs mem t1 ++ dfs mem t2
dfs mem (Choice (Just n) t1 t2) =
    case Map.lookup n mem of
      Nothing -> dfs (Map.insert n L mem) t1 ++ dfs (Map.insert n R mem) t2
      Just L -> dfs mem t1
      Just R -> dfs mem t2


dfsWithEmpty :: Tree a -> [a]
dfsWithEmpty = dfs Map.empty

--------------------------------------------------------
-- function to collect all values with respect to dfs --
--------------------------------------------------------

collectVals :: (AllValues m, Normalform m a b) => m a -> [b]
collectVals expr = dfsWithEmpty (allValues expr)