Copyright	Copyright (C) 2015 Kyle Carter
License	BSD3
Maintainer	Kyle Carter <kylcarte@indiana.edu>
Stability	experimental
Portability	RankNTypes
Safe Haskell	None
Language	Haskell2010

Data.Type.Sum

Description

Sum and SumF are type combinators for representing disjoint sums of indices (as :: [k]) of a single functor (f :: k -> *), or of many functors(fs :: [k -> *]) at a single index (a :: k)@, respectively.

Documentation

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

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))) Source
Witness p q (f a) => Witness p q (Sum k f ((:) k a ([] k))) Source
HTraversable k [k] (Sum k) Source
HFoldable k [k] (Sum k) Source
HFunctor k [k] (Sum k) Source
HIxTraversable [k] k (Index k) (Sum k) Source
HIxFoldable [k] k (Index k) (Sum k) Source
HIxFunctor [k] k (Index k) (Sum k) Source
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))) Source
type WitnessC p q (Sum k f ((:) k a ([] k))) = Witness p q (f a) Source

decomp :: Sum f (a :< as) -> Either (f a) (Sum f as) Source

injectSum :: Index as a -> f a -> Sum f as Source

inj :: a ∈ as => f a -> Sum f as Source

prj :: a ∈ as => Sum f as -> Maybe (f a) Source

index :: Index as a -> Sum f as -> Maybe (f a) Source

data SumF :: [k -> *] -> k -> * where Source

Constructors

InLF :: !(f a) -> SumF (f :< fs) a
InRF :: !(SumF fs a) -> SumF (f :< fs) a

Instances

ListC ((<$>) Constraint (* -> *) Functor fs) => Functor (SumF * fs) Source

decompF :: SumF (f :< fs) a -> Either (f a) (SumF fs a) Source

injF :: f ∈ fs => f a -> SumF fs a Source

prjF :: f ∈ fs => SumF fs a -> Maybe (f a) Source

injectSumF :: Index fs f -> f a -> SumF fs a Source

indexF :: Index fs f -> SumF fs a -> Maybe (f a) Source