{-# 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 = (* -> *) -> * -> *

-- | 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 (e : r) m a -> Either (Union r m a) (e m a)
decomp (Union ElemOf e (e : r)
Here e z a
e) = e m a -> Either (Union r m a) (e m a)
forall a b. b -> Either a b
Right (e z a -> e m a
coerce e z a
e)
decomp (Union (There ElemOf e r
pr) e z a
e) = Union r m a -> Either (Union r m a) (e m a)
forall a b. a -> Either a b
Left (ElemOf e r -> e z a -> Union r m a
forall (z :: * -> *) (m :: * -> *) (e :: Effect) (r :: [Effect]) a.
Coercible z m =>
ElemOf e r -> e z a -> Union r m a
Union ElemOf e r
pr e z a
e)
{-# INLINE decomp #-}

-- | Extract the only effect of an 'Union'.
extract :: RepresentationalEff e
        => Union '[e] m a
        -> e m a
extract :: Union '[e] m a -> e m a
extract (Union ElemOf e '[e]
Here e z a
e) = e z a -> e m a
coerce e z a
e
extract (Union (There ElemOf e r
pr) e z a
_) = ElemOf e '[] -> e m a
forall a (e :: a) b. ElemOf e '[] -> b
absurdMember ElemOf e r
ElemOf e '[]
pr
{-# INLINE extract #-}

weaken :: Union r m a -> Union (e ': r) m a
weaken :: Union r m a -> Union (e : r) m a
weaken (Union ElemOf e r
pr e z a
e) = ElemOf e (e : r) -> e z a -> Union (e : r) m a
forall (z :: * -> *) (m :: * -> *) (e :: Effect) (r :: [Effect]) a.
Coercible z m =>
ElemOf e r -> e z a -> Union r m a
Union (ElemOf e r -> ElemOf e (e : r)
forall a (e :: a) (r :: [a]) (_e :: a).
ElemOf e r -> ElemOf e (_e : r)
There ElemOf e r
pr) e z a
e
{-# INLINE weaken #-}

absurdU :: Union '[] m a -> b
absurdU :: Union '[] m a -> b
absurdU (Union ElemOf e '[]
pr e z a
_) = case ElemOf e '[]
pr of {}
{-# INLINE absurdU #-}


-- | Weaken an 'Algebra' by removing the topmost effect.
weakenAlg :: Algebra' (e ': r) m a -> Algebra' r m a
weakenAlg :: Algebra' (e : r) m a -> Algebra' r m a
weakenAlg Algebra' (e : r) m a
alg Union r m a
u = Algebra' (e : r) m a
alg (Union r m a -> Union (e : r) m a
forall (r :: [Effect]) (m :: * -> *) a (e :: Effect).
Union r m a -> Union (e : r) m a
weaken Union r m a
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 :: Algebra' r m a -> (e m a -> m a) -> Algebra' (e : r) m a
powerAlg Algebra' r m a
alg e m a -> m a
h = Algebra' r m a
-> (forall (z :: * -> *). Coercible z m => e z a -> m a)
-> Algebra' (e : r) m a
forall (e :: Effect) (r :: [Effect]) (m :: * -> *) a.
Algebra' r m a
-> (forall (z :: * -> *). Coercible z m => e z a -> m a)
-> Algebra' (e : r) m a
powerAlg' Algebra' r m a
alg (e m a -> m a
h (e m a -> m a) -> (e z a -> e m a) -> e z a -> m a
forall b a c. Coercible b a => (b -> c) -> (a -> b) -> a -> c
.# e z a -> e m a
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' :: Algebra' r m a
-> (forall (z :: * -> *). Coercible z m => e z a -> m a)
-> Algebra' (e : r) m a
powerAlg' Algebra' r m a
_ forall (z :: * -> *). Coercible z m => e z a -> m a
h (Union ElemOf e (e : r)
Here e z a
e) = e z a -> m a
forall (z :: * -> *). Coercible z m => e z a -> m a
h e z a
e z a
e
powerAlg' Algebra' r m a
alg forall (z :: * -> *). Coercible z m => e z a -> m a
_ (Union (There ElemOf e r
pr) e z a
e) = Algebra' r m a
alg (ElemOf e r -> e z a -> Union r m a
forall (z :: * -> *) (m :: * -> *) (e :: Effect) (r :: [Effect]) a.
Coercible z m =>
ElemOf e r -> e z a -> Union r m a
Union ElemOf e r
pr e z a
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 :: Reformulation' r p m z a -> Reformulation' (e : r) (e : p) m z a
addPrim Reformulation' r p m z a
reform forall x. m x -> z x
n Algebra (e : p) z
alg = Algebra' r z a
-> (forall (z :: * -> *). Coercible z z => e z a -> z a)
-> Algebra' (e : r) z a
forall (e :: Effect) (r :: [Effect]) (m :: * -> *) a.
Algebra' r m a
-> (forall (z :: * -> *). Coercible z m => e z a -> m a)
-> Algebra' (e : r) m a
powerAlg' (Reformulation' r p m z a
reform forall x. m x -> z x
n (Algebra' (e : p) z x -> Algebra' p z x
forall (e :: Effect) (r :: [Effect]) (m :: * -> *) a.
Algebra' (e : r) m a -> Algebra' r m a
weakenAlg Algebra' (e : p) z x
Algebra (e : p) z
alg)) (Union (e : p) z a -> z a
Algebra (e : p) z
alg (Union (e : p) z a -> z a)
-> (e z a -> Union (e : p) z a) -> e z a -> z a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ElemOf e (e : p) -> e z a -> Union (e : p) z a
forall (z :: * -> *) (m :: * -> *) (e :: Effect) (r :: [Effect]) a.
Coercible z m =>
ElemOf e r -> e z a -> Union r m a
Union ElemOf e (e : p)
forall a (e :: a) (r :: [a]). ElemOf e (e : r)
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 :: Reformulation' r p m z a -> Reformulation' r p (t m) z a
liftReform Reformulation' r p m z a
reform = \forall x. t m x -> z x
n -> Reformulation' r p m z a
reform (t m x -> z x
forall x. t m x -> z x
n (t m x -> z x) -> (m x -> t m x) -> m x -> z x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. m x -> t m x
forall (t :: Effect) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift)
{-# INLINE liftReform #-}

coerceReform :: Coercible m n
             => Reformulation' r p m z a
             -> Reformulation' r p n z a
coerceReform :: Reformulation' r p m z a -> Reformulation' r p n z a
coerceReform Reformulation' r p m z a
reform forall x. n x -> z x
n Algebra p z
alg = Algebra' r z a -> Algebra' r z a
coerce (Reformulation' r p m z a
reform (n x -> z x
forall x. n x -> z x
n (n x -> z x) -> (m x -> n x) -> m x -> z x
forall b a c. Coercible b a => (b -> c) -> (a -> b) -> a -> c
.# m x -> n x
coerce) Algebra p z
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 :: Reformulation' (e : r) p m z a -> Reformulation' r p m z a
weakenReform Reformulation' (e : r) p m z a
reform forall x. m x -> z x
n Algebra p z
alg = Algebra' (e : r) z a -> Algebra' r z a
forall (e :: Effect) (r :: [Effect]) (m :: * -> *) a.
Algebra' (e : r) m a -> Algebra' r m a
weakenAlg (Reformulation' (e : r) p m z a
reform forall x. m x -> z x
n Algebra p z
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 :: Algebra '[] m -> Algebra '[] (t m)
thread Algebra '[] m
_ = Union '[] (t m) x -> t m x
forall (m :: * -> *) a b. Union '[] m a -> b
absurdU
  {-# INLINE thread #-}

instance (ThreadsEff t e, Threads t p) => Threads t (e ': p) where
  thread :: Algebra (e : p) m -> Algebra (e : p) (t m)
thread Algebra (e : p) m
alg = Algebra' p (t m) x
-> (e (t m) x -> t m x) -> Algebra' (e : p) (t m) x
forall (e :: Effect) (r :: [Effect]) (m :: * -> *) a.
RepresentationalEff e =>
Algebra' r m a -> (e m a -> m a) -> Algebra' (e : r) m a
powerAlg (Algebra p m -> Algebra p (t m)
forall (t :: Effect) (p :: [Effect]) (m :: * -> *).
(Threads t p, Monad m) =>
Algebra p m -> Algebra p (t m)
thread (Algebra' (e : p) m x -> Algebra' p m x
forall (e :: Effect) (r :: [Effect]) (m :: * -> *) a.
Algebra' (e : r) m a -> Algebra' r m a
weakenAlg Algebra' (e : p) m x
Algebra (e : p) m
alg)) ((forall x. e m x -> m x) -> e (t m) x -> t m x
forall (t :: Effect) (e :: Effect) (m :: * -> *) a.
(ThreadsEff t e, Monad m) =>
(forall x. e m x -> m x) -> e (t m) a -> t m a
threadEff (Union (e : p) m x -> m x
Algebra (e : p) m
alg (Union (e : p) m x -> m x)
-> (e m x -> Union (e : p) m x) -> e m x -> m x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ElemOf e (e : p) -> e m x -> Union (e : p) m x
forall (z :: * -> *) (m :: * -> *) (e :: Effect) (r :: [Effect]) a.
Coercible z m =>
ElemOf e r -> e z a -> Union r m a
Union ElemOf e (e : p)
forall a (e :: a) (r :: [a]). ElemOf e (e : r)
Here))
  {-# INLINEABLE thread #-}

-- | Inject an effect into a 'Union' containing that effect.
inj :: Member e r => e m a -> Union r m a
inj :: e m a -> Union r m a
inj = ElemOf e r -> e m a -> Union r m a
forall (z :: * -> *) (m :: * -> *) (e :: Effect) (r :: [Effect]) a.
Coercible z m =>
ElemOf e r -> e z a -> Union r m a
Union ElemOf e r
forall k (e :: k) (r :: [k]). Member e r => ElemOf e r
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 :: e m a -> e n a
coerceEff = e m a -> e n a
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 :: (e m a -> m b) -> e n a -> n b
coerceAlg = (e m a -> m b) -> e n a -> n b
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