content: {-# LANGUAGE TypeFamilies #-}
  {-# LANGUAGE UndecidableInstances #-}
  {-# LANGUAGE DataKinds #-}
  {-# LANGUAGE FlexibleContexts #-}
  {-# LANGUAGE GADTs #-}
  {-# LANGUAGE NoMonomorphismRestriction #-}
  {-# LANGUAGE RankNTypes #-}
  {-# LANGUAGE ScopedTypeVariables #-}
  {-# LANGUAGE TypeOperators #-}
  {-# LANGUAGE Trustworthy #-}
  -- | Lazy state effect
  module Control.Eff.State.OnDemand where
  
  import Control.Eff
  import Control.Eff.Extend
  
  import Control.Eff.Writer.Lazy
  import Control.Eff.Reader.Lazy
  import qualified Control.Eff.State.Lazy as S
  
  import Control.Monad.Base
  import Control.Monad.Trans.Control
  
  import Data.Function (fix)
  
  -- ------------------------------------------------------------------------
  -- | State, lazy (i.e., on-demand)
  --
  -- Extensible effects make it clear that where the computation is delayed
  -- (which I take as an advantage) and they do maintain the degree of
  -- extensibility (the delayed computation must be effect-closed, but the
  -- whole computation does not have to be).
  data OnDemandState s v where
    Get  :: OnDemandState s s
    Put  :: s -> OnDemandState s ()
    Delay :: Eff '[OnDemandState s] a  -> OnDemandState s a --  Eff as a transformer
  
  -- | Given a continuation, respond to requests
  instance Handle (OnDemandState s) r a (s -> k) where
    handle h q sreq s = case sreq of
      Get     -> h (q ^$ s) s
      Put s'  -> h (q ^$ ()) s'
      Delay m -> let ~(x, s') = run $ (fix (handle_relay S.withState)) m s
                                in h (q ^$ x) s'
  
  instance ( MonadBase m m
           , LiftedBase m r
           ) => MonadBaseControl m (Eff (OnDemandState s ': r)) where
      type StM (Eff (OnDemandState s ': r)) a = StM (Eff r) (a,s)
      liftBaseWith f = do s <- get
                          raise $ liftBaseWith $ \runInBase ->
                            f (runInBase . runState s)
      restoreM x = do (a, s :: s) <- raise (restoreM x)
                      put s
                      return a
  
  
  -- | Return the current value of the state. The signatures are inferred
  {-# NOINLINE get #-}
  get :: Member (OnDemandState s) r => Eff r s
  get = send Get
  {-# RULES
    "get/bind" forall k. get >>= k = send Get >>= k
   #-}
  
  -- | Write a new value of the state.
  {-# NOINLINE put #-}
  put :: Member (OnDemandState s) r => s -> Eff r ()
  put s = send (Put s)
  {-# RULES
    "put/bind"     forall k v. put v >>= k = send (Put v) >>= k
   #-}
  {-# RULES
    "put/semibind" forall k v. put v >>  k = send (Put v) >>= (\() -> k)
   #-}
  -- The purpose of the rules is to expose send, which is then being
  -- fuzed by the send/bind rule. The send/bind rule is very profitable!
  -- These rules are essentially inlining of get/put. Somehow GHC does not
  -- inline get/put, even if I put the INLINE directives and play with phases.
  -- (Inlining works if I use 'inline' explicitly).
  
  onDemand :: Member (OnDemandState s) r => Eff '[OnDemandState s] v -> Eff r v
  onDemand = send . Delay
  
  -- | Run a State effect
  runState :: s                            -- ^ Initial state
           -> Eff (OnDemandState s ': r) w -- ^ Effect incorporating State
           -> Eff r (w,s)                  -- ^ Effect containing final state and a return value
  runState s m = fix (handle_relay S.withState) m s
  
  -- | Transform the state with a function.
  modify :: (Member (OnDemandState s) r) => (s -> s) -> Eff r ()
  modify f = get >>= put . f
  
  -- | Run a State effect, discarding the final state.
  evalState :: s -> Eff (OnDemandState s ': r) w -> Eff r w
  evalState s = fmap fst . runState s
  
  -- | Run a State effect and return the final state.
  execState :: s -> Eff (OnDemandState s ': r) w -> Eff r s
  execState s = fmap snd . runState s
  
  -- | A different representation of State: decomposing State into mutation
  -- (Writer) and Reading. We don't define any new effects: we just handle the
  -- existing ones.  Thus we define a handler for two effects together.
  runStateR :: s -> Eff (Writer s ': Reader s ': r) w -> Eff r (w,s)
  runStateR s (Val x) = S.withState x s
  runStateR s (E q u) = case u of
    U0 (Tell w) -> handle loop q (S.Put w) s
    U1 (U0 Ask) -> handle loop q S.Get s
    U1 (U1 u') -> relay loop q u' s
    where loop = flip runStateR
  
  -- | Backwards state
  -- The overall state is represented with two attributes: the inherited
  -- getAttr and the synthesized putAttr.
  -- At the root node, putAttr becomes getAttr, tying the knot.
  -- As usual, the inherited attribute is the argument (i.e., the @environment@)
  -- and the synthesized is the result of the handler |go| below.
  runStateBack0 :: Eff '[OnDemandState s] a -> (a,s)
  runStateBack0 m =
    let (x,s) = go m s in
    (x,s)
   where
     go :: Eff '[OnDemandState s] a -> s -> (a,s)
     go (Val x) s = (x,s)
     go (E q u) s0 = case decomp u of
       Right Get      -> k s0 s0
       Right (Put s1)  -> let ~(x,sp) = k () sp in (x,s1)
       Right (Delay m1) -> let ~(x,s1) = go m1 s0 in k x s1
       Left _ -> error "Impossible happened: Nothing to relay!"
       where
         k = qComp q go
  
  -- | Another implementation, exploring Haskell's laziness to make putAttr
  -- also technically inherited, to accumulate the sequence of
  -- updates. This implementation is compatible with deep handlers, and
  -- lets us play with different notions of backwardness.
  runStateBack :: Eff '[OnDemandState s] a -> (a,s)
  runStateBack m =
    let (x,(_,sp)) = run $ go m (sp,[]) in
    (x,head sp)
   where
     go :: Eff '[OnDemandState s] a -> ([s],[s]) -> Eff '[] (a,([s],[s]))
     go = fix (handle_relay' hdl S.withState)
     hdl h q Get s0@(sg, _) = h (q ^$ head sg) s0
     hdl h q (Put s1) (sg, sp) = h (q ^$ ()) (tail sg,sp++[s1])
     hdl h q (Delay m1) s0 = let ~(x,s1) = run $ go m1 s0 in h (q ^$ x) s1
  
  -- ^ A different notion of backwards is realized if we change the Put handler
  -- slightly. How?
  