-- This snippet simulates naive dictionary passing for Curry type
-- classes using the explicit-sharing package for functional logic
-- programming in Haskell.
--
-- It defines a dictionary for the class
--
--   class Arb a where arb :: a
--
-- and a corresponding instance for the type Bool
--
--   instance Arb Bool where arb = False ? True
--
-- See Curry mailing list thread started by Wolfgang Lux on Aug 28, 2009.
--
-- After simulating the naive dictionary passing, we adjust the
-- sharing behaviour of the dictionary data type and investigate the
-- such non-sharing types further.
 
{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances #-}
 
import Control.Monad.Sharing
import Data.Monadic.List
 
-- first we need some boilerplate for nondeterministic booleans and pairs
data Pair m a b = Pair (m a) (m b)
 
instance (Monad m, Shareable m a, Shareable m b) => Shareable m (Pair m a b)
 where
  shareArgs f (Pair x y) = return Pair `ap` f x `ap` f y
 
instance (Monad m, Convertible m a c, Convertible m b d)
      => Convertible m (Pair m a b) (c,d)
 where
  convArgs f (Pair x y) = return (,) `ap` (f =<< x) `ap` (f =<< y)
 
-- now we define the dictionary
data Arb m a = Arb (m a)
 
instance (Monad m, Shareable m a) => Shareable m (Arb m a)
 where
  -- the usual implementation of shareArgs:
  -- shareArgs f (Arb x) = return Arb `ap` f x
 
  -- an alternative version that does not share recursively
  shareArgs _ = return
 
-- arb (Arb x) = x
arb :: Monad m => m (Arb m a) -> m a
arb m = m >>= \x -> case x of Arb y -> y
 
-- instArbBool = (Arb arbBool)
instArbBool :: MonadPlus m => m (Arb m Bool)
instArbBool = return (Arb arbBool)
 
-- arbBool = False ? True
arbBool :: MonadPlus m => m Bool
arbBool = return False `mplus` return True
 
-- arbP2 da db = (arb da, arb db)
arbP2 :: Monad m => m (Arb m a) -> m (Arb m b) -> m (Pair m a b)
arbP2 da db = return (Pair (arb da) (arb db))
 
-- arbL2 da = [arb da, arb da]
arbL2 :: (Monad m, Shareable m a, Sharing m) => m (Arb m a) -> m (List m a)
arbL2 da = do d <- share da
              cons (arb d) (cons (arb d) nil)
 
-- test functions
 
arbP2Bool :: [(Bool,Bool)]
arbP2Bool = evalLazy (arbP2 instArbBool instArbBool)
 
-- with the usual Shareable instance this yields two results with the
-- version that does not share recursively it yields four.
arbL2Bool :: [[Bool]]
arbL2Bool = evalLazy (arbL2 instArbBool)
 
-- How about nesting? We define two types similar to the Arb
-- dictionary. One specifies its argument to be evaluated using
-- call-time choice, the other uses the eval-time choice with the
-- syntax proposed by Wolfgang.
--
-- data CTC a = CTC a
-- data ETC a = ETC ?a
 
data CTC m a = CTC (m a)
data ETC m a = ETC (m a)
 
-- the difference between ETC and CTC can be seen in their Shareable
-- instances
 
instance (Monad m, Shareable m a) => Shareable m (CTC m a)
 where
  -- the argument of CTC is shared recursively 
  shareArgs f (CTC x) = return CTC `ap` f x
 
instance (Monad m, Shareable m a) => Shareable m (ETC m a)
 where
  -- the argument of ETC is not shared recursively 
  shareArgs _ (ETC x) = return (ETC x)
 
-- Boilerlate again: in order to observe the results of computations
-- that produce values of type 'CTC a' or 'ETC a' we define a
-- corresponding non-monadic type and associated Convertible
-- instances.
 
data Res a = Res a deriving Show
 
instance (Monad m, Convertible m a b) => Convertible m (CTC m a) (Res b)
 where convArgs f (CTC x) = return Res `ap` (f =<< x)
 
instance (Monad m, Convertible m a b) => Convertible m (ETC m a) (Res b)
 where convArgs f (ETC x) = return Res `ap` (f =<< x)
 
-- here is a simple function that allows to detect sharing:
--
-- dup x = (x,x)
dup :: (Monad m, Sharing m, Shareable m a) => m a -> m (Pair m a a)
dup x = do y <- share x
           return (Pair y y)
 
-- We can observe the difference between ETC and CTC by wrapping
-- arbBool inside them and passing the result to dup.
 
ctcCoin :: MonadPlus m => m (CTC m Bool)
ctcCoin = return (CTC arbBool)
 
etcCoin :: MonadPlus m => m (ETC m Bool)
etcCoin = return (ETC arbBool)
 
-- dup (CTC arbBool) ~> two results
ctcArgsAreShared :: [(Res Bool,Res Bool)]
ctcArgsAreShared = evalLazy (dup ctcCoin)
 
-- dup (ETC arbBool) ~> four results
etcArgsAreNotShared :: [(Res Bool,Res Bool)]
etcArgsAreNotShared = evalLazy (dup etcCoin)
 
-- Here is a function that demonstrates sharing inside the ETC constructor
--
-- shareInside :: Bool -> (ETC (Bool,Bool), ETC (Bool,Bool))
-- shareInside x = dup (ETC (x,x))
shareInside :: (MonadPlus m, Sharing m)
            => m Bool
            -> m (Pair m (ETC m (Pair m Bool Bool)) (ETC m (Pair m Bool Bool)))
shareInside x = do y <- share x
                   dup (return (ETC (return (Pair y y))))
 
sharedETCargsRemainShared :: [(Res (Bool,Bool),Res (Bool,Bool))]
sharedETCargsRemainShared = evalLazy (shareInside arbBool)
 
-- Bernds examples:
 
-- data ETC2 a = ETC2 ?a ?a
-- data ETC3 a = ETC3 ?a a
 
data ETC2 m a = ETC2 (m a) (m a)
data ETC3 m a = ETC3 (m a) (m a)
 
data Res2 a = Res2 a a
 
instance (Monad m, Shareable m a) => Shareable m (ETC2 m a)
 where
  shareArgs _ (ETC2 x y) = return (ETC2 x y)
 
instance (Monad m, Shareable m a) => Shareable m (ETC3 m a)
 where
  shareArgs f (ETC3 x y) = return ETC3 `ap` return x `ap` f y
 
instance (Monad m, Convertible m a b) => Convertible m (ETC2 m a) (Res2 b)
 where
  convArgs f (ETC2 x y) = return Res2 `ap` (f =<< x) `ap` (f =<< y)
 
instance (Monad m, Convertible m a b) => Convertible m (ETC3 m a) (Res2 b)
 where
  convArgs f (ETC3 x y) = return Res2 `ap` (f =<< x) `ap` (f =<< y)
 
f2 :: (Monad m, Sharing m) => m Int -> m (ETC2 m Int)
f2 x = do y <- share x
          return (ETC2 y y)
 
f3 :: (Monad m, Sharing m) => m Int -> m (ETC3 m Int)
f3 x = do y <- share x
          return (ETC3 y y)
 
plus2 :: Monad m => m (ETC2 m Int) -> m Int
plus2 m = m >>= \ (ETC2 x y) -> liftM2 (+) x y
 
plus3 :: Monad m => m (ETC3 m Int) -> m Int
plus3 m = m >>= \ (ETC3 x y) -> liftM2 (+) x y
 
test2 :: [Int]
test2 = evalLazy (plus2 (f2 (return 0 `mplus` return 1)))
 
test3 :: [Int]
test3 = evalLazy (plus3 (f3 (return 0 `mplus` return 1)))
 
-- another example by Bernd:
 
data C m a = C (m a)
 
instance (Monad m, Shareable m a) => Shareable m (C m a)
 where 
  shareArgs _ = return
 
plus :: Monad m => m (C m Int) -> m (C m Int) -> m Int 
plus a b = a >>= \ (C c) ->
           b >>= \ (C d) ->
           c >>= \ x     ->
           d >>= \ y     ->
           return (x+y)
 
cnst :: Monad m => m a -> m b -> m a
cnst x _ = x
 
e1, e2, e3 :: (MonadPlus m, Sharing m) => m Int
e1 = share (return (C (return 0 `mplus` return 1))) >>= \x -> plus x x
 
-- y is not shared (does not occur more than once)
e2 = let y = return 0 `mplus` return 1
      in share (return (C y)) >>= \x -> plus x x
 
-- now, y is shared
e3 = share (return 0 `mplus` return 1) >>= \y ->
     share (return (C y)) >>= \x -> cnst (plus x x) y
 
-- *Main> evalLazy e1 :: [Int]
-- [0,1,1,2]
-- *Main> evalLazy e2 :: [Int]
-- [0,1,1,2]
-- *Main> evalLazy e3 :: [Int]
-- [0,2]