Copyright	(c) 2011 Patrick Bahr
License	BSD3
Maintainer	Patrick Bahr <[email protected]>
Stability	experimental
Portability	non-portable (GHC Extensions)
Safe Haskell	None
Language	Haskell2010

Data.Comp.Multi.Sum

Contents

Projections for Signatures and Terms
Injections for Signatures and Terms
Injections and Projections for Constants

Description

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

Synopsis

type (:<:) (f :: (Type -> Type) -> Type -> Type) (g :: (Type -> Type) -> Type -> Type) = Subsume (ComprEmb (Elem f g)) f g
data ((f :: (Type -> Type) -> k -> Type) :+: (g :: (Type -> Type) -> k -> Type)) (h :: Type -> Type) (e :: k)
caseH :: forall {k} f (a :: Type -> Type) (b :: k) c g. (f a b -> c) -> (g a b -> c) -> (f :+: g) a b -> c
proj :: forall (f :: (Type -> Type) -> Type -> Type) (g :: (Type -> Type) -> Type -> Type) (a :: Type -> Type). f :<: g => NatM Maybe (g a) (f a)
project :: forall (g :: (Type -> Type) -> Type -> Type) (f :: (Type -> Type) -> Type -> Type) h (a :: Type -> Type). g :<: f => NatM Maybe (Cxt h f a) (g (Cxt h f a))
deepProject :: forall (g :: (Type -> Type) -> Type -> Type) (f :: (Type -> Type) -> Type -> Type). (HTraversable g, g :<: f) => CxtFunM Maybe f g
inj :: forall (f :: (Type -> Type) -> Type -> Type) (g :: (Type -> Type) -> Type -> Type) (a :: Type -> Type). f :<: g => f a :-> g a
inject :: forall (g :: (Type -> Type) -> Type -> Type) (f :: (Type -> Type) -> Type -> Type) h (a :: Type -> Type). g :<: f => g (Cxt h f a) :-> Cxt h f a
deepInject :: forall (g :: (Type -> Type) -> Type -> Type) (f :: (Type -> Type) -> Type -> Type). (HFunctor g, g :<: f) => CxtFun g f
split :: forall (f :: (Type -> Type) -> Type -> Type) (f1 :: (Type -> Type) -> Type -> Type) (f2 :: (Type -> Type) -> Type -> Type) (a :: Type -> Type). f :=: (f1 :+: f2) => (f1 (Term f) :-> a) -> (f2 (Term f) :-> a) -> Term f :-> a
injectConst :: forall (g :: (Type -> Type) -> Type -> Type) (f :: (Type -> Type) -> Type -> Type) h (a :: Type -> Type). (HFunctor g, g :<: f) => Const g :-> Cxt h f a
projectConst :: forall (g :: (Type -> Type) -> Type -> Type) (f :: (Type -> Type) -> Type -> Type) h (a :: Type -> Type). (HFunctor g, g :<: f) => NatM Maybe (Cxt h f a) (Const g)
injectCxt :: forall (g :: (Type -> Type) -> Type -> Type) (f :: (Type -> Type) -> Type -> Type) h' h (a :: Type -> Type). (HFunctor g, g :<: f) => Cxt h' g (Cxt h f a) :-> Cxt h f a
liftCxt :: forall (f :: (Type -> Type) -> Type -> Type) (g :: (Type -> Type) -> Type -> Type) (a :: Type -> Type). (HFunctor f, g :<: f) => g a :-> Context f a
substHoles :: forall (f :: (Type -> Type) -> Type -> Type) (g :: (Type -> Type) -> Type -> Type) (v :: Type -> Type) h (a :: Type -> Type) h'. (HFunctor f, HFunctor g, f :<: g) => (v :-> Cxt h g a) -> Cxt h' f v :-> Cxt h g a

Documentation

type (:<:) (f :: (Type -> Type) -> Type -> Type) (g :: (Type -> Type) -> Type -> Type) = Subsume (ComprEmb (Elem f g)) f g infixl 5 Source #

A constraint f :<: g expresses that the signature f is subsumed by g, i.e. f can be used to construct elements in g.

data ((f :: (Type -> Type) -> k -> Type) :+: (g :: (Type -> Type) -> k -> Type)) (h :: Type -> Type) (e :: k) infixr 6 Source #

Data type defining coproducts.

Instances

Instances details

(ShowHF f, ShowHF g) => ShowHF (f :+: g) Source #
Instance details Defined in Data.Comp.Multi.Show Methods showHF :: Alg (f :+: g) (K String) Source # showHF' :: (f :+: g) (K String) :=> String Source #
(EqHF f, EqHF g) => EqHF (f :+: g) Source #	`EqF` is propagated through sums.
Instance details Defined in Data.Comp.Multi.Equality Methods eqHF :: forall (g0 :: Type -> Type) i j. KEq g0 => (f :+: g) g0 i -> (f :+: g) g0 j -> Bool Source #
(HFoldable f, HFoldable g) => HFoldable (f :+: g) Source #
Instance details Defined in Data.Comp.Multi.Ops Methods hfold :: Monoid m => (f :+: g) (K m) :=> m Source # hfoldMap :: forall m (a :: Type -> Type). Monoid m => (a :=> m) -> (f :+: g) a :=> m Source # hfoldr :: forall (a :: Type -> Type) b. (a :=> (b -> b)) -> b -> (f :+: g) a :=> b Source # hfoldl :: forall b (a :: Type -> Type). (b -> a :=> b) -> b -> (f :+: g) a :=> b Source # hfoldr1 :: (a -> a -> a) -> (f :+: g) (K a) :=> a Source # hfoldl1 :: (a -> a -> a) -> (f :+: g) (K a) :=> a Source #
(HFunctor f, HFunctor g) => HFunctor (f :+: g) Source #
Instance details Defined in Data.Comp.Multi.Ops Methods hfmap :: forall (f0 :: Type -> Type) (g0 :: Type -> Type). (f0 :-> g0) -> (f :+: g) f0 :-> (f :+: g) g0 Source #
(HTraversable f, HTraversable g) => HTraversable (f :+: g) Source #
Instance details Defined in Data.Comp.Multi.Ops Methods hmapM :: forall (m :: Type -> Type) (a :: Type -> Type) (b :: Type -> Type). Monad m => NatM m a b -> NatM m ((f :+: g) a) ((f :+: g) b) Source # htraverse :: forall (f0 :: Type -> Type) (a :: Type -> Type) (b :: Type -> Type). Applicative f0 => NatM f0 a b -> NatM f0 ((f :+: g) a) ((f :+: g) b) Source #
(OrdHF f, OrdHF g) => OrdHF (f :+: g) Source #	`OrdHF` is propagated through sums.
Instance details Defined in Data.Comp.Multi.Ordering Methods compareHF :: forall (a :: Type -> Type) i j. KOrd a => (f :+: g) a i -> (f :+: g) a j -> Ordering Source #
(Desugar f h, Desugar g h) => Desugar (f :+: g) h Source #
Instance details Defined in Data.Comp.Multi.Desugar Methods desugHom :: Hom (f :+: g) h Source # desugHom' :: forall (a :: Type -> Type). Alg (f :+: g) (Context h a) Source #
(HasVars f v, HasVars g v) => HasVars (f :+: g) v Source #
Instance details Defined in Data.Comp.Multi.Variables Methods isVar :: forall (a :: Type -> Type). (f :+: g) a :=> Maybe v Source # bindsVars :: forall (m :: Type -> Type) (a :: Type -> Type). Mapping m a => (f :+: g) a :=> m (Set v) Source #
DistAnn s p s' => DistAnn (f :+: s) p ((f :&: p) :+: s') Source #
Instance details Defined in Data.Comp.Multi.Ops Methods injectA :: forall (a :: Type -> Type). p -> (f :+: s) a :-> ((f :&: p) :+: s') a Source # projectA :: forall (a :: Type -> Type). ((f :&: p) :+: s') a :-> ((f :+: s) a :&: p) Source #
RemA s s' => RemA ((f :&: p) :+: s) (f :+: s') Source #
Instance details Defined in Data.Comp.Multi.Ops Methods remA :: forall (a :: Type -> Type). ((f :&: p) :+: s) a :-> (f :+: s') a Source #

caseH :: forall {k} f (a :: Type -> Type) (b :: k) c g. (f a b -> c) -> (g a b -> c) -> (f :+: g) a b -> c Source #

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

Projections for Signatures and Terms

proj :: forall (f :: (Type -> Type) -> Type -> Type) (g :: (Type -> Type) -> Type -> Type) (a :: Type -> Type). f :<: g => NatM Maybe (g a) (f a) Source #

project :: forall (g :: (Type -> Type) -> Type -> Type) (f :: (Type -> Type) -> Type -> Type) h (a :: Type -> Type). 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. If the signature g is compound of n atomic signatures, use projectn instead.

deepProject :: forall (g :: (Type -> Type) -> Type -> Type) (f :: (Type -> Type) -> Type -> Type). (HTraversable g, g :<: f) => CxtFunM Maybe f g 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.

Injections for Signatures and Terms

inj :: forall (f :: (Type -> Type) -> Type -> Type) (g :: (Type -> Type) -> Type -> Type) (a :: Type -> Type). f :<: g => f a :-> g a Source #

inject :: forall (g :: (Type -> Type) -> Type -> Type) (f :: (Type -> Type) -> Type -> Type) h (a :: Type -> Type). g :<: f => g (Cxt h f a) :-> Cxt h f a 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.

deepInject :: forall (g :: (Type -> Type) -> Type -> Type) (f :: (Type -> Type) -> Type -> Type). (HFunctor 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.

split :: forall (f :: (Type -> Type) -> Type -> Type) (f1 :: (Type -> Type) -> Type -> Type) (f2 :: (Type -> Type) -> Type -> Type) (a :: Type -> Type). f :=: (f1 :+: f2) => (f1 (Term f) :-> a) -> (f2 (Term f) :-> a) -> Term f :-> a Source #

Injections and Projections for Constants

injectConst :: forall (g :: (Type -> Type) -> Type -> Type) (f :: (Type -> Type) -> Type -> Type) h (a :: Type -> Type). (HFunctor g, g :<: f) => Const g :-> Cxt h f a Source #

projectConst :: forall (g :: (Type -> Type) -> Type -> Type) (f :: (Type -> Type) -> Type -> Type) h (a :: Type -> Type). (HFunctor g, g :<: f) => NatM Maybe (Cxt h f a) (Const g) Source #

injectCxt :: forall (g :: (Type -> Type) -> Type -> Type) (f :: (Type -> Type) -> Type -> Type) h' h (a :: Type -> Type). (HFunctor g, g :<: f) => Cxt h' g (Cxt h f a) :-> Cxt h f a Source #

This function injects a whole context into another context.

liftCxt :: forall (f :: (Type -> Type) -> Type -> Type) (g :: (Type -> Type) -> Type -> Type) (a :: Type -> Type). (HFunctor f, g :<: f) => g a :-> Context f a Source #

This function lifts the given functor to a context.

substHoles :: forall (f :: (Type -> Type) -> Type -> Type) (g :: (Type -> Type) -> Type -> Type) (v :: Type -> Type) h (a :: Type -> Type) h'. (HFunctor f, HFunctor g, f :<: g) => (v :-> Cxt h g a) -> Cxt h' f v :-> Cxt h g a Source #

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.