module Data.Type.Product.Lifted where
import Data.Type.Index
import Type.Class.Known
import Type.Class.Witness
import Type.Family.Constraint
import Type.Family.List
import Data.Monoid ((<>))
data FProd (fs :: [k -> *]) :: k -> * where
ØF :: FProd Ø a
(:<<) :: !(f a) -> !(FProd fs a) -> FProd (f :< fs) a
infixr 5 :<<
pattern (:>>) :: (f :: k -> *) (a :: k) -> (g :: k -> *) a -> FProd '[f,g] a
pattern a :>> b = a :<< b :<< ØF
infix 6 :>>
onlyF :: f a -> FProd '[f] a
onlyF = (:<< ØF)
(>>:) :: FProd fs a -> f a -> FProd (fs >: f) a
(>>:) = \case
ØF -> onlyF
b :<< as -> (b :<<) . (as >>:)
infixl 6 >>:
headF :: FProd (f :< fs) a -> f a
headF (a :<< _) = a
tailF :: FProd (f :< fs) a -> FProd fs a
tailF (_ :<< as) = as
initF :: FProd (f :< fs) a -> FProd (Init' f fs) a
initF (a :<< as) = case as of
ØF -> ØF
(:<<){} -> a :<< initF as
lastF :: FProd (f :< fs) a -> Last' f fs a
lastF (a :<< as) = case as of
ØF -> a
(:<<){} -> lastF as
reverseF :: FProd fs a -> FProd (Reverse fs) a
reverseF = \case
ØF -> ØF
a :<< as -> reverseF as >>: a
appendF :: FProd fs a -> FProd gs a -> FProd (fs ++ gs) a
appendF = \case
ØF -> id
a :<< as -> (a :<<) . appendF as
onHeadF :: (f a -> g a) -> FProd (f :< fs) a -> FProd (g :< fs) a
onHeadF f (a :<< as) = f a :<< as
onTailF :: (FProd fs a -> FProd gs a) -> FProd (f :< fs) a -> FProd (f :< gs) a
onTailF f (a :<< as) = a :<< f as
uncurryF :: (f a -> FProd fs a -> r) -> FProd (f :< fs) a -> r
uncurryF f (a :<< as) = f a as
curryF :: (l ~ (f :< fs)) => (FProd l a -> r) -> f a -> FProd fs a -> r
curryF f a as = f $ a :<< as
indexF :: Index fs f -> FProd fs a -> f a
indexF = \case
IZ -> headF
IS x -> indexF x . tailF
instance ListC (Functor <$> fs) => Functor (FProd fs) where
fmap f = \case
ØF -> ØF
a :<< as -> fmap f a :<< fmap f as
instance ListC (Foldable <$> fs) => Foldable (FProd fs) where
foldMap f = \case
ØF -> mempty
a :<< as -> foldMap f a <> foldMap f as
instance
( ListC (Functor <$> fs)
, ListC (Foldable <$> fs)
, ListC (Traversable <$> fs)
) => Traversable (FProd fs) where
traverse f = \case
ØF -> pure ØF
a :<< as -> (:<<) <$> traverse f a <*> traverse f as
imapF :: (forall f. Index fs f -> f a -> f b)
-> FProd fs a -> FProd fs b
imapF f = \case
ØF -> ØF
a :<< as -> f IZ a :<< imapF (f . IS) as
ifoldMapF :: Monoid m
=> (forall f. Index fs f -> f a -> m)
-> FProd fs a -> m
ifoldMapF f = \case
ØF -> mempty
a :<< as -> f IZ a <> ifoldMapF (f . IS) as
itraverseF :: Applicative g
=> (forall f. Index fs f -> f a -> g (f b))
-> FProd fs a -> g (FProd fs b)
itraverseF f = \case
ØF -> pure ØF
a :<< as -> (:<<) <$> f IZ a <*> itraverseF (f . IS) as
instance Known (FProd Ø) a where
known = ØF
instance (Known f a, Known (FProd fs) a) => Known (FProd (f :< fs)) a where
type KnownC (FProd (f :< fs)) a = (Known f a, Known (FProd fs) a)
known = known :<< known
instance Witness ØC ØC (FProd Ø a) where
r \\ _ = r
instance (Witness p q (f a), Witness s t (FProd fs a)) => Witness (p,s) (q,t) (FProd (f :< fs) a) where
type WitnessC (p,s) (q,t) (FProd (f :< fs) a) = (Witness p q (f a), Witness s t (FProd fs a))
r \\ (a :<< as) = r \\ a \\ as