content: {-# LANGUAGE AllowAmbiguousTypes #-}
  {-# OPTIONS_HADDOCK not-home #-}
  module Control.Effect.Internal.Union where
  
  import Data.Coerce
  import Data.Kind (Constraint)
  
  import Control.Monad.Trans
  import Control.Monad.Trans.Reader (ReaderT)
  
  import Control.Effect.Internal.Membership
  import Control.Effect.Internal.Utils
  
  -- | The kind of effects.
  --
  -- Helpful for defining new effects:
  --
  -- @
  -- data InOut i o :: Effect where
  --   Input  :: InOut i o m i
  --   Output :: o -> InOut i o m ()
  -- @
  --
  type Effect = (Type -> Type) -> Type -> Type
  
  -- | An effect for collecting multiple effects into one effect.
  --
  -- Behind the scenes, 'Union' is the most important effect
  -- in the entire library, as the 'Control.Effect.Carrier' class is built
  -- around handling 'Union's of effects.
  --
  -- However, even outside of defining novel 'Control.Effect.Carrier' instances,
  -- 'Union' can be useful as an effect in its own right.
  -- 'Union' is useful for effect newtypes -- effects defined through creating a
  -- newtype over an existing effect.
  -- By making a newtype of 'Union', it's possible to wrap multiple effects in one
  -- newtype.
  --
  -- Not to be confused with 'Control.Effect.Bundle'.
  -- Unlike 'Control.Effect.Bundle', 'Union' is a proper effect that is given no
  -- special treatment by 'Control.Effect.Eff' or 'Control.Effect.Effs'.
  data Union (r :: [Effect]) m a where
    Union :: Coercible z m => ElemOf e r -> e z a -> Union r m a
  
  -- | An @'Algebra' r m@ desribes a collection of effect handlers for @m@ over
  -- all effects in the list @r@.
  type Algebra r m = forall x. Union r m x -> m x
  
  -- | A first-rank type which can often be used instead of 'Algebra'
  type Algebra' r m a = Union r m a -> m a
  
  -- | 'RepresentationalEff' is the constraint every effect is expected
  -- to satisfy: namely, that any effect @e m a@ is representational in @m@,
  -- which -- in practice -- means that no constraints are ever placed upon
  -- @m@ within the definion of @e@, and that @m@ isn't present in
  -- the return type of any action of @e@.
  --
  -- You don't need to make instances of 'RepresentationalEff'; the compiler
  -- will automatically infer if your effect satisfies it.
  --
  -- 'RepresentationalEff' is not a very serious requirement, and
  -- even effects that don't satisfy it can typically be rewritten into
  -- equally powerful variants that do.
  --
  -- If you ever encounter that an effect you've written doesn't satisfy
  -- 'RepresentationalEff', please consult
  -- [the wiki](https://github.com/KingoftheHomeless/in-other-words/wiki/Advanced-topics#making-effects-representationaleff).
  class    ( forall m n x. Coercible m n => Coercible (e m x) (e n x) )
        => RepresentationalEff (e :: Effect)
  instance ( forall m n x. Coercible m n => Coercible (e m x) (e n x) )
        => RepresentationalEff (e :: Effect)
  
  
  decomp :: RepresentationalEff e
         => Union (e ': r) m a
         -> Either (Union r m a) (e m a)
  decomp (Union Here e) = Right (coerce e)
  decomp (Union (There pr) e) = Left (Union pr e)
  {-# INLINE decomp #-}
  
  -- | Extract the only effect of an 'Union'.
  extract :: RepresentationalEff e
          => Union '[e] m a
          -> e m a
  extract (Union Here e) = coerce e
  extract (Union (There pr) _) = absurdMember pr
  {-# INLINE extract #-}
  
  weaken :: Union r m a -> Union (e ': r) m a
  weaken (Union pr e) = Union (There pr) e
  {-# INLINE weaken #-}
  
  absurdU :: Union '[] m a -> b
  absurdU (Union pr _) = case pr of {}
  {-# INLINE absurdU #-}
  
  
  -- | Weaken an 'Algebra' by removing the topmost effect.
  weakenAlg :: Algebra' (e ': r) m a -> Algebra' r m a
  weakenAlg alg u = alg (weaken u)
  {-# INLINE weakenAlg #-}
  
  -- | Strengthen an 'Algebra' by providing a handler for a new effect @e@.
  powerAlg :: forall e r m a
            . RepresentationalEff e
           => Algebra' r m a
           -> (e m a -> m a)
           -> Algebra' (e ': r) m a
  powerAlg alg h = powerAlg' alg (h .# coerce)
  {-# INLINE powerAlg #-}
  
  powerAlg' :: forall e r m a
             . Algebra' r m a
            -> (forall z. Coercible z m => e z a -> m a)
            -> Algebra' (e ': r) m a
  powerAlg' _ h (Union Here e) = h e
  powerAlg' alg _ (Union (There pr) e) = alg (Union pr e)
  {-# INLINEABLE powerAlg' #-}
  
  
  -- | Add a primitive effect and corresponding derived effect to a 'Reformulation'.
  addPrim :: forall e r p m z a
           . Monad z
          => Reformulation' r p m z a
          -> Reformulation' (e ': r) (e ': p) m z a
  addPrim reform n alg = powerAlg' (reform n (weakenAlg alg)) (alg . Union Here)
  {-# INLINE addPrim #-}
  
  -- | Lift an @m@-based 'Reformulation' to a @t m@-based 'Reformulation',
  -- where @t@ is any 'MonadTrans'
  liftReform
    :: (MonadTrans t, Monad m)
    => Reformulation' r p m z a
    -> Reformulation' r p (t m) z a
  liftReform reform = \n -> reform (n . lift)
  {-# INLINE liftReform #-}
  
  coerceReform :: Coercible m n
               => Reformulation' r p m z a
               -> Reformulation' r p n z a
  coerceReform reform n alg = coerce (reform (n .# coerce) alg)
  {-# INLINE coerceReform #-}
  
  -- | Weaken a 'Reformulation' by removing the topmost
  -- derived effect.
  weakenReform :: Reformulation' (e ': r) p m z a
               -> Reformulation' r p m z a
  weakenReform reform n alg = weakenAlg (reform n alg)
  {-# INLINE weakenReform #-}
  
  -- | A /less/ higher-rank variant of 'Reformulation', which is sometimes
  -- important.
  type Reformulation' r p m z a
    =  (forall x. m x -> z x)
    -> Algebra p z
    -> Algebra' r z a
  
  -- | The type of 'Control.Effect.Carrier.reformulate'.
  --
  -- A @'Reformulation' r p m@ describes how the derived effects @r@ are
  -- formulated in terms of the primitive effects @p@ and first-order operations
  -- of @m@.
  -- This is done by providing an @'Algebra' r z@ for any monad @z@ that lifts
  -- @m@ and implements an 'Algebra' over @p@.
  type Reformulation r p m
    =  forall z
     . Monad z
    => (forall x. m x -> z x)
    -> Algebra p z
    -> Algebra r z
  
  -- | An instance of 'ThreadsEff' represents the ability for a monad transformer
  -- @t@ to thread a primitive effect @e@ -- i.e. lift handlers of that effect.
  --
  -- Instances of 'ThreadsEff' are accumulated into entire stacks of primitive
  -- effects by 'Threads'.
  --
  -- You only need to make 'ThreadsEff' instances for monad transformers that
  -- aren't simply newtypes over existing monad transformers. You also don't need
  -- to make them for 'Control.Monad.Trans.Identity.IdentityT'.
  class RepresentationalEff e => ThreadsEff t e where
    threadEff :: Monad m
              => (forall x. e m x -> m x)
              -> e (t m) a
              -> t m a
  
  -- | @'Threads' t p@ is satisfied if @'ThreadsEff' t e@ instances are defined for
  -- each effect @e@ in @p@. By using the @'Threads' t p@ constraint, you're
  -- able to lift 'Algebra's over @p@ from any monad @m@ to @t m@. This is useful
  -- when defining custom 'Control.Effect.Carrier.Carrier' instances.
  --
  -- Note that you /should not/ place a @'Threads' t p@ constraint if @t@ is
  -- simply a newtype over an existsing monad transformer @u@ that already has
  -- 'ThreadsEff' instances defined for it. Instead, you should place a
  -- @'Threads' u p@ constraint, and use its 'thread' by coercing the resulting
  -- algebra from @'Algebra' p (u m)@ to @'Algebra' p (t m)@'.
  -- That way, you avoid having to define redundant 'ThreadsEff' instances for
  -- every newtype of a monad transformer.
  --
  -- 'Threads' forms the basis of /threading constraints/
  -- (see 'Control.Effect.Threaders'), and every threading constraint offered
  -- in the library makes use of 'Threads' in one way or another.
  class Threads t p where
    thread :: Monad m
           => Algebra p m
           -> Algebra p (t m)
  
  instance Threads t '[] where
    thread _ = absurdU
    {-# INLINE thread #-}
  
  instance (ThreadsEff t e, Threads t p) => Threads t (e ': p) where
    thread alg = powerAlg (thread (weakenAlg alg)) (threadEff (alg . Union Here))
    {-# INLINEABLE thread #-}
  
  -- | Inject an effect into a 'Union' containing that effect.
  inj :: Member e r => e m a -> Union r m a
  inj = Union membership
  {-# INLINE inj #-}
  
  -- | The most common threading constraint of the library, as it is emitted by
  -- @-Simple@ interpreters (interpreters that internally make use of
  -- 'Control.Effect.interpretSimple' or 'Control.Effect.reinterpretSimple').
  --
  -- 'ReaderThreads' accepts all the primitive effects
  -- (intended to be used as such) offered in this library.
  --
  -- Most notably, 'ReaderThreads' accepts @'Control.Effect.Unlift.Unlift' b@.
  class    (forall i. Threads (ReaderT i) p) => ReaderThreads p
  instance (forall i. Threads (ReaderT i) p) => ReaderThreads p
  
  coerceEff :: forall n m e a
             . (Coercible n m, RepresentationalEff e)
            => e m a
            -> e n a
  coerceEff = coerce
  {-# INLINE coerceEff #-}
  
  coerceAlg :: forall n m e a b
             . (Coercible n m, RepresentationalEff e)
            => (e m a -> m b)
            -> e n a -> n b
  coerceAlg = coerce
  {-# INLINE coerceAlg #-}
  
  -- | A pseudo-effect given special treatment by 'Control.Effect.Eff'
  -- and 'Control.Effect.Effs'.
  --
  -- An @'Control.Effect.Eff'/s@ constraint on
  -- @'Bundle' '[eff1, eff2, ... , effn]@
  -- will expand it into membership constraints for @eff1@ through @effn@.
  -- For example:
  --
  -- @
  -- 'Control.Effect.Error.Error' e = 'Bundle' '['Control.Effect.Error.Throw' e, 'Control.Effect.Error.Catch' e]
  -- @
  --
  -- so
  --
  -- @
  -- 'Control.Effect.Eff' ('Control.Effect.Error.Error' e) m = ('Control.Effect.Carrier' m, 'Control.Effect.Member' ('Control.Effect.Error.Throw' e) ('Control.Effect.Derivs' m), 'Control.Effect.Member' ('Control.Effect.Error.Catch' e) ('Control.Effect.Derivs' m))
  -- @
  --
  -- 'Bundle' should /never/ be used in any other contexts but within
  -- 'Control.Effect.Eff' and 'Control.Effect.Effs', as it isn't an actual effect.
  --
  -- Not to be confused with 'Control.Effect.Union.Union', which is a proper
  -- effect that combines multiple effects into one.
  data Bundle :: [Effect] -> Effect
  
  type family Append l r where
    Append '[] r = r
    Append (x ': l) r = x ': (Append l r)
  
  type family FlattenBundles (e :: [Effect]) :: [Effect] where
    FlattenBundles '[] = '[]
    FlattenBundles (Bundle bs ': es) = Append (FlattenBundles bs) (FlattenBundles es)
    FlattenBundles (e ': es) = e ': FlattenBundles es
  
  type family Members (es :: [Effect]) (r :: [Effect]) :: Constraint where
    Members '[] r = ()
    Members (e ': es) r = (Member e r, Members es r)
  
  type EffMembers (xs :: [Effect]) (r :: [Effect]) = Members (FlattenBundles xs) r
  