Data.Comp.Multi.Sum

This module defines sums on signatures. All definitions are generalised versions of those in Data.Comp.Sum.

Documentation

type (:<:) f g = 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.

data (f :+: g) (h :: * -> *) e infixr 6

Data type defining coproducts.

Instances

(HFunctor f, HFunctor g) => HFunctor (f :+: g)

Defined in Data.Comp.Multi.Ops

Methods

hfmap :: (f0 :-> g0) -> (f :+: g) f0 :-> (f :+: g) g0

(HFoldable f, HFoldable g) => HFoldable (f :+: g)

Defined in Data.Comp.Multi.Ops

Methods

hfold :: Monoid m => (f :+: g) (K m) :=> m

hfoldMap :: Monoid m => (a :=> m) -> (f :+: g) a :=> m

hfoldr :: (a :=> (b -> b)) -> b -> (f :+: g) a :=> b

hfoldl :: (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

(HTraversable f, HTraversable g) => HTraversable (f :+: g)

Defined in Data.Comp.Multi.Ops

Methods

hmapM :: Monad m => NatM m a b -> NatM m ((f :+: g) a) ((f :+: g) b)

htraverse :: Applicative f0 => NatM f0 a b -> NatM f0 ((f :+: g) a) ((f :+: g) b)

(ShowHF f, ShowHF g) => ShowHF (f :+: g)

Defined in Data.Comp.Multi.Show

Methods

showHF :: Alg (f :+: g) (K String)

showHF' :: (f :+: g) (K String) :=> String

(EqHF f, EqHF g) => EqHF (f :+: g)

EqF is propagated through sums.

Defined in Data.Comp.Multi.Equality

Methods

eqHF :: KEq g0 => (f :+: g) g0 i -> (f :+: g) g0 j -> Bool

(OrdHF f, OrdHF g) => OrdHF (f :+: g)

OrdHF is propagated through sums.

Defined in Data.Comp.Multi.Ordering

Methods

compareHF :: KOrd a => (f :+: g) a i -> (f :+: g) a j -> Ordering

(HasVars f v, HasVars g v) => HasVars (f :+: g) v

Defined in Data.Comp.Multi.Variables

Methods

isVar :: (f :+: g) a i -> Maybe v

bindsVars :: Mapping m a => (f :+: g) a :=> m (Set v)

(Desugar f h, Desugar g h) => Desugar (f :+: g) h

Defined in Data.Comp.Multi.Desugar

Methods

desugHom :: Hom (f :+: g) h

desugHom' :: (f :+: g) (Context h a) i -> Context h a i

DistAnn s p s' => DistAnn (f :+: s) p ((f :&: p) :+: s')

Defined in Data.Comp.Multi.Ops

Methods

injectA :: p -> (f :+: s) a :-> ((f :&: p) :+: s') a

projectA :: ((f :&: p) :+: s') a i -> ((f :+: s) a :&: p) i

RemA s s' => RemA ((f :&: p) :+: s) (f :+: s')

Defined in Data.Comp.Multi.Ops

Methods

remA :: ((f :&: p) :+: s) a i -> (f :+: s') a i

caseH :: (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.

Projections for Signatures and Terms

proj :: forall f g a. f :<: g => NatM Maybe (g a) (f a)

project :: g :<: f => NatM Maybe (Cxt h f a) (g (Cxt h f a))

Project the outermost layer of a term to a sub signature. If the signature g is compound of n atomic signatures, use projectn instead.

deepProject :: (HTraversable g, g :<: f) => CxtFunM Maybe f g

Tries to coerce a termcontext to a termcontext over a sub-signature. If the signature g is compound of n atomic signatures, use deepProjectn instead.

Injections for Signatures and Terms

inj :: forall f g a. f :<: g => f a :-> g a

inject :: g :<: f => g (Cxt h f a) :-> Cxt h f a

Inject a term where the outermost layer is a sub signature. If the signature g is compound of n atomic signatures, use injectn instead.

deepInject :: (HFunctor g, g :<: f) => CxtFun g f

Inject a term over a sub signature to a term over larger signature. If the signature g is compound of n atomic signatures, use deepInjectn instead.

split :: f :=: (f1 :+: f2) => (f1 (Term f) :-> a) -> (f2 (Term f) :-> a) -> Term f :-> a

Injections and Projections for Constants

injectConst :: (HFunctor g, g :<: f) => Const g :-> Cxt h f a

projectConst :: (HFunctor g, g :<: f) => NatM Maybe (Cxt h f a) (Const g)

injectCxt :: (HFunctor g, g :<: f) => Cxt h' g (Cxt h f a) :-> Cxt h f a

This function injects a whole context into another context.

liftCxt :: (HFunctor f, g :<: f) => g a :-> Context f a

This function lifts the given functor to a context.

substHoles :: (HFunctor f, HFunctor g, f :<: g) => (v :-> Cxt h g a) -> Cxt h' f v :-> Cxt h g a

This function applies the given context with hole type a to a family f of contexts (possibly terms) indexed by a. That is, each hole h is replaced by the context f h.