Data.Comp.Sum

This module provides the infrastructure to extend signatures.

Documentation

class sub :<: sup where

Signature containment relation for automatic injections. The left-hand must be an atomic signature, where as the right-hand side must have a list-like structure. Examples include f :<: f :+: g and g :<: f :+: (g :+: h), non-examples include f :+: g :<: f :+: (g :+: h) and f :<: (f :+: g) :+: h.

Methods

inj :: sub a -> sup a

proj :: sup a -> Maybe (sub a)

Instances

f :<: f

f :<: g => f :<: (:+: h g)

f :<: (:+: f g)

data (f :+: g) e

Formal sum of signatures (functors).

Constructors

Inl (f e)

Inr (g e)

Instances

f :<: g => f :<: (:+: h g)

f :<: (:+: f g)

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

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

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

(ShowF f, ShowF g) => ShowF (:+: 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.

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

Instances of ArbitraryF are closed under forming sums.

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

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

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

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

RemoveP s s' => RemoveP (:+: (:&: 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)

Projections for Signatures and Terms

proj2 :: forall f g1 g2 a. (g1 :<: f, g2 :<: f) => f a -> Maybe ((g1 :+: g2) a)

A variant of proj for binary sum signatures.

proj3 :: forall f g1 g2 g3 a. (g1 :<: f, g2 :<: f, g3 :<: f) => f a -> Maybe ((g1 :+: (g2 :+: g3)) a)

A variant of proj for ternary sum signatures.

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

Project the outermost layer of a term to a sub signature.

project2 :: (g1 :<: f, g2 :<: f) => Cxt h f a -> Maybe ((g1 :+: g2) (Cxt h f a))

Project the outermost layer of a term to a binary sub signature.

project3 :: (g1 :<: f, g2 :<: f, g3 :<: f) => Cxt h f a -> Maybe ((g1 :+: (g2 :+: g3)) (Cxt h f a))

Project the outermost layer of a term to a ternary sub signature.

deepProject :: (Traversable f, Functor g, g :<: f) => Cxt h f a -> Maybe (Cxt h g a)

Project a term to a term over a sub signature.

deepProject2 :: (Traversable f, Functor g1, Functor g2, g1 :<: f, g2 :<: f) => Cxt h f a -> Maybe (Cxt h (g1 :+: g2) a)

Project a term to a term over a binary sub signature.

deepProject3 :: (Traversable f, Functor g1, Functor g2, Functor g3, g1 :<: f, g2 :<: f, g3 :<: f) => Cxt h f a -> Maybe (Cxt h (g1 :+: (g2 :+: g3)) a)

Project a term to a term over a ternary sub signature.

deepProject' :: forall g f h a. (Traversable g, g :<: f) => Cxt h f a -> Maybe (Cxt h g a)

A variant of deepProject where the sub signature is required to be Traversable rather than the whole signature.

deepProject2' :: forall g1 g2 f h a. (Traversable g1, Traversable g2, g1 :<: f, g2 :<: f) => Cxt h f a -> Maybe (Cxt h (g1 :+: g2) a)

A variant of deepProject2 where the sub signatures are required to be Traversable rather than the whole signature.

deepProject3' :: forall g1 g2 g3 f h a. (Traversable g1, Traversable g2, Traversable g3, g1 :<: f, g2 :<: f, g3 :<: f) => Cxt h f a -> Maybe (Cxt h (g1 :+: (g2 :+: g3)) a)

A variant of deepProject3 where the sub signatures are required to be Traversable rather than the whole signature.

Injections for Signatures and Terms

inj2 :: (f1 :<: g, f2 :<: g) => (f1 :+: f2) a -> g a

A variant of inj for binary sum signatures.

inj3 :: (f1 :<: g, f2 :<: g, f3 :<: g) => (f1 :+: (f2 :+: f3)) a -> g a

A variant of inj for ternary sum signatures.

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

Inject a term where the outermost layer is a sub signature.

inject2 :: (f1 :<: g, f2 :<: g) => (f1 :+: f2) (Cxt h g a) -> Cxt h g a

Inject a term where the outermost layer is a binary sub signature.

inject3 :: (f1 :<: g, f2 :<: g, f3 :<: g) => (f1 :+: (f2 :+: f3)) (Cxt h g a) -> Cxt h g a

Inject a term where the outermost layer is a ternary sub signature.

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

Inject a term over a sub signature to a term over larger signature.

deepInject2 :: (Functor f1, Functor f2, Functor g, f1 :<: g, f2 :<: g) => Cxt h (f1 :+: f2) a -> Cxt h g a

Inject a term over a binary sub signature to a term over larger signature.

deepInject3 :: (Functor f1, Functor f2, Functor f3, Functor g, f1 :<: g, f2 :<: g, f3 :<: g) => Cxt h (f1 :+: (f2 :+: f3)) a -> Cxt h g a

Inject a term over a ternary signature to a term over larger signature.

deepInjectE :: (ExpFunctor g, g :<: f) => Term g -> Term f

A variant of deepInject for exponential signatures.

deepInjectE2 :: (ExpFunctor g1, ExpFunctor g2, g1 :<: f, g2 :<: f) => Term (g1 :+: g2) -> Term f

A variant of deepInject2 for exponential signatures.

deepInjectE3 :: (ExpFunctor g1, ExpFunctor g2, ExpFunctor g3, g1 :<: f, g2 :<: f, g3 :<: f) => Term (g1 :+: (g2 :+: g3)) -> Term f

A variant of deepInject3 for exponential signatures.

Injections and Projections for Constants

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

injectConst2 :: (Functor f1, Functor f2, Functor g, f1 :<: g, f2 :<: g) => Const (f1 :+: f2) -> Cxt h g a

injectConst3 :: (Functor f1, Functor f2, Functor f3, Functor g, f1 :<: g, f2 :<: g, f3 :<: g) => Const (f1 :+: (f2 :+: f3)) -> Cxt h g 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