| 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 |
Data.Comp.Multi.Sum
Description
This module defines sums on signatures. All definitions are generalised versions of those in Data.Comp.Sum.
Synopsis
- class (f :: (* -> *) -> * -> *) :<: (g :: (* -> *) -> * -> *)
- class f :<: Sum fs => f :-<: fs
- data Sum (fs :: [(* -> *) -> * -> *]) h e
- proj :: (:<:) 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 :: (:<:) 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 :=: Sum fs => (forall e l. Alts fs (HFix f) e (a l)) -> HFix 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
- type family IsSum (f :: (* -> *) -> * -> *) :: Bool where ...
- type NotSum f = IsSum f ~ False
- isNode :: forall f g h a l. f :<: g => Proxy f -> Cxt h g a l -> Bool
Documentation
class (f :: (* -> *) -> * -> *) :<: (g :: (* -> *) -> * -> *) infixl 5 Source #
data Sum (fs :: [(* -> *) -> * -> *]) h e Source #
Data type defining a sum of signatures.
It is inspired by modular reifiable matching, as described in
- Oliveira, Bruno C. D. S., Shin-Cheng Mu, and Shu-Hung You. "Modular reifiable matching: a list-of-functors approach to two-level types." In Haskell Symposium, 2015.
except that this definition uses value-level integers (in the Elem datatype) in place
of type-level naturals. It hence uses unsafeCoerce under the hood, but is type-safe if used
through the public API. The result is that values of this type take constant memory with respect to the number
of summands (unlike vanilla datatypes à la carte), and constant time to dereference
(unlike modular reifiable matching). The representation is the bare minimum: an int representing the alternative,
and pointer to the value.
Instances
| Mem f fs => f :<: (Sum fs) Source # | |
| All (HasVars v) fs => HasVars v (Sum fs) Source # | |
| All HFunctor fs => HFunctor (Sum fs) Source # | |
| (All HFoldable fs, All HFunctor fs) => HFoldable (Sum fs) Source # | |
Defined in Data.Comp.Multi.Ops Methods hfold :: Monoid m => Sum fs (K m) :=> m Source # hfoldMap :: forall m (a :: Type -> Type). Monoid m => (a :=> m) -> Sum fs a :=> m Source # hfoldr :: forall (a :: Type -> Type) b. (a :=> (b -> b)) -> b -> Sum fs a :=> b Source # hfoldl :: forall b (a :: Type -> Type). (b -> a :=> b) -> b -> Sum fs a :=> b Source # | |
| (All HTraversable fs, All HFoldable fs, All HFunctor fs) => HTraversable (Sum fs) Source # | |
Defined in Data.Comp.Multi.Ops | |
| All EqHF fs => EqHF (Sum fs) Source # |
|
| (All OrdHF fs, EqHF (Sum fs)) => OrdHF (Sum fs) Source # |
|
| All ShowHF fs => ShowHF (Sum fs) Source # | |
| (RemA f g, RemA (Sum fs) (Sum gs)) => RemA (Sum (f ': fs)) (Sum (g ': gs)) Source # | |
| (Generic (f e l), Generic (Sum fs e l)) => Generic (Sum (f ': fs) e l) Source # | |
| Generic (Sum ('[] :: [(Type -> Type) -> Type -> Type]) e l) Source # | |
| type Rep (Sum (f ': fs) e l) Source # | |
| type Rep (Sum ('[] :: [(Type -> Type) -> Type -> Type]) e l) Source # | |
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 projectn 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
deepProjectn 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 injectn 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 deepInjectn
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.
liftCxt :: (HFunctor f, g :<: f) => g a :-> Context f a Source #
This function lifts the given functor to a context.
substHoles :: (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.