compdata-0.2: Compositional Data Types

Portability non-portable (GHC Extensions) experimental Patrick Bahr

Data.Comp.Multi.Sum

Description

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

Synopsis

Documentation

class sub :<: sup whereSource

The subsumption relation.

Methods

inj :: sub a :-> sup aSource

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

Instances

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

data (f :+: g) h e Source

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)Source

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)Source

A variant of `proj` for ternary sum signatures.

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

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))Source

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))Source

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)Source

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)Source

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)Source

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 aSource

A variant of `inj` for binary sum signatures.

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

A variant of `inj` for ternary sum signatures.

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

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 aSource

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 aSource

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 aSource

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 aSource

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 aSource

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 aSource

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

injectConst3 :: (HFunctor f1, HFunctor f2, HFunctor f3, HFunctor g, f1 :<: g, f2 :<: g, f3 :<: g) => Const (f1 :+: (f2 :+: f3)) :-> Cxt h g aSource

projectConst :: (HFunctor g, g :<: f) => NatM Maybe (Cxt h f a) (Const g)Source

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

This function injects a whole context into another context.

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

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 aSource

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`.