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)))

HTraversable k [k] (Sum k)

HFoldable k [k] (Sum k)

HFunctor k [k] (Sum k)

HIxTraversable [k] k (Index k) (Sum k)

HIxFoldable [k] k (Index k) (Sum k)

HIxFunctor [k] k (Index k) (Sum k)

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)