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)

Methods

hfmap :: (f :-> g) -> (* :+: f) g f :-> (* :+: f) g g

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

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)

Methods

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

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

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

EqF is propagated through sums.

Methods

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

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

OrdHF is propagated through sums.

Methods

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

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

Methods

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

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

(HasVars f v0, HasVars g v0) => HasVars ((:+:) * f g) v0

Methods

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

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

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

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')

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.