module Data.Type.Sum.Lifted where
import Data.Type.Index
import Type.Class.Witness
import Type.Family.List
data FSum :: [k -> *] -> k -> * where
FInL :: !(f a) -> FSum (f :< fs) a
FInR :: !(FSum fs a) -> FSum (f :< fs) a
nilFSum :: FSum Ø a -> Void
nilFSum = impossible
fdecomp :: FSum (f :< fs) a -> Either (f a) (FSum fs a)
fdecomp = \case
FInL a -> Left a
FInR s -> Right s
finj :: (f ∈ fs) => f a -> FSum fs a
finj = injectFSum elemIndex
fprj :: (f ∈ fs) => FSum fs a -> Maybe (f a)
fprj = findex elemIndex
injectFSum :: Index fs f -> f a -> FSum fs a
injectFSum = \case
IZ -> FInL
IS x -> FInR . injectFSum x
findex :: Index fs f -> FSum fs a -> Maybe (f a)
findex = \case
IZ -> \case
FInL a -> Just a
_ -> Nothing
IS x -> \case
FInR s -> findex x s
_ -> Nothing
instance ListC (Functor <$> fs) => Functor (FSum fs) where
fmap f = \case
FInL a -> FInL $ f <$> a
FInR s -> FInR $ f <$> s
instance ListC (Foldable <$> fs) => Foldable (FSum fs) where
foldMap f = \case
FInL a -> foldMap f a
FInR s -> foldMap f s
instance
( ListC (Functor <$> fs)
, ListC (Foldable <$> fs)
, ListC (Traversable <$> fs)
) => Traversable (FSum fs) where
traverse f = \case
FInL a -> FInL <$> traverse f a
FInR s -> FInR <$> traverse f s
imapFSum :: (forall f. Index fs f -> f a -> f b)
-> FSum fs a -> FSum fs b
imapFSum f = \case
FInL a -> FInL $ f IZ a
FInR s -> FInR $ imapFSum (f . IS) s
ifoldMapFSum :: (forall f. Index fs f -> f a -> m)
-> FSum fs a -> m
ifoldMapFSum f = \case
FInL a -> f IZ a
FInR s -> ifoldMapFSum (f . IS) s
itraverseFSum :: Functor g
=> (forall f. Index fs f -> f a -> g (f b))
-> FSum fs a -> g (FSum fs b)
itraverseFSum f = \case
FInL a -> FInL <$> f IZ a
FInR s -> FInR <$> itraverseFSum (f . IS) s