compdata-param-0.9.2: Parametric Compositional Data Types

Copyright(c) 2011 Patrick Bahr Tom Hvitved
LicenseBSD3
MaintainerTom Hvitved <hvitved@diku.dk>
Stabilityexperimental
Portabilitynon-portable (GHC Extensions)
Safe HaskellNone
LanguageHaskell98

Data.Comp.Param.Multi.Sum

Contents

Description

This module provides the infrastructure to extend signatures.

Synopsis

Documentation

class (sub :: (* -> *) -> (* -> *) -> * -> *) :<: sup Source #

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.

Minimal complete definition

inj, proj

Instances
f :<: f Source # 
Instance details

Defined in Data.Comp.Param.Multi.Ops

Methods

inj :: f a b i -> f a b i Source #

proj :: f a b i -> Maybe (f a b i) Source #

f :<: g => f :<: (h :+: g) Source # 
Instance details

Defined in Data.Comp.Param.Multi.Ops

Methods

inj :: f a b i -> (h :+: g) a b i Source #

proj :: (h :+: g) a b i -> Maybe (f a b i) Source #

f :<: (f :+: g) Source # 
Instance details

Defined in Data.Comp.Param.Multi.Ops

Methods

inj :: f a b i -> (f :+: g) a b i Source #

proj :: (f :+: g) a b i -> Maybe (f a b i) Source #

data (f :+: g) (a :: * -> *) (b :: * -> *) i infixr 6 Source #

Formal sum of signatures (difunctors).

Instances
f :<: g => f :<: (h :+: g) Source # 
Instance details

Defined in Data.Comp.Param.Multi.Ops

Methods

inj :: f a b i -> (h :+: g) a b i Source #

proj :: (h :+: g) a b i -> Maybe (f a b i) Source #

f :<: (f :+: g) Source # 
Instance details

Defined in Data.Comp.Param.Multi.Ops

Methods

inj :: f a b i -> (f :+: g) a b i Source #

proj :: (f :+: g) a b i -> Maybe (f a b i) Source #

(HDifunctor f, HDifunctor g) => HDifunctor (f :+: g) Source # 
Instance details

Defined in Data.Comp.Param.Multi.Ops

Methods

hdimap :: (a :-> b) -> (c :-> d) -> (f :+: g) b c :-> (f :+: g) a d Source #

(ShowHD f, ShowHD g) => ShowHD (f :+: g) Source # 
Instance details

Defined in Data.Comp.Param.Multi.Show

Methods

showHD :: (f :+: g) Name (K (FreshM String)) i -> FreshM String Source #

(HDitraversable f, HDitraversable g) => HDitraversable (f :+: g) Source # 
Instance details

Defined in Data.Comp.Param.Multi.Ops

Methods

hdimapM :: Monad m => NatM m b c -> NatM m ((f :+: g) a b) ((f :+: g) a c) Source #

(EqHD f, EqHD g) => EqHD (f :+: g) Source #

EqHD is propagated through sums.

Instance details

Defined in Data.Comp.Param.Multi.Equality

Methods

eqHD :: PEq a => (f :+: g) Name a i -> (f :+: g) Name a j -> FreshM Bool Source #

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

OrdHD is propagated through sums.

Instance details

Defined in Data.Comp.Param.Multi.Ordering

Methods

compareHD :: POrd a => (f :+: g) Name a i -> (f :+: g) Name a j -> FreshM Ordering Source #

(Desugar f h, Desugar g h) => Desugar (f :+: g) h Source # 
Instance details

Defined in Data.Comp.Param.Multi.Desugar

Methods

desugHom :: Hom (f :+: g) h Source #

desugHom' :: (f :+: g) a (Cxt h0 h a b) i -> Cxt h0 h a b i Source #

DistAnn s p s' => DistAnn (f :+: s) p ((f :&: p) :+: s') Source # 
Instance details

Defined in Data.Comp.Param.Multi.Ops

Methods

injectA :: p -> (f :+: s) a b :-> ((f :&: p) :+: s') a b Source #

projectA :: ((f :&: p) :+: s') a b i -> ((f :+: s) a b :&: p) i Source #

RemA s s' => RemA ((f :&: p) :+: s) (f :+: s') Source # 
Instance details

Defined in Data.Comp.Param.Multi.Ops

Methods

remA :: ((f :&: p) :+: s) a b i -> (f :+: s') a b i Source #

(Eq (f a b i), Eq (g a b i)) => Eq ((f :+: g) a b i) # 
Instance details

Defined in Data.Comp.Param.Multi.Sum

Methods

(==) :: (f :+: g) a b i -> (f :+: g) a b i -> Bool #

(/=) :: (f :+: g) a b i -> (f :+: g) a b i -> Bool #

(Ord (f a b i), Ord (g a b i)) => Ord ((f :+: g) a b i) # 
Instance details

Defined in Data.Comp.Param.Multi.Sum

Methods

compare :: (f :+: g) a b i -> (f :+: g) a b i -> Ordering #

(<) :: (f :+: g) a b i -> (f :+: g) a b i -> Bool #

(<=) :: (f :+: g) a b i -> (f :+: g) a b i -> Bool #

(>) :: (f :+: g) a b i -> (f :+: g) a b i -> Bool #

(>=) :: (f :+: g) a b i -> (f :+: g) a b i -> Bool #

max :: (f :+: g) a b i -> (f :+: g) a b i -> (f :+: g) a b i #

min :: (f :+: g) a b i -> (f :+: g) a b i -> (f :+: g) a b i #

(Show (f a b i), Show (g a b i)) => Show ((f :+: g) a b i) # 
Instance details

Defined in Data.Comp.Param.Multi.Sum

Methods

showsPrec :: Int -> (f :+: g) a b i -> ShowS #

show :: (f :+: g) a b i -> String #

showList :: [(f :+: g) a b i] -> ShowS #

caseHD :: (f a b i -> c) -> (g a b i -> c) -> (f :+: g) a b i -> c Source #

Utility function to case on a higher-order difunctor sum, without exposing the internal representation of sums.

Projections for Signatures and Terms

proj :: (:<:) sub sup => NatM Maybe (sup a b) (sub a b) Source #

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

inj :: (:<:) sub sup => sub a b :-> sup a b Source #

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

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

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 i Source #

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 i Source #

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 i Source #

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 i Source #

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 i Source #

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 i Source #

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 i Source #

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

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 i Source #

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 i Source #

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 i Source #

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 i Source #

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 i Source #

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 i Source #

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 i Source #

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 i Source #

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 i Source #

deepInject :: (HDifunctor g, g :<: f) => CxtFun g f Source #

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

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

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

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

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

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

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

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

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

injectCxt :: (HDifunctor g, g :<: f) => Cxt h g a (Cxt h f a b) :-> Cxt h f a b Source #

This function injects a whole context into another context.

liftCxt :: (HDifunctor f, g :<: f) => g a b :-> Cxt Hole f a b Source #

This function lifts the given functor to a context.

Orphan instances

(Eq (f a b i), Eq (g a b i)) => Eq ((f :+: g) a b i) Source # 
Instance details

Methods

(==) :: (f :+: g) a b i -> (f :+: g) a b i -> Bool #

(/=) :: (f :+: g) a b i -> (f :+: g) a b i -> Bool #

(Ord (f a b i), Ord (g a b i)) => Ord ((f :+: g) a b i) Source # 
Instance details

Methods

compare :: (f :+: g) a b i -> (f :+: g) a b i -> Ordering #

(<) :: (f :+: g) a b i -> (f :+: g) a b i -> Bool #

(<=) :: (f :+: g) a b i -> (f :+: g) a b i -> Bool #

(>) :: (f :+: g) a b i -> (f :+: g) a b i -> Bool #

(>=) :: (f :+: g) a b i -> (f :+: g) a b i -> Bool #

max :: (f :+: g) a b i -> (f :+: g) a b i -> (f :+: g) a b i #

min :: (f :+: g) a b i -> (f :+: g) a b i -> (f :+: g) a b i #

(Show (f a b i), Show (g a b i)) => Show ((f :+: g) a b i) Source # 
Instance details

Methods

showsPrec :: Int -> (f :+: g) a b i -> ShowS #

show :: (f :+: g) a b i -> String #

showList :: [(f :+: g) a b i] -> ShowS #