{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE EmptyDataDecls #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE PatternGuards #-}
{-# LANGUAGE DeriveDataTypeable, GeneralizedNewtypeDeriving, DeriveFunctor #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE NoMonomorphismRestriction #-}

-- | Original work available at: http://okmij.org/ftp/Hgetell/extensible/Eff.hs.
-- This module implements extensible effects as an alternative to monad transformers,
-- as described in http://okmij.org/ftp/Hgetell/extensible/exteff.pdf.
--
-- Extensible Effects are implemented as typeclass constraints on an Eff[ect] datatype.
-- A contrived example is:
--
--   -- Print a list of numbers, then print their sum.
--   printAndSum :: (Member (Lift IO) e, Member State e) => [Integer] -> Eff e Integer
--   printAndSum (x:xs) = do
--        lift $ putStrLn $ show x
--        onState (+ x)
--   printAndSum [] = getState >>= lift . putStrLn
module Control.Eff( Eff
                  , Member
                  , (:>)
                  , run
                  , send
                  , admin
                  , Reader
                  , runReader
                  , getReader
                  , local
                  , Trace
                  , trace
                  , runTrace
                  , Yield
                  , yield
                  , runC
                  , Y (..)
                  , State
                  , getState
                  , putState
                  , onState
                  , runState
                  , Choose
                  , choose
                  , runChoice
                  , Lift
                  , lift
                  , runLift
                  , Exc
                  , throwError
                  , runError
                  , catchError
                  , Fresh
                  , fresh
                  , runFresh
                  , CutFalse
                  , call
                  , cutfalse
                  ) where

import Control.Applicative (Applicative (..), (<$>))
import Control.Monad (join, ap)
import Data.OpenUnion1
import Data.Typeable

-- | A `VE` is either a value, or an effect of type `Union r` producing another `VE`.
-- The result is that a `VE` can produce an arbitrarily long chain of `Union r`
-- effects, terminated with a pure value.
data VE w r = Val w | E !(Union r (VE w r))

fromVal :: VE w r -> w
fromVal (Val w) = w
fromVal _ = error "fromVal E"

-- | A `Request w r a` consumes values of type `a`, and produces `VE w r`,
-- i.e. a `w` value embedded arbitrarily deep in `Union r` effects.
type Request w r a = a -> VE w r

-- Eff r a can consume a request (i.e. a -> VE w r)
newtype Eff r a = Eff { runEff :: forall w. Request w r a -> VE w r }

instance Functor (Eff r) where
    fmap f m = Eff $ \k -> runEff m (k . f)

instance Applicative (Eff r) where
    pure = return
    (<*>) = ap

instance Monad (Eff r) where
    {-# INLINE return #-}
    {-# INLINE (>>=) #-}
    return x = Eff $ \k -> k x
    m >>= f  = Eff $ \k -> runEff m (\v -> runEff (f v) k)

-- send a request and wait for a reply
send :: (forall w. (a -> VE w r) -> Union r (VE w r)) -> Eff r a
send f = Eff (E . f)

-- administer a client: launch a coroutine and wait for it
-- to send a request or terminate with a value
admin :: Eff r w -> VE w r
admin (Eff m) = m Val

-- ------------------------------------------------------------------------
-- The initial case, no effects

data Void -- no constructors

-- The type of run ensures that all effects must be handled:
-- only pure computations may be run.
run :: Eff Void w -> w
run = fromVal . admin
-- the other case is unreachable since Void has no constructors
-- Therefore, run is a total function if m Val terminates.

-- A convenient pattern: given a request (open union), either
-- handle it or relay it.
handleRelay :: Typeable1 t =>
     Union (t :> r) v -> (v -> Eff r a) -> (t v -> Eff r a) -> Eff r a
handleRelay u loop h = either passOn h $ decomp u
  where passOn u' = send (<$> u') >>= loop
  -- perhaps more efficient:
  -- passOn u' = send (\k -> fmap (\w -> runEff (loop w) k) u')

-- Add something like Control.Exception.catches? It could be useful
-- for control with cut.

interpose :: (Typeable1 t, Functor t, Member t r) =>
     Union r v -> (v -> Eff r a) -> (t v -> Eff r a) -> Eff r a
interpose u loop h = maybe (send (<$> u) >>= loop) h $ prj u

-- ------------------------------------------------------------------------
-- The Reader monad

-- | The request for a value of type e from the current environment.
-- This environment is analogous to a parameter of type e.
newtype Reader e v = Reader (e -> v)
    deriving (Typeable, Functor)

getReader :: Typeable e => Member (Reader e) r => Eff r e
getReader = send (inj . Reader)

-- | The handler of Reader requests. The return type shows that
-- all Reader requests are fully handled.
runReader :: Typeable e => Eff (Reader e :> r) w -> e -> Eff r w
runReader m e = loop (admin m) where
 loop (Val x) = return x
 loop (E u) = handleRelay u loop (\(Reader k) -> loop (k e))

-- | Locally rebind the value in the dynamic environment.
-- This function both requests and admins Reader requests.
local :: (Typeable e, Member (Reader e) r) =>
     (e -> e) -> Eff r a -> Eff r a
local f m = do
  e <- f <$> getReader
  let loop (Val x) = return x
      loop (E u) = interpose u loop (\(Reader k) -> loop (k e))
  loop (admin m)


-- ------------------------------------------------------------------------
-- Exceptions

-- exceptions of the type e; no resumption
newtype Exc e v = Exc e
    deriving (Functor, Typeable)

-- The type is inferred
throwError :: (Typeable e, Member (Exc e) r) => e -> Eff r a
throwError e = send (\_ -> inj $ Exc e)

runError :: Typeable e => Eff (Exc e :> r) a -> Eff r (Either e a)
runError m = loop (admin m)
 where
 loop (Val x)  = return (Right x)
 loop (E u)    = handleRelay u loop (\(Exc e) -> return (Left e))

-- The handler is allowed to rethrow the exception
catchError :: (Typeable e, Member (Exc e) r) =>
        Eff r a -> (e -> Eff r a) -> Eff r a
catchError m handle = loop (admin m)
 where
 loop (Val x)  = return x
 loop (E u)    = interpose u loop (\(Exc e) -> handle e)


-- ------------------------------------------------------------------------
-- Non-determinism (choice)

-- choose lst non-deterministically chooses one value from the lst
-- choose [] thus corresponds to failure
data Choose v = forall a. Choose [a] (a -> v)
              deriving (Typeable)

instance Functor Choose where
    fmap f (Choose lst k) = Choose lst (f . k)

choose :: Member Choose r => [a] -> Eff r a
choose lst = send (inj . Choose lst)

-- MonadPlus-like operators are expressible via choose

mzero' :: Member Choose r => Eff r a
mzero' = choose []

mplus' :: Member Choose r => Eff r a -> Eff r a -> Eff r a
mplus' m1 m2 = join $ choose [m1,m2]


-- The interpreter
runChoice :: forall a r. Eff (Choose :> r) a -> Eff r [a]
runChoice m = loop (admin m)
 where
 loop (Val x)  = return [x]
 loop (E u)    = handleRelay u loop (\(Choose lst k) -> handle lst k)
 -- Need the signature since local bindings aren't polymorphic any more
 handle :: [t] -> (t -> VE a (Choose :> r)) -> Eff r [a]
 handle [] _  = return []
 handle [x] k = loop (k x)
 handle lst k = concat <$> mapM (loop . k) lst


-- ------------------------------------------------------------------------
-- | Strict state.
-- Example:
-- Implementing Fresh in terms of State but not revealing that fact.
-- runFresh' :: (Typeable i, Enum i, Num i) => Eff (Fresh i :> r) w -> i -> Eff r w
-- runFresh' m s = fst <$> runState s (loop $ admin m)
--  where
--   loop (Val x) = return x
--   loop (E u)   = case decomp u of
--     Right (Fresh k) -> do
--                       n <- getState
--                       putState (n + 1)
--                       loop (k n)
--     Left u' -> send (\k -> unsafeReUnion $ k <$> u') >>= loop
data State s w = State (s -> s) (s -> w)
  deriving (Typeable, Functor)

putState :: Typeable e => Member (State e) r => e -> Eff r ()
putState = onState . const

getState :: Typeable e => Member (State e) r => Eff r e
getState = send (inj . State id)

onState :: (Typeable s, Member (State s) r) => (s -> s) -> Eff r ()
onState f = send (\k -> inj (State f (\_ -> k ())))

runState :: Typeable s => s -> Eff (State s :> r) w -> Eff r (w, s)
runState s0 = loop s0 . admin where
 loop s (Val x) = return (x, s)
 loop s (E u)   = handleRelay u (loop s) $
                       \(State t k) -> let s' = t s in s' `seq` loop s' (k s')

newtype Fresh i v = Fresh (i -> v)
    deriving (Functor, Typeable)

fresh :: (Typeable i, Enum i, Member (Fresh i) r) => Eff r i
fresh = send (inj . Fresh)

runFresh :: (Typeable i, Enum i) => Eff (Fresh i :> r) w -> i -> Eff r w
runFresh m s0 = loop s0 (admin m)
  where
    loop _ (Val x) = return x
    loop s (E u)   = handleRelay u (loop s) $
                          \(Fresh k) -> (loop $! succ s) (k s)


-- ------------------------------------------------------------------------
-- Tracing (debug printing)

data Trace v = Trace String (() -> v)
    deriving (Typeable, Functor)

-- Printing a string in a trace
trace :: Member Trace r => String -> Eff r ()
trace x = send (inj . Trace x)

-- The handler for IO request: a terminal handler
runTrace :: Eff (Trace :> Void) w -> IO w
runTrace m = loop (admin m) where
 loop (Val x) = return x
 loop (E u)   = prjForce u $ \(Trace s k) -> putStrLn s >> loop (k ())

-- ------------------------------------------------------------------------
-- Lifting: emulating monad transformers

data Lift m v = forall a. Lift (m a) (a -> v)

-- For ST monad, we have to define LiftST since (ST s) can't be Typeable:
-- s must be polymorphic without any constraints

{--
ghci 7.6.3 ==>
Eff.hs:465:29: Warning:
    In the use of `mkTyCon' (imported from Data.Typeable):
    Deprecated: "either derive Typeable, or use mkTyCon3 instead"
--}
instance Typeable1 m => Typeable1 (Lift m) where
    typeOf1 _ =
     mkTyConApp (mkTyCon3 "" "Eff" "Lift") [typeOf1 (undefined:: m ())]

instance Functor (Lift m) where
    fmap f (Lift m k) = Lift m (f . k)

-- | Lift a Monad to an Effect.
lift :: (Typeable1 m, Member (Lift m) r) => m a -> Eff r a
lift m = send (inj . Lift m)

-- | The handler of Lift requests. It is meant to be terminal: we only allow
-- a single Lifted Monad because Monads aren't commutative
-- (e.g. Maybe (IO a) is functionally different from IO (Maybe a)).
runLift :: (Monad m, Typeable1 m) => Eff (Lift m :> Void) w -> m w
runLift m = loop (admin m) where
 loop (Val x) = return x
 loop (E u) = prjForce u $ \(Lift m' k) -> m' >>= loop . k

-- ------------------------------------------------------------------------
-- Co-routines
-- The interface is intentionally chosen to be the same as in transf.hs

-- | The yield request: reporting the value of type e and suspending
-- the coroutine
-- (For simplicity, a co-routine reports a value but accepts unit)
data Yield a v = Yield a (() -> v)
    deriving (Typeable, Functor)

yield :: (Typeable a, Member (Yield a) r) => a -> Eff r ()
yield x = send (inj . Yield x)

-- | Status of a thread: done or reporting the value of the type a
-- (For simplicity, a co-routine reports a value but accepts unit)
data Y r a = Done | Y a (() -> Eff r (Y r a))

-- | Launch a thread and report its status.
runC :: Typeable a => Eff (Yield a :> r) w -> Eff r (Y r a)
runC m = loop (admin m) where
 loop (Val _) = return Done
 loop (E u)   = handleRelay u loop $
                 \(Yield x k) -> return (Y x (loop . k))


-- ------------------------------------------------------------------------
-- An example of non-trivial interaction of effects, handling of two
-- effects together
-- Non-determinism with control (cut)
-- For the explanation of cut, see Section 5 of Hinze ICFP 2000 paper.
-- Hinze suggests expressing cut in terms of cutfalse
--  ! = return () `mplus` cutfalse
-- where
--  cutfalse :: m a
-- satisfies the following laws
--   cutfalse >>= k  = cutfalse              (F1)
--   cutfalse | m    = cutfalse              (F2)
-- (note: m `mplus` cutfalse is different from cutfalse `mplus` m)
-- In other words, cutfalse is the left zero of both bind and mplus.
--
-- Hinze also introduces the operation call :: m a -> m a that
-- delimits the effect of cut: call m executes m. If the cut is
-- invoked in m, it discards only the choices made since m was called.
-- Hinze postulates the axioms of call:
--
--   call false = false                          (C1)
--   call (return a | m) = return a | call m     (C2)
--   call (m | cutfalse) = call m                (C3)
--   call (lift m >>= k) = lift m >>= (call . k) (C4)
--
-- call m behaves like m except any cut inside m has only a local effect,
-- he says.

-- Hinze noted a problem with the `mechanical' derivation of backtracing
-- monad transformer with cut: no axiom specifying the interaction of
-- call with bind; no way to simplify nested invocations of call.

-- We use exceptions for cutfalse
-- Therefore, the law ``cutfalse >>= k       = cutfalse''
-- is satisfied automatically since all exceptions have the above property.

data CutFalse = CutFalse deriving Typeable

cutfalse :: Member (Exc CutFalse) r => Eff r a
cutfalse = throwError CutFalse

-- The interpreter -- it is like reify . reflect with a twist
-- Compare this implementation with the huge implementation of call
-- in Hinze 2000 (Figure 9)
-- Each clause corresponds to the axiom of call or cutfalse.
-- All axioms are covered.
-- The code clearly expresses the intuition that call watches the choice points
-- of its argument computation. When it encounteres a cutfalse request,
-- it discards the remaining choicepoints.

-- It completely handles CutFalse effects but not non-determinism
call :: Member Choose r => Eff (Exc CutFalse :> r) a -> Eff r a
call m = loop [] (admin m) where
 loop jq (Val x) = return x `mplus'` next jq          -- (C2)
 loop jq (E u) = case decomp u of
    Right (Exc CutFalse) -> mzero'  -- drop jq (F2)
    Left u' -> check jq u'

 check jq u | Just (Choose [] _) <- prj u  = next jq  -- (C1)
 check jq u | Just (Choose [x] k) <- prj u = loop jq (k x)  -- (C3), optim
 check jq u | Just (Choose lst k) <- prj u = next $ map k lst ++ jq -- (C3)
 check jq u = send (<$> u) >>= loop jq      -- (C4)

 next []    = mzero'
 next (h:t) = loop t h