Data.Type.Sum

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

Documentation

data Sum f :: [k] -> * where

Constructors

InL :: !(f a) -> Sum f (a :< as)

InR :: !(Sum f as) -> Sum f (a :< as)

Instances

(Witness p q (f a), Witness p q (Sum k f ((:<) k b as))) => Witness p q (Sum k f ((:<) k a ((:<) k b as)))

Witness p q (f a) => Witness p q (Sum k f ((:) k a ([] k)))

Traversable1 k [k] (Sum k)

Foldable1 k [k] (Sum k)

Functor1 k [k] (Sum k)

IxTraversable1 [k] k (Index k) (Sum k)

IxFoldable1 [k] k (Index k) (Sum k)

IxFunctor1 [k] k (Index k) (Sum k)

Read1 k f => Read1 [k] (Sum k f)

Show1 k f => Show1 [k] (Sum k f)

Ord1 k f => Ord1 [k] (Sum k f)

Eq1 k f => Eq1 [k] (Sum k f)

ListC ((<$>) Constraint * Eq ((<$>) * k f as)) => Eq (Sum k f as)

(ListC ((<$>) Constraint * Eq ((<$>) * k f as)), ListC ((<$>) Constraint * Ord ((<$>) * k f as))) => Ord (Sum k f as)

ListC ((<$>) Constraint * Show ((<$>) * k f as)) => Show (Sum k f as)

type WitnessC p q (Sum k f ((:<) k a ((:<) k b as))) = (Witness p q (f a), Witness p q (Sum k f ((:<) k b as)))

type WitnessC p q (Sum k f ((:) k a ([] k))) = Witness p q (f a)

nilSum :: Sum f Ø -> Void

There are no possible values of the type Sum f Ø.

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