compdata-0.3: Compositional Data Types

Portabilitynon-portable (GHC Extensions)
Stabilityexperimental
MaintainerTom Hvitved <hvitved@diku.dk>

Data.Comp.Param.Sum

Contents

Description

This module provides the infrastructure to extend signatures.

Synopsis

Documentation

class sub :<: sup whereSource

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 b -> sup a bSource

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

Instances

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

data (f :+: g) a b Source

Formal sum of signatures (difunctors).

Instances

f :<: g => f :<: (:+: h g) 
f :<: (:+: f g) 
(Difunctor f, Difunctor g) => Difunctor (:+: f g) 
(EqD f, EqD g) => EqD (:+: f g)

EqD is propagated through sums.

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

OrdD is propagated through sums.

(ShowD f, ShowD g) => ShowD (:+: f g) 
(Desugar f g[aZw0], Desugar g g[aZw0]) => Desugar (:+: f g) g[aZw0] 
(Ditraversable f m a, Ditraversable g m a) => Ditraversable (:+: f g) m a 
DistAnn s p s' => DistAnn (:+: f s) p (:+: (:&: f p) s') 
RemA s s' => RemA (:+: (:&: f p) s) (:+: f s') 
(Eq (f a b), Eq (g a b)) => Eq (:+: f g a b) 
(Ord (f a b), Ord (g a b)) => Ord (:+: f g a b) 
(Show (f a b), Show (g a b)) => Show (:+: f g a b) 

Projections for Signatures and Terms

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

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

proj4 :: forall f a b g1 g2 g3 g4. (g1 :<: f, g2 :<: f, g3 :<: f, g4 :<: f) => f a b -> Maybe (:+: g4 (:+: g3 (:+: g2 g1)) a b)Source

proj5 :: forall f a b g1 g2 g3 g4 g5. (g1 :<: f, g2 :<: f, g3 :<: f, g4 :<: f, g5 :<: f) => f a b -> Maybe (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1))) a b)Source

proj6 :: forall f a b g1 g2 g3 g4 g5 g6. (g1 :<: f, g2 :<: f, g3 :<: f, g4 :<: f, g5 :<: f, g6 :<: f) => f a b -> Maybe (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1)))) a b)Source

proj7 :: forall f a b g1 g2 g3 g4 g5 g6 g7. (g1 :<: f, g2 :<: f, g3 :<: f, g4 :<: f, g5 :<: f, g6 :<: f, g7 :<: f) => f a b -> Maybe (:+: g7 (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1))))) a b)Source

proj8 :: forall f a b g1 g2 g3 g4 g5 g6 g7 g8. (g1 :<: f, g2 :<: f, g3 :<: f, g4 :<: f, g5 :<: f, g6 :<: f, g7 :<: f, g8 :<: f) => f a b -> Maybe (:+: g8 (:+: g7 (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1)))))) a b)Source

proj9 :: forall f a b g1 g2 g3 g4 g5 g6 g7 g8 g9. (g1 :<: f, g2 :<: f, g3 :<: f, g4 :<: f, g5 :<: f, g6 :<: f, g7 :<: f, g8 :<: f, g9 :<: f) => f a b -> Maybe (:+: g9 (:+: g8 (:+: g7 (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1))))))) a b)Source

proj10 :: forall f a b g1 g2 g3 g4 g5 g6 g7 g8 g9 g10. (g1 :<: f, g2 :<: f, g3 :<: f, g4 :<: f, g5 :<: f, g6 :<: f, g7 :<: f, g8 :<: f, g9 :<: f, g10 :<: f) => f a b -> Maybe (:+: g10 (:+: g9 (:+: g8 (:+: g7 (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1)))))))) a b)Source

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

Project the outermost layer of a term to a sub signature. If the signature g is compound of n atomic signatures, use projectn instead.

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

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

project4 :: forall h f a b g1 g2 g3 g4. (g1 :<: f, g2 :<: f, g3 :<: f, g4 :<: f) => Cxt h f a b -> Maybe (:+: g4 (:+: g3 (:+: g2 g1)) a (Cxt h f a b))Source

project5 :: forall h f a b g1 g2 g3 g4 g5. (g1 :<: f, g2 :<: f, g3 :<: f, g4 :<: f, g5 :<: f) => Cxt h f a b -> Maybe (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1))) a (Cxt h f a b))Source

project6 :: forall h f a b g1 g2 g3 g4 g5 g6. (g1 :<: f, g2 :<: f, g3 :<: f, g4 :<: f, g5 :<: f, g6 :<: f) => Cxt h f a b -> Maybe (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1)))) a (Cxt h f a b))Source

project7 :: forall h f a b g1 g2 g3 g4 g5 g6 g7. (g1 :<: f, g2 :<: f, g3 :<: f, g4 :<: f, g5 :<: f, g6 :<: f, g7 :<: f) => Cxt h f a b -> Maybe (:+: g7 (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1))))) a (Cxt h f a b))Source

project8 :: forall h f a b g1 g2 g3 g4 g5 g6 g7 g8. (g1 :<: f, g2 :<: f, g3 :<: f, g4 :<: f, g5 :<: f, g6 :<: f, g7 :<: f, g8 :<: f) => Cxt h f a b -> Maybe (:+: g8 (:+: g7 (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1)))))) a (Cxt h f a b))Source

project9 :: forall h f a b g1 g2 g3 g4 g5 g6 g7 g8 g9. (g1 :<: f, g2 :<: f, g3 :<: f, g4 :<: f, g5 :<: f, g6 :<: f, g7 :<: f, g8 :<: f, g9 :<: f) => Cxt h f a b -> Maybe (:+: g9 (:+: g8 (:+: g7 (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1))))))) a (Cxt h f a b))Source

project10 :: forall h f a b g1 g2 g3 g4 g5 g6 g7 g8 g9 g10. (g1 :<: f, g2 :<: f, g3 :<: f, g4 :<: f, g5 :<: f, g6 :<: f, g7 :<: f, g8 :<: f, g9 :<: f, g10 :<: f) => Cxt h f a b -> Maybe (:+: g10 (:+: g9 (:+: g8 (:+: g7 (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1)))))))) a (Cxt h f a b))Source

deepProject :: (Ditraversable g Maybe Any, g :<: f) => CxtFunM Maybe f gSource

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.

deepProject2 :: forall f g1 g2. (Ditraversable (:+: g2 g1) Maybe Any, g1 :<: f, g2 :<: f) => CxtFunM Maybe f (:+: g2 g1)Source

deepProject3 :: forall f g1 g2 g3. (Ditraversable (:+: g3 (:+: g2 g1)) Maybe Any, g1 :<: f, g2 :<: f, g3 :<: f) => CxtFunM Maybe f (:+: g3 (:+: g2 g1))Source

deepProject4 :: forall f g1 g2 g3 g4. (Ditraversable (:+: g4 (:+: g3 (:+: g2 g1))) Maybe Any, g1 :<: f, g2 :<: f, g3 :<: f, g4 :<: f) => CxtFunM Maybe f (:+: g4 (:+: g3 (:+: g2 g1)))Source

deepProject5 :: forall f g1 g2 g3 g4 g5. (Ditraversable (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1)))) Maybe Any, g1 :<: f, g2 :<: f, g3 :<: f, g4 :<: f, g5 :<: f) => CxtFunM Maybe f (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1))))Source

deepProject6 :: forall f g1 g2 g3 g4 g5 g6. (Ditraversable (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1))))) Maybe Any, g1 :<: f, g2 :<: f, g3 :<: f, g4 :<: f, g5 :<: f, g6 :<: f) => CxtFunM Maybe f (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1)))))Source

deepProject7 :: forall f g1 g2 g3 g4 g5 g6 g7. (Ditraversable (:+: g7 (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1)))))) Maybe Any, g1 :<: f, g2 :<: f, g3 :<: f, g4 :<: f, g5 :<: f, g6 :<: f, g7 :<: f) => CxtFunM Maybe f (:+: g7 (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1))))))Source

deepProject8 :: forall f g1 g2 g3 g4 g5 g6 g7 g8. (Ditraversable (:+: g8 (:+: g7 (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1))))))) Maybe Any, g1 :<: f, g2 :<: f, g3 :<: f, g4 :<: f, g5 :<: f, g6 :<: f, g7 :<: f, g8 :<: f) => CxtFunM Maybe f (:+: g8 (:+: g7 (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1)))))))Source

deepProject9 :: forall f g1 g2 g3 g4 g5 g6 g7 g8 g9. (Ditraversable (:+: g9 (:+: g8 (:+: g7 (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1)))))))) Maybe Any, g1 :<: f, g2 :<: f, g3 :<: f, g4 :<: f, g5 :<: f, g6 :<: f, g7 :<: f, g8 :<: f, g9 :<: f) => CxtFunM Maybe f (:+: g9 (:+: g8 (:+: g7 (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1))))))))Source

deepProject10 :: forall f g1 g2 g3 g4 g5 g6 g7 g8 g9 g10. (Ditraversable (:+: g10 (:+: g9 (:+: g8 (:+: g7 (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1))))))))) Maybe Any, g1 :<: f, g2 :<: f, g3 :<: f, g4 :<: f, g5 :<: f, g6 :<: f, g7 :<: f, g8 :<: f, g9 :<: f, g10 :<: f) => CxtFunM Maybe f (:+: g10 (:+: g9 (:+: g8 (:+: g7 (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1)))))))))Source

Injections for Signatures and Terms

inj2 :: forall g a b f1 f2. (f1 :<: g, f2 :<: g) => :+: f2 f1 a b -> g a bSource

inj3 :: forall g a b f1 f2 f3. (f1 :<: g, f2 :<: g, f3 :<: g) => :+: f3 (:+: f2 f1) a b -> g a bSource

inj4 :: forall g a b f1 f2 f3 f4. (f1 :<: g, f2 :<: g, f3 :<: g, f4 :<: g) => :+: f4 (:+: f3 (:+: f2 f1)) a b -> g a bSource

inj5 :: forall g a b f1 f2 f3 f4 f5. (f1 :<: g, f2 :<: g, f3 :<: g, f4 :<: g, f5 :<: g) => :+: f5 (:+: f4 (:+: f3 (:+: f2 f1))) a b -> g a bSource

inj6 :: forall g a b f1 f2 f3 f4 f5 f6. (f1 :<: g, f2 :<: g, f3 :<: g, f4 :<: g, f5 :<: g, f6 :<: g) => :+: f6 (:+: f5 (:+: f4 (:+: f3 (:+: f2 f1)))) a b -> g a bSource

inj7 :: forall g a b f1 f2 f3 f4 f5 f6 f7. (f1 :<: g, f2 :<: g, f3 :<: g, f4 :<: g, f5 :<: g, f6 :<: g, f7 :<: g) => :+: f7 (:+: f6 (:+: f5 (:+: f4 (:+: f3 (:+: f2 f1))))) a b -> g a bSource

inj8 :: forall g a b f1 f2 f3 f4 f5 f6 f7 f8. (f1 :<: g, f2 :<: g, f3 :<: g, f4 :<: g, f5 :<: g, f6 :<: g, f7 :<: g, f8 :<: g) => :+: f8 (:+: f7 (:+: f6 (:+: f5 (:+: f4 (:+: f3 (:+: f2 f1)))))) a b -> g a bSource

inj9 :: forall g a b f1 f2 f3 f4 f5 f6 f7 f8 f9. (f1 :<: g, f2 :<: g, f3 :<: g, f4 :<: g, f5 :<: g, f6 :<: g, f7 :<: g, f8 :<: g, f9 :<: g) => :+: f9 (:+: f8 (:+: f7 (:+: f6 (:+: f5 (:+: f4 (:+: f3 (:+: f2 f1))))))) a b -> g a bSource

inj10 :: forall g a b f1 f2 f3 f4 f5 f6 f7 f8 f9 f10. (f1 :<: g, f2 :<: g, f3 :<: g, f4 :<: g, f5 :<: g, f6 :<: g, f7 :<: g, f8 :<: g, f9 :<: g, f10 :<: g) => :+: f10 (:+: f9 (:+: f8 (:+: f7 (:+: f6 (:+: f5 (:+: f4 (:+: f3 (:+: f2 f1)))))))) a b -> g a bSource

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

Inject a term where the outermost layer is a sub signature. If the signature g is compound of n atomic signatures, use injectn instead.

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

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

inject4 :: forall h g a b f1 f2 f3 f4. (f1 :<: g, f2 :<: g, f3 :<: g, f4 :<: g) => :+: f4 (:+: f3 (:+: f2 f1)) a (Cxt h g a b) -> Cxt h g a bSource

inject5 :: forall h g a b f1 f2 f3 f4 f5. (f1 :<: g, f2 :<: g, f3 :<: g, f4 :<: g, f5 :<: g) => :+: f5 (:+: f4 (:+: f3 (:+: f2 f1))) a (Cxt h g a b) -> Cxt h g a bSource

inject6 :: forall h g a b f1 f2 f3 f4 f5 f6. (f1 :<: g, f2 :<: g, f3 :<: g, f4 :<: g, f5 :<: g, f6 :<: g) => :+: f6 (:+: f5 (:+: f4 (:+: f3 (:+: f2 f1)))) a (Cxt h g a b) -> Cxt h g a bSource

inject7 :: forall h g a b f1 f2 f3 f4 f5 f6 f7. (f1 :<: g, f2 :<: g, f3 :<: g, f4 :<: g, f5 :<: g, f6 :<: g, f7 :<: g) => :+: f7 (:+: f6 (:+: f5 (:+: f4 (:+: f3 (:+: f2 f1))))) a (Cxt h g a b) -> Cxt h g a bSource

inject8 :: forall h g a b f1 f2 f3 f4 f5 f6 f7 f8. (f1 :<: g, f2 :<: g, f3 :<: g, f4 :<: g, f5 :<: g, f6 :<: g, f7 :<: g, f8 :<: g) => :+: f8 (:+: f7 (:+: f6 (:+: f5 (:+: f4 (:+: f3 (:+: f2 f1)))))) a (Cxt h g a b) -> Cxt h g a bSource

inject9 :: forall h g a b f1 f2 f3 f4 f5 f6 f7 f8 f9. (f1 :<: g, f2 :<: g, f3 :<: g, f4 :<: g, f5 :<: g, f6 :<: g, f7 :<: g, f8 :<: g, f9 :<: g) => :+: f9 (:+: f8 (:+: f7 (:+: f6 (:+: f5 (:+: f4 (:+: f3 (:+: f2 f1))))))) a (Cxt h g a b) -> Cxt h g a bSource

inject10 :: forall h g a b f1 f2 f3 f4 f5 f6 f7 f8 f9 f10. (f1 :<: g, f2 :<: g, f3 :<: g, f4 :<: g, f5 :<: g, f6 :<: g, f7 :<: g, f8 :<: g, f9 :<: g, f10 :<: g) => :+: f10 (:+: f9 (:+: f8 (:+: f7 (:+: f6 (:+: f5 (:+: f4 (:+: f3 (:+: f2 f1)))))))) a (Cxt h g a b) -> Cxt h g a bSource

deepInject :: (Difunctor g, g :<: f) => CxtFun g fSource

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.

deepInject2 :: forall g f1 f2. (Difunctor (:+: f2 f1), f1 :<: g, f2 :<: g) => CxtFun (:+: f2 f1) gSource

deepInject3 :: forall g f1 f2 f3. (Difunctor (:+: f3 (:+: f2 f1)), f1 :<: g, f2 :<: g, f3 :<: g) => CxtFun (:+: f3 (:+: f2 f1)) gSource

deepInject4 :: forall g f1 f2 f3 f4. (Difunctor (:+: f4 (:+: f3 (:+: f2 f1))), f1 :<: g, f2 :<: g, f3 :<: g, f4 :<: g) => CxtFun (:+: f4 (:+: f3 (:+: f2 f1))) gSource

deepInject5 :: forall g f1 f2 f3 f4 f5. (Difunctor (:+: f5 (:+: f4 (:+: f3 (:+: f2 f1)))), f1 :<: g, f2 :<: g, f3 :<: g, f4 :<: g, f5 :<: g) => CxtFun (:+: f5 (:+: f4 (:+: f3 (:+: f2 f1)))) gSource

deepInject6 :: forall g f1 f2 f3 f4 f5 f6. (Difunctor (:+: f6 (:+: f5 (:+: f4 (:+: f3 (:+: f2 f1))))), f1 :<: g, f2 :<: g, f3 :<: g, f4 :<: g, f5 :<: g, f6 :<: g) => CxtFun (:+: f6 (:+: f5 (:+: f4 (:+: f3 (:+: f2 f1))))) gSource

deepInject7 :: forall g f1 f2 f3 f4 f5 f6 f7. (Difunctor (:+: f7 (:+: f6 (:+: f5 (:+: f4 (:+: f3 (:+: f2 f1)))))), f1 :<: g, f2 :<: g, f3 :<: g, f4 :<: g, f5 :<: g, f6 :<: g, f7 :<: g) => CxtFun (:+: f7 (:+: f6 (:+: f5 (:+: f4 (:+: f3 (:+: f2 f1)))))) gSource

deepInject8 :: forall g f1 f2 f3 f4 f5 f6 f7 f8. (Difunctor (:+: f8 (:+: f7 (:+: f6 (:+: f5 (:+: f4 (:+: f3 (:+: f2 f1))))))), f1 :<: g, f2 :<: g, f3 :<: g, f4 :<: g, f5 :<: g, f6 :<: g, f7 :<: g, f8 :<: g) => CxtFun (:+: f8 (:+: f7 (:+: f6 (:+: f5 (:+: f4 (:+: f3 (:+: f2 f1))))))) gSource

deepInject9 :: forall g f1 f2 f3 f4 f5 f6 f7 f8 f9. (Difunctor (:+: f9 (:+: f8 (:+: f7 (:+: f6 (:+: f5 (:+: f4 (:+: f3 (:+: f2 f1)))))))), f1 :<: g, f2 :<: g, f3 :<: g, f4 :<: g, f5 :<: g, f6 :<: g, f7 :<: g, f8 :<: g, f9 :<: g) => CxtFun (:+: f9 (:+: f8 (:+: f7 (:+: f6 (:+: f5 (:+: f4 (:+: f3 (:+: f2 f1)))))))) gSource

deepInject10 :: forall g f1 f2 f3 f4 f5 f6 f7 f8 f9 f10. (Difunctor (:+: f10 (:+: f9 (:+: f8 (:+: f7 (:+: f6 (:+: f5 (:+: f4 (:+: f3 (:+: f2 f1))))))))), f1 :<: g, f2 :<: g, f3 :<: g, f4 :<: g, f5 :<: g, f6 :<: g, f7 :<: g, f8 :<: g, f9 :<: g, f10 :<: g) => CxtFun (:+: f10 (:+: f9 (:+: f8 (:+: f7 (:+: f6 (:+: f5 (:+: f4 (:+: f3 (:+: f2 f1))))))))) gSource

Injections and Projections for Constants

injectConst :: (Difunctor g, g :<: f) => Const g -> Cxt h f Any aSource

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

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

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

injectCxt :: (Difunctor g, g :<: f) => Cxt h g a (Cxt h f a b) -> Cxt h f a bSource

This function injects a whole context into another context.

liftCxt :: (Difunctor f, g :<: f) => g a b -> Cxt Hole f a bSource

This function lifts the given functor to a context.