Copyright | Copyright (C) 2015 Kyle Carter |
---|---|
License | BSD3 |
Maintainer | Kyle Carter <kylcarte@indiana.edu> |
Stability | experimental |
Portability | RankNTypes |
Safe Haskell | None |
Language | Haskell2010 |
Sum
is a type combinators for representing disjoint sums of
indices (as :: [k])
of a single functor @(f :: k -> *).
Contrast to the many-functors-one-index FSum
- data Sum f :: [k] -> * where
- nilSum :: Sum f Ø -> Void
- decomp :: Sum f (a :< as) -> Either (f a) (Sum f as)
- injectSum :: Index as a -> f a -> Sum f as
- inj :: a ∈ as => f a -> Sum f as
- prj :: a ∈ as => Sum f as -> Maybe (f a)
- index :: Index as a -> Sum f as -> Maybe (f a)
- elimSum :: (forall x xs. f x -> p (x :< xs)) -> (forall x xs. Index as x -> p xs -> p (x :< xs)) -> Sum f as -> p as
Documentation
data Sum f :: [k] -> * where Source #
(Witness p q (f a1), Witness p q (Sum a f ((:<) a b as))) => Witness p q (Sum a f ((:<) a a1 ((:<) a b as))) Source # | |
Witness p q (f a) => Witness p q (Sum k f ((:) k a ([] k))) Source # | |
IxTraversable1 k [k] (Index k) (Sum k) Source # | |
IxFoldable1 k [k] (Index k) (Sum k) Source # | |
IxFunctor1 k [k] (Index k) (Sum k) Source # | |
Traversable1 [k] k (Sum k) Source # | |
Foldable1 [k] k (Sum k) Source # | |
Functor1 [k] k (Sum k) Source # | |
Read1 k f => Read1 [k] (Sum k f) Source # | |
Show1 k f => Show1 [k] (Sum k f) Source # | |
Ord1 k f => Ord1 [k] (Sum k f) Source # | |
Eq1 k f => Eq1 [k] (Sum k f) Source # | |
ListC ((<$>) Constraint * Eq ((<$>) * k f as)) => Eq (Sum k f as) Source # | |
(ListC ((<$>) Constraint * Eq ((<$>) * k f as)), ListC ((<$>) Constraint * Ord ((<$>) * k f as))) => Ord (Sum k f as) Source # | |
ListC ((<$>) Constraint * Show ((<$>) * k f as)) => Show (Sum k f as) Source # | |
type WitnessC p q (Sum a f ((:<) a a1 ((:<) a b as))) Source # | |
type WitnessC p q (Sum k f ((:) k a ([] k))) Source # | |