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)

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

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

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

EqF is propagated through sums.

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

OrdHF is propagated through sums.

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

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

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

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

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.