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 (Elem f g) f g, NoDupl f g (AnyDupl 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 (Elem f g) f g, NoDupl f g (AnyDupl f g)) infixl 5 Source
The :<: constraint is a conjunction of two constraints. The first
one is used to construct the evidence that is used to implement the
injection and projection functions. The first constraint alone
would allow instances such as F :+: F :<: F
or F :+: (F :+: G)
:<: F :+: G
which have multiple occurrences of the same
sub-signature on the left-hand side. Such instances are usually
unintended and yield injection functions that are not
injective. The second constraint excludes such instances.
data (f :+: g) h e infixr 6 Source
Data type defining coproducts.
Subsume (Found p) f g => Subsume (Found (Ri p)) f ((:+:) * g' g) | |
Subsume (Found p) f g => Subsume (Found (Le p)) f ((:+:) * g g') | |
(Subsume (Found p1) f1 g, Subsume (Found p2) f2 g) => Subsume (Found (Sum p1 p2)) ((:+:) * f1 f2) g | |
(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.