Copyright | (c) 2011 Patrick Bahr |
---|---|
License | BSD3 |
Maintainer | Patrick Bahr <paba@diku.dk> |
Stability | experimental |
Portability | non-portable (GHC Extensions) |
Safe Haskell | None |
Language | Haskell98 |
This module defines sums on signatures. All definitions are generalised versions of those in Data.Comp.Sum.
- type (:<:) f g = Subsume (ComprEmb (Elem f g)) f g
- data (f :+: g) h e
- caseH :: (f a b -> c) -> (g a b -> c) -> (f :+: g) a b -> c
- proj :: forall f g a. f :<: g => NatM Maybe (g a) (f a)
- project :: g :<: f => NatM Maybe (Cxt h f a) (g (Cxt h f a))
- deepProject :: (HTraversable g, g :<: f) => CxtFunM Maybe f g
- inj :: forall f g a. f :<: g => f a :-> g a
- inject :: g :<: f => g (Cxt h f a) :-> Cxt h f a
- deepInject :: (HFunctor g, g :<: f) => CxtFun g f
- split :: f :=: (f1 :+: f2) => (f1 (Term f) :-> a) -> (f2 (Term f) :-> a) -> Term f :-> a
- injectConst :: (HFunctor g, g :<: f) => Const g :-> Cxt h f a
- projectConst :: (HFunctor g, g :<: f) => NatM Maybe (Cxt h f a) (Const g)
- injectCxt :: (HFunctor g, g :<: f) => Cxt h' g (Cxt h f a) :-> Cxt h f a
- liftCxt :: (HFunctor f, g :<: f) => g a :-> Context f a
- substHoles :: (HFunctor f, HFunctor g, f :<: g) => (v :-> Cxt h g a) -> Cxt h' f v :-> Cxt h g a
Documentation
type (:<:) f g = 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 :+: g) h e infixr 6 Source
Data type defining coproducts.
(HFunctor f, HFunctor g) => HFunctor ((:+:) * f g) | |
(HFoldable f, HFoldable g) => HFoldable ((:+:) * f g) | |
(HTraversable f, HTraversable g) => HTraversable ((:+:) * f g) | |
(ShowHF f, ShowHF g) => ShowHF ((:+:) * f g) | |
(EqHF f, EqHF g) => EqHF ((:+:) * f g) |
|
(OrdHF f, OrdHF g) => OrdHF ((:+:) * f g) |
|
(Desugar f h, Desugar g h) => Desugar ((:+:) * f g) h | |
(HasVars f v0, HasVars g v0) => HasVars ((:+:) * f g) v | |
DistAnn s p s' => DistAnn ((:+:) * f s) p ((:+:) * ((:&:) * f p) s') | |
RemA s s' => RemA ((:+:) * ((:&:) * f p) s) ((:+:) * f s') |
caseH :: (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
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. If the signature
g
is compound of n atomic signatures, use project
n instead.
deepProject :: (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
deepProject
n instead.
Injections for Signatures and Terms
inject :: 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 inject
n instead.
deepInject :: (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 deepInject
n
instead.
Injections and Projections for Constants
injectCxt :: (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.