Data.Comp.Sum

This module provides the infrastructure to extend signatures.

Documentation

type (:<:) f g = (GetEmbD (GetEmb f g) f g, NoDup (Duplicates (GetEmb f g)) f g) infixl 5

The :<: constraint is a conjunction of two constraints. The first one is used to construct the evidence that is used to implement the injection and projection functions. The first constraint alone would allow instances such as F :+: F :<: F or F :+: (F :+: G) :<: F :+: G which have multiple occurrences of the same sub-signature on the left-hand side. Such instances are usually unintended and yield injection functions that are not injective. The second constraint excludes such instances.

type (:=:) f g = (f :<: g, g :<: f) infixl 5

data (f :+: g) e infixr 6

Formal sum of signatures (functors).

Instances

GetEmbD (Found p) f g => GetEmbD (Found (GoRight p)) f ((:+:) g' g)

GetEmbD (Found p) f g => GetEmbD (Found (GoLeft p)) f ((:+:) g g')

(GetEmbD (Found p1) f1 g, GetEmbD (Found p2) f2 g) => GetEmbD (Found (Sum p1 p2)) ((:+:) f1 f2) g

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

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

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

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

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

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

Instances of ArbitraryF are closed under forming sums.

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

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

EqF is propagated through sums.

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

OrdF is propagated through sums.

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

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

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

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

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

(Eq (f a), Eq (g a)) => Eq ((:+:) f g a)

(Ord (f a), Ord (g a)) => Ord ((:+:) f g a)

(Show (f a), Show (g a)) => Show ((:+:) f g a)

caseF :: (f a -> b) -> (g a -> b) -> (f :+: g) a -> b

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

Projections for Signatures and Terms

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

project :: g :<: f => Cxt h f a -> Maybe (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 :: (Traversable 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.

project_ :: SigFunM Maybe f g -> Cxt h f a -> Maybe (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_ :: Traversable g => SigFunM Maybe f g -> 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 :: (Functor 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.

inject_ :: SigFun 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_ :: Functor g => SigFun 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 :: (Functor g, g :<: f) => Const g -> Cxt h f a

projectConst :: (Functor g, g :<: f) => Cxt h f a -> Maybe (Const g)

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

This function injects a whole context into another context.

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

This function lifts the given functor to a context.

substHoles :: (Functor f, Functor g, f :<: g) => Cxt h' f v -> (v -> Cxt h g a) -> 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.

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