Data.Comp.Multi.Sum

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

Documentation

class sub :<: sup where

The subsumption relation.

Methods

inj :: sub a :-> sup a

proj :: NatM Maybe (sup a) (sub a)

Instances

f :<: f

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

f :<: (:+: f g)

data (f :+: g) h e

Data type defining coproducts.

Constructors

Inl (f h e)

Inr (g h e)

Instances

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

f :<: (:+: f g)

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

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

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

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

EqF is propagated through sums.

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

Projections for Signatures and Terms

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

A variant of proj for binary sum signatures.

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

A variant of proj for ternary sum signatures.

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.

project2 :: (g1 :<: f, g2 :<: f) => NatM Maybe (Cxt h f a) ((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) => NatM Maybe (Cxt h f a) ((g1 :+: (g2 :+: g3)) (Cxt h f a))

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

deepProject :: (HTraversable f, HFunctor g, g :<: f) => NatM Maybe (Cxt h f a) (Cxt h g a)

Project a term to a term over a sub signature.

deepProject2 :: (HTraversable f, HFunctor g1, HFunctor g2, g1 :<: f, g2 :<: f) => NatM Maybe (Cxt h f a) (Cxt h (g1 :+: g2) a)

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

deepProject3 :: (HTraversable f, HFunctor g1, HFunctor g2, HFunctor g3, g1 :<: f, g2 :<: f, g3 :<: f) => NatM Maybe (Cxt h f a) (Cxt h (g1 :+: (g2 :+: g3)) a)

Project a term to a term over a ternary sub 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 :: (HFunctor g, HFunctor 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 :: (HFunctor f1, HFunctor f2, HFunctor 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 :: (HFunctor f1, HFunctor f2, HFunctor f3, HFunctor g, f1 :<: g, f2 :<: g, f3 :<: g) => Cxt h (f1 :+: (f2 :+: f3)) a :-> Cxt h g a

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

Injections and Projections for Constants

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

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

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