compdata-0.5.2: Compositional Data Types

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

Data.Comp.MultiParam.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 :: NatM Maybe (sup a b) (sub a b)Source

Instances

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

data (f :+: g) a b i Source

Formal sum of signatures (difunctors).

Instances

:<: f g => f :<: (:+: h g) 
f :<: (:+: f g) 
(HDifunctor f, HDifunctor g) => HDifunctor (:+: f g) 
(HDitraversable f, HDitraversable g) => HDitraversable (:+: f g) 
(ShowHD f, ShowHD g) => ShowHD (:+: f g) 
(EqHD f, EqHD g) => EqHD (:+: f g)

EqHD is propagated through sums.

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

OrdHD is propagated through sums.

(Desugar f g0, Desugar g g0) => Desugar (:+: f g) g0 
DistAnn s p s' => DistAnn (:+: f s) p (:+: (:&: f p) s') 
RemA s s' => RemA (:+: (:&: f p) s) (:+: f s') 
(Eq (f a b i), Eq (g a b i)) => Eq (:+: f g a b i) 
(Ord (f a b i), Ord (g a b i)) => Ord (:+: f g a b i) 
(Show (f a b i), Show (g a b i)) => Show (:+: f g a b i) 

Projections for Signatures and Terms

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

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

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

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

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

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

proj8 :: forall f a b i 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 i -> Maybe (:+: g8 (:+: g7 (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1)))))) a b i)Source

proj9 :: forall f a b i 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 i -> Maybe (:+: g9 (:+: g8 (:+: g7 (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1))))))) a b i)Source

proj10 :: forall f a b i 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 i -> Maybe (:+: g10 (:+: g9 (:+: g8 (:+: g7 (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1)))))))) a b i)Source

project :: g :<: f => NatM Maybe (Cxt h f a b) (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 i g1 g2. (:<: g1 f, :<: g2 f) => Cxt h f a b i -> Maybe (:+: g2 g1 a (Cxt h f a b) i)Source

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

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

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

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

project7 :: forall h f a b i 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 i -> Maybe (:+: g7 (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1))))) a (Cxt h f a b) i)Source

project8 :: forall h f a b i 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 i -> Maybe (:+: g8 (:+: g7 (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1)))))) a (Cxt h f a b) i)Source

project9 :: forall h f a b i 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 i -> Maybe (:+: g9 (:+: g8 (:+: g7 (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1))))))) a (Cxt h f a b) i)Source

project10 :: forall h f a b i 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 i -> Maybe (:+: g10 (:+: g9 (:+: g8 (:+: g7 (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1)))))))) a (Cxt h f a b) i)Source

deepProject :: (HDitraversable g, g :<: f) => Term f i -> Maybe (Term g i)Source

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 i g1 g2. (HDitraversable (:+: g2 g1), :<: g1 f, :<: g2 f) => Term f i -> Maybe (Term (:+: g2 g1) i)Source

deepProject3 :: forall f i g1 g2 g3. (HDitraversable (:+: g3 (:+: g2 g1)), :<: g1 f, :<: g2 f, :<: g3 f) => Term f i -> Maybe (Term (:+: g3 (:+: g2 g1)) i)Source

deepProject4 :: forall f i g1 g2 g3 g4. (HDitraversable (:+: g4 (:+: g3 (:+: g2 g1))), :<: g1 f, :<: g2 f, :<: g3 f, :<: g4 f) => Term f i -> Maybe (Term (:+: g4 (:+: g3 (:+: g2 g1))) i)Source

deepProject5 :: forall f i g1 g2 g3 g4 g5. (HDitraversable (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1)))), :<: g1 f, :<: g2 f, :<: g3 f, :<: g4 f, :<: g5 f) => Term f i -> Maybe (Term (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1)))) i)Source

deepProject6 :: forall f i g1 g2 g3 g4 g5 g6. (HDitraversable (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1))))), :<: g1 f, :<: g2 f, :<: g3 f, :<: g4 f, :<: g5 f, :<: g6 f) => Term f i -> Maybe (Term (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1))))) i)Source

deepProject7 :: forall f i g1 g2 g3 g4 g5 g6 g7. (HDitraversable (:+: g7 (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1)))))), :<: g1 f, :<: g2 f, :<: g3 f, :<: g4 f, :<: g5 f, :<: g6 f, :<: g7 f) => Term f i -> Maybe (Term (:+: g7 (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1)))))) i)Source

deepProject8 :: forall f i g1 g2 g3 g4 g5 g6 g7 g8. (HDitraversable (:+: g8 (:+: g7 (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1))))))), :<: g1 f, :<: g2 f, :<: g3 f, :<: g4 f, :<: g5 f, :<: g6 f, :<: g7 f, :<: g8 f) => Term f i -> Maybe (Term (:+: g8 (:+: g7 (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1))))))) i)Source

deepProject9 :: forall f i g1 g2 g3 g4 g5 g6 g7 g8 g9. (HDitraversable (:+: g9 (:+: g8 (:+: g7 (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1)))))))), :<: g1 f, :<: g2 f, :<: g3 f, :<: g4 f, :<: g5 f, :<: g6 f, :<: g7 f, :<: g8 f, :<: g9 f) => Term f i -> Maybe (Term (:+: g9 (:+: g8 (:+: g7 (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1)))))))) i)Source

deepProject10 :: forall f i g1 g2 g3 g4 g5 g6 g7 g8 g9 g10. (HDitraversable (:+: g10 (:+: g9 (:+: g8 (:+: g7 (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1))))))))), :<: g1 f, :<: g2 f, :<: g3 f, :<: g4 f, :<: g5 f, :<: g6 f, :<: g7 f, :<: g8 f, :<: g9 f, :<: g10 f) => Term f i -> Maybe (Term (:+: g10 (:+: g9 (:+: g8 (:+: g7 (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1))))))))) i)Source

Injections for Signatures and Terms

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

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

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

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

inj6 :: forall g a b i 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 i -> g a b iSource

inj7 :: forall g a b i 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 i -> g a b iSource

inj8 :: forall g a b i 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 i -> g a b iSource

inj9 :: forall g a b i 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 i -> g a b iSource

inj10 :: forall g a b i 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 i -> g a b iSource

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 i f1 f2. (:<: f1 g, :<: f2 g) => :+: f2 f1 a (Cxt h g a b) i -> Cxt h g a b iSource

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

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

inject5 :: forall h g a b i 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) i -> Cxt h g a b iSource

inject6 :: forall h g a b i 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) i -> Cxt h g a b iSource

inject7 :: forall h g a b i 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) i -> Cxt h g a b iSource

inject8 :: forall h g a b i 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) i -> Cxt h g a b iSource

inject9 :: forall h g a b i 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) i -> Cxt h g a b iSource

inject10 :: forall h g a b i 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) i -> Cxt h g a b iSource

deepInject :: (HDifunctor 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. (HDifunctor (:+: f2 f1), :<: f1 g, :<: f2 g) => CxtFun (:+: f2 f1) gSource

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

deepInject4 :: forall g f1 f2 f3 f4. (HDifunctor (:+: 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. (HDifunctor (:+: 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. (HDifunctor (:+: 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. (HDifunctor (:+: 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. (HDifunctor (:+: 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. (HDifunctor (:+: 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. (HDifunctor (:+: 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

injectCxt :: (HDifunctor 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 :: (HDifunctor f, g :<: f) => g a b :-> Cxt Hole f a bSource

This function lifts the given functor to a context.