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

hinj :: sub a :-> sup a

hproj :: 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

HInl (f h e)

HInr (g h e)

Instances

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

f :<<: (:++: f g)

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

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

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

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

Projections for Signatures and Terms

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

A variant of hproj for binary sum signatures.

hproj3 :: 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 hproj for ternary sum signatures.

hproject :: g :<<: f => NatM Maybe (HCxt h f a) (g (HCxt h f a))

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

hproject2 :: (g1 :<<: f, g2 :<<: f) => NatM Maybe (HCxt h f a) ((g1 :++: g2) (HCxt h f a))

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

hproject3 :: (g1 :<<: f, g2 :<<: f, g3 :<<: f) => NatM Maybe (HCxt h f a) ((g1 :++: (g2 :++: g3)) (HCxt h f a))

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

deepHProject :: (HTraversable f, HFunctor g, g :<<: f) => NatM Maybe (HCxt h f a) (HCxt h g a)

Project a term to a term over a sub signature.

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

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

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

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

Injections for Signatures and Terms

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

A variant of hinj for binary sum signatures.

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

A variant of hinj for ternary sum signatures.

hinject :: g :<<: f => g (HCxt h f a) :-> HCxt h f a

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

hinject2 :: (f1 :<<: g, f2 :<<: g) => (f1 :++: f2) (HCxt h g a) :-> HCxt h g a

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

hinject3 :: (f1 :<<: g, f2 :<<: g, f3 :<<: g) => (f1 :++: (f2 :++: f3)) (HCxt h g a) :-> HCxt h g a

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

deepHInject :: (HFunctor g, HFunctor f, g :<<: f) => HCxt h g a :-> HCxt h f a

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

deepHInject2 :: (HFunctor f1, HFunctor f2, HFunctor g, f1 :<<: g, f2 :<<: g) => HCxt h (f1 :++: f2) a :-> HCxt h g a

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

deepHInject3 :: (HFunctor f1, HFunctor f2, HFunctor f3, HFunctor g, f1 :<<: g, f2 :<<: g, f3 :<<: g) => HCxt h (f1 :++: (f2 :++: f3)) a :-> HCxt h g a

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

deepHInjectE :: (HExpFunctor g, g :<<: f) => HTerm g :-> HTerm f

A variant of deepHInject for exponential signatures.

deepHInjectE2 :: (HExpFunctor g1, HExpFunctor g2, g1 :<<: f, g2 :<<: f) => HTerm (g1 :++: g2) :-> HTerm f

A variant of deepHInject2 for exponential signatures.

deepHInjectE3 :: (HExpFunctor g1, HExpFunctor g2, HExpFunctor g3, g1 :<<: f, g2 :<<: f, g3 :<<: f) => HTerm (g1 :++: (g2 :++: g3)) :-> HTerm f

A variant of deepHInject3 for exponential signatures.

Injections and Projections for Constants

hinjectHConst :: (HFunctor g, g :<<: f) => HConst g :-> HCxt h f a

hinjectHConst2 :: (HFunctor f1, HFunctor f2, HFunctor g, f1 :<<: g, f2 :<<: g) => HConst (f1 :++: f2) :-> HCxt h g a

hinjectHConst3 :: (HFunctor f1, HFunctor f2, HFunctor f3, HFunctor g, f1 :<<: g, f2 :<<: g, f3 :<<: g) => HConst (f1 :++: (f2 :++: f3)) :-> HCxt h g a

hprojectHConst :: (HFunctor g, g :<<: f) => NatM Maybe (HCxt h f a) (HConst g)

hinjectHCxt :: (HFunctor g, g :<<: f) => HCxt h' g (HCxt h f a) :-> HCxt h f a

This function injects a whole context into another context.

liftHCxt :: (HFunctor f, g :<<: f) => g a :-> HContext f a

This function lifts the given functor to a context.

substHHoles :: (HFunctor f, HFunctor g, f :<<: g) => (v :-> HCxt h g a) -> HCxt h' f v :-> HCxt 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.