Copyright	(c) 2023 Yamada Ryo
License	MPL-2.0 (see the file LICENSE)
Maintainer	ymdfield@outlook.jp
Stability	experimental
Portability	portable
Safe Haskell	Safe-Inferred
Language	GHC2021

Control.Effect.Class.Machinery.HFunctor

Description

This module re-exports the HFunctor type class and related definitions from the compdata package, which are required for the Heftia effect handler system. For more details, please refer to CEP-03 and the compdata documentation.

Synopsis

class HFunctor (h :: (Type -> Type) -> Type -> Type) where
- hfmap :: forall (f :: Type -> Type) (g :: Type -> Type). (f :-> g) -> h f :-> h g
makeHFunctor :: Name -> Q [Dec]
class RemA (s :: (Type -> Type) -> Type -> Type) (s' :: (Type -> Type) -> Type -> Type) | s -> s' where
- remA :: forall (a :: Type -> Type). s a :-> s' a
class DistAnn (s :: (Type -> Type) -> Type -> Type) p (s' :: (Type -> Type) -> Type -> Type) | s' -> s, s' -> p where
- injectA :: forall (a :: Type -> Type). p -> s a :-> s' a
- projectA :: forall (a :: Type -> Type). s' a :-> (s a :&: p)
data ((f :: (Type -> Type) -> k -> Type) :&: a) (g :: Type -> Type) (e :: k) = (f g e) :&: a
type (:=:) (f :: (Type -> Type) -> Type -> Type) (g :: (Type -> Type) -> Type -> Type) = (f :<: g, g :<: f)
type (:<:) (f :: (Type -> Type) -> Type -> Type) (g :: (Type -> Type) -> Type -> Type) = Subsume (ComprEmb (Elem f g)) f g
class Subsume (e :: Emb) (f :: (Type -> Type) -> Type -> Type) (g :: (Type -> Type) -> Type -> Type) where
- inj' :: forall (a :: Type -> Type). Proxy e -> f a :-> g a
- prj' :: forall (a :: Type -> Type). Proxy e -> NatM Maybe (g a) (f a)
type family Elem (f :: (Type -> Type) -> Type -> Type) (g :: (Type -> Type) -> Type -> Type) :: Emb where ...
data ((f :: (Type -> Type) -> k -> Type) :+: (g :: (Type -> Type) -> k -> Type)) (h :: Type -> Type) (e :: k)
- = Inl (f h e)
- | Inr (g h e)
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

Documentation

class HFunctor (h :: (Type -> Type) -> Type -> Type) where #

This class represents higher-order functors (Johann, Ghani, POPL '08) which are endofunctors on the category of endofunctors.

Methods

hfmap :: forall (f :: Type -> Type) (g :: Type -> Type). (f :-> g) -> h f :-> h g #

A higher-order functor f also maps a natural transformation g :-> h to a natural transformation f g :-> f h

Instances

Instances details

HFunctor (LiftIns ins) Source #
Instance details Defined in Control.Effect.Class Methods hfmap :: forall (f :: Type -> Type) (g :: Type -> Type). (f :-> g) -> LiftIns ins f :-> LiftIns ins g #
Functor f => HFunctor (Compose f :: (Type -> Type) -> Type -> Type)
Instance details Defined in Data.Comp.Multi.HFunctor Methods hfmap :: forall (f0 :: Type -> Type) (g :: Type -> Type). (f0 :-> g) -> Compose f f0 :-> Compose f g #
HFunctor sig => HFunctor (TagH sig tag) Source #
Instance details Defined in Control.Effect.Class Methods hfmap :: forall (f :: Type -> Type) (g :: Type -> Type). (f :-> g) -> TagH sig tag f :-> TagH sig tag g #
HFunctor f => HFunctor (f :&: a)
Instance details Defined in Data.Comp.Multi.Ops Methods hfmap :: forall (f0 :: Type -> Type) (g :: Type -> Type). (f0 :-> g) -> (f :&: a) f0 :-> (f :&: a) g #
(HFunctor f, HFunctor g) => HFunctor (f :+: g)
Instance details Defined in Data.Comp.Multi.Ops Methods hfmap :: forall (f0 :: Type -> Type) (g0 :: Type -> Type). (f0 :-> g0) -> (f :+: g) f0 :-> (f :+: g) g0 #

makeHFunctor :: Name -> Q [Dec] #

Derive an instance of HFunctor for a type constructor of any higher-order kind taking at least two arguments.

class RemA (s :: (Type -> Type) -> Type -> Type) (s' :: (Type -> Type) -> Type -> Type) | s -> s' where #

Methods

remA :: forall (a :: Type -> Type). s a :-> s' a #

Instances

Instances details

RemA (f :&: p) f
Instance details Defined in Data.Comp.Multi.Ops Methods remA :: forall (a :: Type -> Type). (f :&: p) a :-> f a #
RemA s s' => RemA ((f :&: p) :+: s) (f :+: s')
Instance details Defined in Data.Comp.Multi.Ops Methods remA :: forall (a :: Type -> Type). ((f :&: p) :+: s) a :-> (f :+: s') a #

class DistAnn (s :: (Type -> Type) -> Type -> Type) p (s' :: (Type -> Type) -> Type -> Type) | s' -> s, s' -> p where #

This class defines how to distribute an annotation over a sum of signatures.

Methods

injectA :: forall (a :: Type -> Type). p -> s a :-> s' a #

This function injects an annotation over a signature.

projectA :: forall (a :: Type -> Type). s' a :-> (s a :&: p) #

Instances

Instances details

DistAnn f p (f :&: p)
Instance details Defined in Data.Comp.Multi.Ops Methods injectA :: forall (a :: Type -> Type). p -> f a :-> (f :&: p) a # projectA :: forall (a :: Type -> Type). (f :&: p) a :-> (f a :&: p) #
DistAnn s p s' => DistAnn (f :+: s) p ((f :&: p) :+: s')
Instance details Defined in Data.Comp.Multi.Ops Methods injectA :: forall (a :: Type -> Type). p -> (f :+: s) a :-> ((f :&: p) :+: s') a # projectA :: forall (a :: Type -> Type). ((f :&: p) :+: s') a :-> ((f :+: s) a :&: p) #

data ((f :: (Type -> Type) -> k -> Type) :&: a) (g :: Type -> Type) (e :: k) infixr 7 #

This data type adds a constant product to a signature. Alternatively, this could have also been defined as

data (f :&: a) (g ::  Type -> Type) e = f g e :&: a e

This is too general, however, for example for productHHom.

Constructors

(f g e) :&: a infixr 7

Instances

Instances details

DistAnn f p (f :&: p)
Instance details Defined in Data.Comp.Multi.Ops Methods injectA :: forall (a :: Type -> Type). p -> f a :-> (f :&: p) a # projectA :: forall (a :: Type -> Type). (f :&: p) a :-> (f a :&: p) #
HFoldable f => HFoldable (f :&: a)
Instance details Defined in Data.Comp.Multi.Ops Methods hfold :: Monoid m => (f :&: a) (K m) :=> m # hfoldMap :: forall m (a0 :: Type -> Type). Monoid m => (a0 :=> m) -> (f :&: a) a0 :=> m # hfoldr :: forall (a0 :: Type -> Type) b. (a0 :=> (b -> b)) -> b -> (f :&: a) a0 :=> b # hfoldl :: forall b (a0 :: Type -> Type). (b -> a0 :=> b) -> b -> (f :&: a) a0 :=> b # hfoldr1 :: (a0 -> a0 -> a0) -> (f :&: a) (K a0) :=> a0 # hfoldl1 :: (a0 -> a0 -> a0) -> (f :&: a) (K a0) :=> a0 #
HFunctor f => HFunctor (f :&: a)
Instance details Defined in Data.Comp.Multi.Ops Methods hfmap :: forall (f0 :: Type -> Type) (g :: Type -> Type). (f0 :-> g) -> (f :&: a) f0 :-> (f :&: a) g #
HTraversable f => HTraversable (f :&: a)
Instance details Defined in Data.Comp.Multi.Ops Methods hmapM :: forall (m :: Type -> Type) (a0 :: Type -> Type) (b :: Type -> Type). Monad m => NatM m a0 b -> NatM m ((f :&: a) a0) ((f :&: a) b) # htraverse :: forall (f0 :: Type -> Type) (a0 :: Type -> Type) (b :: Type -> Type). Applicative f0 => NatM f0 a0 b -> NatM f0 ((f :&: a) a0) ((f :&: a) b) #
RemA (f :&: p) f
Instance details Defined in Data.Comp.Multi.Ops Methods remA :: forall (a :: Type -> Type). (f :&: p) a :-> f a #
DistAnn s p s' => DistAnn (f :+: s) p ((f :&: p) :+: s')
Instance details Defined in Data.Comp.Multi.Ops Methods injectA :: forall (a :: Type -> Type). p -> (f :+: s) a :-> ((f :&: p) :+: s') a # projectA :: forall (a :: Type -> Type). ((f :&: p) :+: s') a :-> ((f :+: s) a :&: p) #
RemA s s' => RemA ((f :&: p) :+: s) (f :+: s')
Instance details Defined in Data.Comp.Multi.Ops Methods remA :: forall (a :: Type -> Type). ((f :&: p) :+: s) a :-> (f :+: s') a #

type (:=:) (f :: (Type -> Type) -> Type -> Type) (g :: (Type -> Type) -> Type -> Type) = (f :<: g, g :<: f) infixl 5 #

type (:<:) (f :: (Type -> Type) -> Type -> Type) (g :: (Type -> Type) -> Type -> Type) = Subsume (ComprEmb (Elem f g)) f g infixl 5 #

A constraint f :<: g expresses that the signature f is subsumed by g, i.e. f can be used to construct elements in g.

class Subsume (e :: Emb) (f :: (Type -> Type) -> Type -> Type) (g :: (Type -> Type) -> Type -> Type) where #

Methods

inj' :: forall (a :: Type -> Type). Proxy e -> f a :-> g a #

prj' :: forall (a :: Type -> Type). Proxy e -> NatM Maybe (g a) (f a) #

Instances

Instances details

Subsume ('Found 'Here) f f
Instance details Defined in Data.Comp.Multi.Ops Methods inj' :: forall (a :: Type -> Type). Proxy ('Found 'Here) -> f a :-> f a # prj' :: forall (a :: Type -> Type). Proxy ('Found 'Here) -> NatM Maybe (f a) (f a) #
Subsume ('Found p) f g => Subsume ('Found ('Le p)) f (g :+: g')
Instance details Defined in Data.Comp.Multi.Ops Methods inj' :: forall (a :: Type -> Type). Proxy ('Found ('Le p)) -> f a :-> (g :+: g') a # prj' :: forall (a :: Type -> Type). Proxy ('Found ('Le p)) -> NatM Maybe ((g :+: g') a) (f a) #
Subsume ('Found p) f g => Subsume ('Found ('Ri p)) f (g' :+: g)
Instance details Defined in Data.Comp.Multi.Ops Methods inj' :: forall (a :: Type -> Type). Proxy ('Found ('Ri p)) -> f a :-> (g' :+: g) a # prj' :: forall (a :: Type -> Type). Proxy ('Found ('Ri p)) -> NatM Maybe ((g' :+: g) a) (f a) #
(Subsume ('Found p1) f1 g, Subsume ('Found p2) f2 g) => Subsume ('Found ('Sum p1 p2)) (f1 :+: f2) g
Instance details Defined in Data.Comp.Multi.Ops Methods inj' :: forall (a :: Type -> Type). Proxy ('Found ('Sum p1 p2)) -> (f1 :+: f2) a :-> g a # prj' :: forall (a :: Type -> Type). Proxy ('Found ('Sum p1 p2)) -> NatM Maybe (g a) ((f1 :+: f2) a) #

type family Elem (f :: (Type -> Type) -> Type -> Type) (g :: (Type -> Type) -> Type -> Type) :: Emb where ... #

Equations

Elem f f = 'Found 'Here
Elem (f1 :+: f2) g = Sum' (Elem f1 g) (Elem f2 g)
Elem f (g1 :+: g2) = Choose (Elem f g1) (Elem f g2)
Elem f g = 'NotFound

data ((f :: (Type -> Type) -> k -> Type) :+: (g :: (Type -> Type) -> k -> Type)) (h :: Type -> Type) (e :: k) infixr 6 #

Data type defining coproducts.

Constructors

Inl (f h e)
Inr (g h e)

Instances

Instances details

Subsume ('Found p) f g => Subsume ('Found ('Le p)) f (g :+: g')
Instance details Defined in Data.Comp.Multi.Ops Methods inj' :: forall (a :: Type -> Type). Proxy ('Found ('Le p)) -> f a :-> (g :+: g') a # prj' :: forall (a :: Type -> Type). Proxy ('Found ('Le p)) -> NatM Maybe ((g :+: g') a) (f a) #
Subsume ('Found p) f g => Subsume ('Found ('Ri p)) f (g' :+: g)
Instance details Defined in Data.Comp.Multi.Ops Methods inj' :: forall (a :: Type -> Type). Proxy ('Found ('Ri p)) -> f a :-> (g' :+: g) a # prj' :: forall (a :: Type -> Type). Proxy ('Found ('Ri p)) -> NatM Maybe ((g' :+: g) a) (f a) #
(Subsume ('Found p1) f1 g, Subsume ('Found p2) f2 g) => Subsume ('Found ('Sum p1 p2)) (f1 :+: f2) g
Instance details Defined in Data.Comp.Multi.Ops Methods inj' :: forall (a :: Type -> Type). Proxy ('Found ('Sum p1 p2)) -> (f1 :+: f2) a :-> g a # prj' :: forall (a :: Type -> Type). Proxy ('Found ('Sum p1 p2)) -> NatM Maybe (g a) ((f1 :+: f2) a) #
(EqHF f, EqHF g) => EqHF (f :+: g)	`EqF` is propagated through sums.
Instance details Defined in Data.Comp.Multi.Equality Methods eqHF :: forall (g0 :: Type -> Type) i j. KEq g0 => (f :+: g) g0 i -> (f :+: g) g0 j -> Bool #
(HFoldable f, HFoldable g) => HFoldable (f :+: g)
Instance details Defined in Data.Comp.Multi.Ops Methods hfold :: Monoid m => (f :+: g) (K m) :=> m # hfoldMap :: forall m (a :: Type -> Type). Monoid m => (a :=> m) -> (f :+: g) a :=> m # hfoldr :: forall (a :: Type -> Type) b. (a :=> (b -> b)) -> b -> (f :+: g) a :=> b # hfoldl :: forall b (a :: Type -> Type). (b -> a :=> b) -> b -> (f :+: g) a :=> b # hfoldr1 :: (a -> a -> a) -> (f :+: g) (K a) :=> a # hfoldl1 :: (a -> a -> a) -> (f :+: g) (K a) :=> a #
(HFunctor f, HFunctor g) => HFunctor (f :+: g)
Instance details Defined in Data.Comp.Multi.Ops Methods hfmap :: forall (f0 :: Type -> Type) (g0 :: Type -> Type). (f0 :-> g0) -> (f :+: g) f0 :-> (f :+: g) g0 #
(HTraversable f, HTraversable g) => HTraversable (f :+: g)
Instance details Defined in Data.Comp.Multi.Ops Methods hmapM :: forall (m :: Type -> Type) (a :: Type -> Type) (b :: Type -> Type). Monad m => NatM m a b -> NatM m ((f :+: g) a) ((f :+: g) b) # htraverse :: forall (f0 :: Type -> Type) (a :: Type -> Type) (b :: Type -> Type). Applicative f0 => NatM f0 a b -> NatM f0 ((f :+: g) a) ((f :+: g) b) #
(OrdHF f, OrdHF g) => OrdHF (f :+: g)	`OrdHF` is propagated through sums.
Instance details Defined in Data.Comp.Multi.Ordering Methods compareHF :: forall (a :: Type -> Type) i j. KOrd a => (f :+: g) a i -> (f :+: g) a j -> Ordering #
DistAnn s p s' => DistAnn (f :+: s) p ((f :&: p) :+: s')
Instance details Defined in Data.Comp.Multi.Ops Methods injectA :: forall (a :: Type -> Type). p -> (f :+: s) a :-> ((f :&: p) :+: s') a # projectA :: forall (a :: Type -> Type). ((f :&: p) :+: s') a :-> ((f :+: s) a :&: p) #
RemA s s' => RemA ((f :&: p) :+: s) (f :+: s')
Instance details Defined in Data.Comp.Multi.Ops Methods remA :: forall (a :: Type -> Type). ((f :&: p) :+: s) a :-> (f :+: s') a #

caseH :: forall {k} f (a :: Type -> Type) (b :: k) c g. (f a b -> c) -> (g a b -> c) -> (f :+: g) a b -> c #

Utility function to case on a higher-order functor sum, without exposing the internal representation of sums.

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 #