-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/


-- | A basic framework for effect systems based on effects represented by GADTs.
--   
--   This library provides core definitions of <a>data-effects</a>.
@package data-effects-core
@version 0.1.0.0


-- | This module re-exports the <a>HFunctor</a> type class and related
--   definitions from the <tt>compdata</tt> package. For more details,
--   please refer to the <a><tt>compdata</tt> documentation</a>.
module Data.Effect.HFunctor

-- | This class represents higher-order functors (Johann, Ghani, POPL '08)
--   which are endofunctors on the category of endofunctors.
class HFunctor (h :: Type -> Type -> Type -> Type)

-- | A higher-order functor <tt>f</tt> also maps a natural transformation
--   <tt>g :-&gt; h</tt> to a natural transformation <tt>f g :-&gt; f
--   h</tt>
hfmap :: forall (f :: Type -> Type) (g :: Type -> Type). HFunctor h => (f :-> g) -> h f :-> h g
class RemA (s :: Type -> Type -> Type -> Type) (s' :: Type -> Type -> Type -> Type) | s -> s'
remA :: forall (a :: Type -> Type). RemA s s' => s a :-> s' a

-- | This class defines how to distribute an annotation over a sum of
--   signatures.
class DistAnn (s :: Type -> Type -> Type -> Type) p (s' :: Type -> Type -> Type -> Type) | s' -> s, s' -> p

-- | This function injects an annotation over a signature.
injectA :: forall (a :: Type -> Type). DistAnn s p s' => p -> s a :-> s' a
projectA :: forall (a :: Type -> Type). DistAnn s p s' => s' a :-> (s a :&: p)

-- | This data type adds a constant product to a signature. Alternatively,
--   this could have also been defined as
--   
--   <pre>
--   data (f :&amp;: a) (g ::  Type -&gt; Type) e = f g e :&amp;: a e
--   </pre>
--   
--   This is too general, however, for example for <tt>productHHom</tt>.
data ( (f :: Type -> Type -> k -> Type) :&: a ) (g :: Type -> Type) (e :: k)
(:&:) :: f g e -> a -> (:&:) (f :: (Type -> Type) -> k -> Type) a (g :: Type -> Type) (e :: k)
infixr 7 :&:
infixr 7 :&:
type (f :: Type -> Type -> Type -> Type) :=: (g :: Type -> Type -> Type -> Type) = (f :<: g, g :<: f)
infixl 5 :=:

-- | A constraint <tt>f :&lt;: g</tt> expresses that the signature
--   <tt>f</tt> is subsumed by <tt>g</tt>, i.e. <tt>f</tt> can be used to
--   construct elements in <tt>g</tt>.
type (f :: Type -> Type -> Type -> Type) :<: (g :: Type -> Type -> Type -> Type) = Subsume ComprEmb Elem f g f g
infixl 5 :<:
class Subsume (e :: Emb) (f :: Type -> Type -> Type -> Type) (g :: Type -> Type -> Type -> Type)
inj' :: forall (a :: Type -> Type). Subsume e f g => Proxy e -> f a :-> g a
prj' :: forall (a :: Type -> Type). Subsume e f g => Proxy e -> NatM Maybe (g a) (f a)
type family Elem (f :: Type -> Type -> Type -> Type) (g :: Type -> Type -> Type -> Type) :: Emb

-- | Data type defining coproducts.
data ( (f :: Type -> Type -> k -> Type) :+: (g :: Type -> Type -> k -> Type) ) (h :: Type -> Type) (e :: k)
Inl :: f h e -> (:+:) (f :: (Type -> Type) -> k -> Type) (g :: (Type -> Type) -> k -> Type) (h :: Type -> Type) (e :: k)
Inr :: g h e -> (:+:) (f :: (Type -> Type) -> k -> Type) (g :: (Type -> Type) -> k -> Type) (h :: Type -> Type) (e :: k)
infixr 6 :+:

-- | Utility function to case on a higher-order functor sum, without
--   exposing the internal representation of sums.
caseH :: forall {k} f (a :: Type -> Type) (b :: k) c g. (f a b -> c) -> (g a b -> c) -> (f :+: g) a b -> c
inj :: forall (f :: (Type -> Type) -> Type -> Type) (g :: (Type -> Type) -> Type -> Type) (a :: Type -> Type). f :<: g => f a :-> g a
proj :: forall (f :: (Type -> Type) -> Type -> Type) (g :: (Type -> Type) -> Type -> Type) (a :: Type -> Type). f :<: g => NatM Maybe (g a) (f a)
spl :: forall (f :: (Type -> Type) -> Type -> Type) (f1 :: (Type -> Type) -> Type -> Type) (f2 :: (Type -> Type) -> Type -> Type) (a :: Type -> Type) (b :: Type -> Type). f :=: (f1 :+: f2) => (f1 a :-> b) -> (f2 a :-> b) -> f a :-> b


module Data.Effect

-- | A kind of <i>signature class</i> (a datatype of higher-order effect).
type SigClass = (Type -> Type) -> Type -> Type

-- | A kind of <i>instruction class</i> (a datatype of first-order effect).
type InsClass = Type -> Type

-- | Lift an <i>instruction class</i> to a <i>signature class</i>.
--   
--   Come from <a>heft-lang/POPL2023/haskell/src/Elab.hs</a>.
newtype LiftIns (ins :: InsClass) (f :: Type -> Type) a
LiftIns :: ins a -> LiftIns (ins :: InsClass) (f :: Type -> Type) a
[unliftIns] :: LiftIns (ins :: InsClass) (f :: Type -> Type) a -> ins a

-- | An <i>instruction class</i> with no effects.
data Nop :: InsClass

-- | A <i>signature class</i> with no effects.
type LNop = LiftIns Nop
instance Data.Traversable.Traversable ins => Data.Traversable.Traversable (Data.Effect.LiftIns ins f)
instance Data.Foldable.Foldable ins => Data.Foldable.Foldable (Data.Effect.LiftIns ins f)
instance GHC.Base.Functor ins => GHC.Base.Functor (Data.Effect.LiftIns ins f)
instance Data.Comp.Multi.HFunctor.HFunctor (Data.Effect.LiftIns ins)


module Control.Effect

-- | A type class that represents the ability to send an <i>instruction</i>
--   <tt>ins</tt> to carrier <tt>f</tt>.
class SendIns (ins :: InsClass) f

-- | Send an <i>instruction</i> <tt>ins</tt> to carrier <tt>f</tt>.
sendIns :: SendIns ins f => ins a -> f a

-- | The operator version of <a>SendIns</a>.
type (<:) = SendIns
infix 2 <:

-- | A type class that represents the ability to send a <i>signature</i>
--   <tt>sig</tt> to carrier <tt>f</tt>.
class SendSig (sig :: SigClass) f

-- | Send a <i>signature</i> <tt>sig</tt> to carrier <tt>f</tt>.
sendSig :: SendSig sig f => sig f a -> f a

-- | The operator version of <a>SendSig</a>.
type (<<:) = SendSig
infix 2 <<:

-- | A natural transformation.
type f ~> g = forall (x :: Type). f x -> g x
infixr 2 ~>
instance Control.Effect.SendIns ins f => Control.Effect.SendSig (Data.Effect.LiftIns ins) f


module Control.Effect.Key
class SendInsBy key (ins :: InsClass) f | key f -> ins
sendInsBy :: SendInsBy key ins f => ins a -> f a
class SendSigBy key (sig :: SigClass) f | key f -> sig
sendSigBy :: SendSigBy key sig f => sig f a -> f a

-- | A wrapper data type to represent sending an effect to the carrier
--   <tt>f</tt> with the specified key.
newtype ByKey key (f :: Type -> Type) a
ByKey :: f a -> ByKey key (f :: Type -> Type) a
[runByKey] :: ByKey key (f :: Type -> Type) a -> f a

-- | Send all effects within the scope, keyed, to carrier <tt>f</tt>.
key :: forall key f a. ByKey key f a -> f a
instance forall e k (key :: k) (f :: * -> *). Control.Monad.Error.Class.MonadError e f => Control.Monad.Error.Class.MonadError e (Control.Effect.Key.ByKey key f)
instance forall r w s k (key :: k) (f :: * -> *). (Control.Monad.Reader.Class.MonadReader r f, Control.Monad.Writer.Class.MonadWriter w f, Control.Monad.State.Class.MonadState s f) => Control.Monad.RWS.Class.MonadRWS r w s (Control.Effect.Key.ByKey key f)
instance forall s k (key :: k) (f :: * -> *). Control.Monad.State.Class.MonadState s f => Control.Monad.State.Class.MonadState s (Control.Effect.Key.ByKey key f)
instance forall w k (key :: k) (f :: * -> *). Control.Monad.Writer.Class.MonadWriter w f => Control.Monad.Writer.Class.MonadWriter w (Control.Effect.Key.ByKey key f)
instance forall r k (key :: k) (f :: * -> *). Control.Monad.Reader.Class.MonadReader r f => Control.Monad.Reader.Class.MonadReader r (Control.Effect.Key.ByKey key f)
instance forall k (key :: k) (f :: * -> *). Control.Monad.Fail.MonadFail f => Control.Monad.Fail.MonadFail (Control.Effect.Key.ByKey key f)
instance forall k (key :: k) (f :: * -> *). Control.Monad.IO.Class.MonadIO f => Control.Monad.IO.Class.MonadIO (Control.Effect.Key.ByKey key f)
instance forall k (key :: k) (f :: * -> *). Control.Monad.Fix.MonadFix f => Control.Monad.Fix.MonadFix (Control.Effect.Key.ByKey key f)
instance forall k (key :: k) (f :: * -> *). GHC.Base.MonadPlus f => GHC.Base.MonadPlus (Control.Effect.Key.ByKey key f)
instance forall k (key :: k) (f :: * -> *). GHC.Base.Monad f => GHC.Base.Monad (Control.Effect.Key.ByKey key f)
instance forall k (key :: k) (f :: * -> *). GHC.Base.Alternative f => GHC.Base.Alternative (Control.Effect.Key.ByKey key f)
instance forall k (key :: k) (f :: * -> *). GHC.Base.Applicative f => GHC.Base.Applicative (Control.Effect.Key.ByKey key f)
instance forall k (key :: k) (f :: * -> *). GHC.Base.Functor f => GHC.Base.Functor (Control.Effect.Key.ByKey key f)
instance forall k (key :: k) (ins :: Data.Effect.InsClass) (f :: * -> *). Control.Effect.Key.SendInsBy key ins f => Control.Effect.SendIns ins (Control.Effect.Key.ByKey key f)
instance forall k (key :: k) (sig :: Data.Effect.SigClass) (f :: * -> *). (Control.Effect.Key.SendSigBy key sig f, Data.Comp.Multi.HFunctor.HFunctor sig) => Control.Effect.SendSig sig (Control.Effect.Key.ByKey key f)


module Data.Effect.HFunctor.HCont

-- | This represents that the effect <tt>ff</tt> is finally interpreted as
--   the base carrier <tt>b</tt>.
newtype HCont ff b f (a :: Type)
HCont :: ((f ~> b) -> ff b a) -> HCont ff b f (a :: Type)
[unHCont] :: HCont ff b f (a :: Type) -> (f ~> b) -> ff b a
type (~~>) = HCont
infixr 8 ~~>
instance GHC.Base.Functor (ff b) => GHC.Base.Functor (Data.Effect.HFunctor.HCont.HCont ff b f)
instance Data.Comp.Multi.HFunctor.HFunctor (Data.Effect.HFunctor.HCont.HCont ff g)


module Data.Effect.Key

-- | Keyed <i>instruction class</i>.
newtype Key key (ins :: InsClass) a
Key :: ins a -> Key key (ins :: InsClass) a
[unKey] :: Key key (ins :: InsClass) a -> ins a

-- | Keyed <i>instruction class</i>.
type (#>) = Key
infixr 7 #>

-- | Keyed <i>instruction class</i>.
pattern K :: forall key ins a. ins a -> Key key ins a

-- | Keyed <i>signature class</i>.
newtype KeyH key (sig :: SigClass) f a
KeyH :: sig f a -> KeyH key (sig :: SigClass) f a
[unKeyH] :: KeyH key (sig :: SigClass) f a -> sig f a

-- | Keyed <i>signature class</i>.
type (##>) = KeyH
infixr 7 ##>

-- | Keyed <i>signature class</i>.
pattern KH :: forall key sig f a. sig f a -> KeyH key sig f a
instance forall k (key :: k) (ins :: Data.Effect.InsClass). Data.Traversable.Traversable ins => Data.Traversable.Traversable (Data.Effect.Key.Key key ins)
instance forall k (key :: k) (ins :: Data.Effect.InsClass). Data.Foldable.Foldable ins => Data.Foldable.Foldable (Data.Effect.Key.Key key ins)
instance forall k (key :: k) (ins :: Data.Effect.InsClass). GHC.Base.Functor ins => GHC.Base.Functor (Data.Effect.Key.Key key ins)
instance forall k (key :: k) (sig :: Data.Effect.SigClass). Data.Comp.Multi.HFunctor.HFunctor sig => Data.Comp.Multi.HFunctor.HFunctor (Data.Effect.Key.KeyH key sig)
instance forall k (key :: k) (sig :: Data.Effect.SigClass) (f :: * -> *). Data.Traversable.Traversable (sig f) => Data.Traversable.Traversable (Data.Effect.Key.KeyH key sig f)
instance forall k (key :: k) (sig :: Data.Effect.SigClass) (f :: * -> *). Data.Foldable.Foldable (sig f) => Data.Foldable.Foldable (Data.Effect.Key.KeyH key sig f)
instance forall k (key :: k) (sig :: Data.Effect.SigClass) (f :: * -> *). GHC.Base.Functor (sig f) => GHC.Base.Functor (Data.Effect.Key.KeyH key sig f)


module Data.Effect.Tag

-- | Tagged <i>instruction class</i>.
newtype Tag (ins :: InsClass) tag a
Tag :: ins a -> Tag (ins :: InsClass) tag a
[unTag] :: Tag (ins :: InsClass) tag a -> ins a

-- | Tagged <i>instruction class</i>.
type (#) = Tag
infixl 8 #

-- | Tagged <i>instruction class</i>.
pattern T :: forall tag ins a. ins a -> Tag ins tag a

-- | Tagged <i>signature class</i>.
newtype TagH (sig :: SigClass) tag f a
TagH :: sig f a -> TagH (sig :: SigClass) tag f a
[unTagH] :: TagH (sig :: SigClass) tag f a -> sig f a

-- | Tagged <i>signature class</i>.
type (##) = TagH
infixl 8 ##

-- | Tagged <i>signature class</i>.
pattern TH :: forall tag sig f a. sig f a -> TagH sig tag f a
instance forall (ins :: Data.Effect.InsClass) k (tag :: k). Data.Traversable.Traversable ins => Data.Traversable.Traversable (Data.Effect.Tag.Tag ins tag)
instance forall (ins :: Data.Effect.InsClass) k (tag :: k). Data.Foldable.Foldable ins => Data.Foldable.Foldable (Data.Effect.Tag.Tag ins tag)
instance forall (ins :: Data.Effect.InsClass) k (tag :: k). GHC.Base.Functor ins => GHC.Base.Functor (Data.Effect.Tag.Tag ins tag)
instance forall (sig :: Data.Effect.SigClass) k (tag :: k). Data.Comp.Multi.HFunctor.HFunctor sig => Data.Comp.Multi.HFunctor.HFunctor (Data.Effect.Tag.TagH sig tag)
instance forall (sig :: Data.Effect.SigClass) k (tag :: k) (f :: * -> *). Data.Traversable.Traversable (sig f) => Data.Traversable.Traversable (Data.Effect.Tag.TagH sig tag f)
instance forall (sig :: Data.Effect.SigClass) k (tag :: k) (f :: * -> *). Data.Foldable.Foldable (sig f) => Data.Foldable.Foldable (Data.Effect.Tag.TagH sig tag f)
instance forall (sig :: Data.Effect.SigClass) k (tag :: k) (f :: * -> *). GHC.Base.Functor (sig f) => GHC.Base.Functor (Data.Effect.Tag.TagH sig tag f)


module Control.Effect.Tag

-- | A wrapper data type to represent sending an effect to the carrier
--   <tt>f</tt> with the specified tag.
newtype ViaTag tag (f :: Type -> Type) a
ViaTag :: f a -> ViaTag tag (f :: Type -> Type) a
[runViaTag] :: ViaTag tag (f :: Type -> Type) a -> f a

-- | Send all effects within the scope, tagged, to carrier <tt>f</tt>.
tag :: forall tag f a. ViaTag tag f a -> f a
instance forall e k (tag :: k) (f :: * -> *). Control.Monad.Error.Class.MonadError e f => Control.Monad.Error.Class.MonadError e (Control.Effect.Tag.ViaTag tag f)
instance forall r w s k (tag :: k) (f :: * -> *). (Control.Monad.Reader.Class.MonadReader r f, Control.Monad.Writer.Class.MonadWriter w f, Control.Monad.State.Class.MonadState s f) => Control.Monad.RWS.Class.MonadRWS r w s (Control.Effect.Tag.ViaTag tag f)
instance forall s k (tag :: k) (f :: * -> *). Control.Monad.State.Class.MonadState s f => Control.Monad.State.Class.MonadState s (Control.Effect.Tag.ViaTag tag f)
instance forall w k (tag :: k) (f :: * -> *). Control.Monad.Writer.Class.MonadWriter w f => Control.Monad.Writer.Class.MonadWriter w (Control.Effect.Tag.ViaTag tag f)
instance forall r k (tag :: k) (f :: * -> *). Control.Monad.Reader.Class.MonadReader r f => Control.Monad.Reader.Class.MonadReader r (Control.Effect.Tag.ViaTag tag f)
instance forall k (tag :: k) (f :: * -> *). Control.Monad.Fail.MonadFail f => Control.Monad.Fail.MonadFail (Control.Effect.Tag.ViaTag tag f)
instance forall k (tag :: k) (f :: * -> *). Control.Monad.IO.Class.MonadIO f => Control.Monad.IO.Class.MonadIO (Control.Effect.Tag.ViaTag tag f)
instance forall k (tag :: k) (f :: * -> *). Control.Monad.Fix.MonadFix f => Control.Monad.Fix.MonadFix (Control.Effect.Tag.ViaTag tag f)
instance forall k (tag :: k) (f :: * -> *). GHC.Base.MonadPlus f => GHC.Base.MonadPlus (Control.Effect.Tag.ViaTag tag f)
instance forall k (tag :: k) (f :: * -> *). GHC.Base.Monad f => GHC.Base.Monad (Control.Effect.Tag.ViaTag tag f)
instance forall k (tag :: k) (f :: * -> *). GHC.Base.Alternative f => GHC.Base.Alternative (Control.Effect.Tag.ViaTag tag f)
instance forall k (tag :: k) (f :: * -> *). GHC.Base.Applicative f => GHC.Base.Applicative (Control.Effect.Tag.ViaTag tag f)
instance forall k (tag :: k) (f :: * -> *). GHC.Base.Functor f => GHC.Base.Functor (Control.Effect.Tag.ViaTag tag f)
instance forall k (ins :: Data.Effect.InsClass) (tag :: k) (f :: * -> *). Control.Effect.SendIns (ins Data.Effect.Tag.# tag) f => Control.Effect.SendIns ins (Control.Effect.Tag.ViaTag tag f)
instance forall k (sig :: Data.Effect.SigClass) (tag :: k) (f :: * -> *). (Control.Effect.SendSig (sig Data.Effect.Tag.## tag) f, Data.Comp.Multi.HFunctor.HFunctor sig) => Control.Effect.SendSig sig (Control.Effect.Tag.ViaTag tag f)
instance forall k1 k2 (key :: k1) (ins :: Data.Effect.InsClass) (tag :: k2) (f :: * -> *). Control.Effect.Key.SendInsBy key (ins Data.Effect.Tag.# tag) f => Control.Effect.Key.SendInsBy key ins (Control.Effect.Tag.ViaTag tag f)
instance forall k1 k2 (key :: k1) (sig :: Data.Effect.SigClass) (tag :: k2) (f :: * -> *). (Control.Effect.Key.SendSigBy key (sig Data.Effect.Tag.## tag) f, Data.Comp.Multi.HFunctor.HFunctor sig) => Control.Effect.Key.SendSigBy key sig (Control.Effect.Tag.ViaTag tag f)