{-# LANGUAGE PolyKinds            #-}
{-# LANGUAGE TypeFamilies         #-}
module Barbies.Generics.Applicative
  ( GApplicative(..)
  )

where


import Data.Functor.Product(Product(..))
import Data.Kind(Type)
import Data.Proxy(Proxy (..))

import Data.Generics.GenericN


class GApplicative n (f :: k -> Type) (g :: k -> Type) repbf repbg repbfg where
  gprod
    :: Proxy n
    -> Proxy f
    -> Proxy g
    -> repbf x
    -> repbg x
    -> repbfg x

  gpure
    :: (f ~ g, repbf ~ repbg)
    => Proxy n
    -> Proxy f
    -> Proxy repbf
    -> Proxy repbfg
    -> (forall a . f a)
    -> repbf x

-- ----------------------------------
-- Trivial cases
-- ----------------------------------

instance
  ( GApplicative n f g repf repg repfg
  ) => GApplicative n f g (M1 i c repf)
                          (M1 i c repg)
                          (M1 i c repfg)
  where
  gprod :: forall (x :: k).
Proxy n
-> Proxy f
-> Proxy g
-> M1 i c repf x
-> M1 i c repg x
-> M1 i c repfg x
gprod Proxy n
pn Proxy f
pf Proxy g
pg (M1 repf x
l) (M1 repg x
r)
    = forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 (forall {k} {k} k (n :: k) (f :: k -> *) (g :: k -> *)
       (repbf :: k -> *) (repbg :: k -> *) (repbfg :: k -> *) (x :: k).
GApplicative n f g repbf repbg repbfg =>
Proxy n -> Proxy f -> Proxy g -> repbf x -> repbg x -> repbfg x
gprod Proxy n
pn Proxy f
pf Proxy g
pg repf x
l repg x
r)
  {-# INLINE gprod #-}

  gpure :: forall (x :: k).
(f ~ g, M1 i c repf ~ M1 i c repg) =>
Proxy n
-> Proxy f
-> Proxy (M1 i c repf)
-> Proxy (M1 i c repfg)
-> (forall (a :: k). f a)
-> M1 i c repf x
gpure Proxy n
pn Proxy f
pf Proxy (M1 i c repf)
_ Proxy (M1 i c repfg)
_ forall (a :: k). f a
x
    = forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 (forall {k} {k} k (n :: k) (f :: k -> *) (g :: k -> *)
       (repbf :: k -> *) (repbg :: k -> *) (repbfg :: k -> *) (x :: k).
(GApplicative n f g repbf repbg repbfg, f ~ g, repbf ~ repbg) =>
Proxy n
-> Proxy f
-> Proxy repbf
-> Proxy repbfg
-> (forall (a :: k). f a)
-> repbf x
gpure Proxy n
pn Proxy f
pf (forall {k} (t :: k). Proxy t
Proxy @repf) (forall {k} (t :: k). Proxy t
Proxy @repfg) forall (a :: k). f a
x)
  {-# INLINE gpure #-}


instance GApplicative n f g U1 U1 U1 where
  gprod :: forall (x :: k).
Proxy n -> Proxy f -> Proxy g -> U1 x -> U1 x -> U1 x
gprod Proxy n
_ Proxy f
_ Proxy g
_ U1 x
U1 U1 x
U1 = forall k (p :: k). U1 p
U1
  {-# INLINE gprod #-}

  gpure :: forall (x :: k).
(f ~ g, U1 ~ U1) =>
Proxy n
-> Proxy f
-> Proxy U1
-> Proxy U1
-> (forall (a :: k). f a)
-> U1 x
gpure Proxy n
_ Proxy f
_ Proxy U1
_ Proxy U1
_ forall (a :: k). f a
_ = forall k (p :: k). U1 p
U1
  {-# INLINE gpure #-}


instance
  ( GApplicative n f g lf lg lfg
  , GApplicative n f g rf rg rfg
  ) => GApplicative n f g (lf  :*: rf)
                          (lg  :*: rg)
                          (lfg :*: rfg) where
  gprod :: forall (x :: k).
Proxy n
-> Proxy f
-> Proxy g
-> (:*:) lf rf x
-> (:*:) lg rg x
-> (:*:) lfg rfg x
gprod Proxy n
pn Proxy f
pf Proxy g
pg (lf x
l1 :*: rf x
l2) (lg x
r1 :*: rg x
r2)
    = (lf x
l1 lf x -> lg x -> lfg x
`lprod` lg x
r1) forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: (rf x
l2 rf x -> rg x -> rfg x
`rprod` rg x
r2)
    where
      lprod :: lf x -> lg x -> lfg x
lprod = forall {k} {k} k (n :: k) (f :: k -> *) (g :: k -> *)
       (repbf :: k -> *) (repbg :: k -> *) (repbfg :: k -> *) (x :: k).
GApplicative n f g repbf repbg repbfg =>
Proxy n -> Proxy f -> Proxy g -> repbf x -> repbg x -> repbfg x
gprod Proxy n
pn Proxy f
pf Proxy g
pg
      rprod :: rf x -> rg x -> rfg x
rprod = forall {k} {k} k (n :: k) (f :: k -> *) (g :: k -> *)
       (repbf :: k -> *) (repbg :: k -> *) (repbfg :: k -> *) (x :: k).
GApplicative n f g repbf repbg repbfg =>
Proxy n -> Proxy f -> Proxy g -> repbf x -> repbg x -> repbfg x
gprod Proxy n
pn Proxy f
pf Proxy g
pg
  {-# INLINE gprod #-}

  gpure :: forall (x :: k).
(f ~ g, (lf :*: rf) ~ (lg :*: rg)) =>
Proxy n
-> Proxy f
-> Proxy (lf :*: rf)
-> Proxy (lfg :*: rfg)
-> (forall (a :: k). f a)
-> (:*:) lf rf x
gpure Proxy n
pn Proxy f
pf Proxy (lf :*: rf)
_ Proxy (lfg :*: rfg)
_ forall (a :: k). f a
x
    =   forall {k} {k} k (n :: k) (f :: k -> *) (g :: k -> *)
       (repbf :: k -> *) (repbg :: k -> *) (repbfg :: k -> *) (x :: k).
(GApplicative n f g repbf repbg repbfg, f ~ g, repbf ~ repbg) =>
Proxy n
-> Proxy f
-> Proxy repbf
-> Proxy repbfg
-> (forall (a :: k). f a)
-> repbf x
gpure Proxy n
pn Proxy f
pf (forall {k} (t :: k). Proxy t
Proxy @lf) (forall {k} (t :: k). Proxy t
Proxy @lfg) forall (a :: k). f a
x
    forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: forall {k} {k} k (n :: k) (f :: k -> *) (g :: k -> *)
       (repbf :: k -> *) (repbg :: k -> *) (repbfg :: k -> *) (x :: k).
(GApplicative n f g repbf repbg repbfg, f ~ g, repbf ~ repbg) =>
Proxy n
-> Proxy f
-> Proxy repbf
-> Proxy repbfg
-> (forall (a :: k). f a)
-> repbf x
gpure Proxy n
pn Proxy f
pf (forall {k} (t :: k). Proxy t
Proxy @rf) (forall {k} (t :: k). Proxy t
Proxy @rfg) forall (a :: k). f a
x
  {-# INLINE gpure #-}


-- --------------------------------
-- The interesting cases
-- --------------------------------

type P = Param

-- {{ Functor application -----------------------------------------------------
instance
  GApplicative n f g (Rec (P n f a) (f a))
                     (Rec (P n g a) (g a))
                     (Rec (P n (f `Product` g) a) ((f `Product` g) a))
  where
  gpure :: forall (x :: k).
(f ~ g, Rec (P n f a) (f a) ~ Rec (P n g a) (g a)) =>
Proxy n
-> Proxy f
-> Proxy (Rec (P n f a) (f a))
-> Proxy (Rec (P n (Product f g) a) (Product f g a))
-> (forall (a :: k). f a)
-> Rec (P n f a) (f a) x
gpure Proxy n
_ Proxy f
_ Proxy (Rec (P n f a) (f a))
_ Proxy (Rec (P n (Product f g) a) (Product f g a))
_ forall (a :: k). f a
x
    = forall {k} p a (x :: k). K1 R a x -> Rec p a x
Rec (forall k i c (p :: k). c -> K1 i c p
K1 forall (a :: k). f a
x)
  {-# INLINE gpure #-}

  gprod :: forall (x :: k).
Proxy n
-> Proxy f
-> Proxy g
-> Rec (P n f a) (f a) x
-> Rec (P n g a) (g a) x
-> Rec (P n (Product f g) a) (Product f g a) x
gprod Proxy n
_ Proxy f
_ Proxy g
_ (Rec (K1 f a
fa)) (Rec (K1 g a
ga))
    = forall {k} p a (x :: k). K1 R a x -> Rec p a x
Rec (forall k i c (p :: k). c -> K1 i c p
K1 (forall {k} (f :: k -> *) (g :: k -> *) (a :: k).
f a -> g a -> Product f g a
Pair f a
fa g a
ga))
  {-# INLINE gprod #-}


instance
  ( Applicative h
  ) =>
  GApplicative n f g (Rec (h (P n f a)) (h (f a)))
                     (Rec (h (P n g a)) (h (g a)))
                     (Rec (h (P n (f `Product` g) a)) (h ((f `Product` g) a)))
  where
  gpure :: forall (x :: k).
(f ~ g,
 Rec (h (P n f a)) (h (f a)) ~ Rec (h (P n g a)) (h (g a))) =>
Proxy n
-> Proxy f
-> Proxy (Rec (h (P n f a)) (h (f a)))
-> Proxy (Rec (h (P n (Product f g) a)) (h (Product f g a)))
-> (forall (a :: k). f a)
-> Rec (h (P n f a)) (h (f a)) x
gpure Proxy n
_ Proxy f
_ Proxy (Rec (h (P n f a)) (h (f a)))
_ Proxy (Rec (h (P n (Product f g) a)) (h (Product f g a)))
_ forall (a :: k). f a
x
    = forall {k} p a (x :: k). K1 R a x -> Rec p a x
Rec (forall k i c (p :: k). c -> K1 i c p
K1 forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a. Applicative f => a -> f a
pure forall (a :: k). f a
x)
  {-# INLINE gpure #-}

  gprod :: forall (x :: k).
Proxy n
-> Proxy f
-> Proxy g
-> Rec (h (P n f a)) (h (f a)) x
-> Rec (h (P n g a)) (h (g a)) x
-> Rec (h (P n (Product f g) a)) (h (Product f g a)) x
gprod Proxy n
_ Proxy f
_ Proxy g
_ (Rec (K1 h (f a)
fa)) (Rec (K1 h (g a)
ga))
    = forall {k} p a (x :: k). K1 R a x -> Rec p a x
Rec (forall k i c (p :: k). c -> K1 i c p
K1 (forall {k} (f :: k -> *) (g :: k -> *) (a :: k).
f a -> g a -> Product f g a
Pair forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> h (f a)
fa forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> h (g a)
ga))
  {-# INLINE gprod #-}
-- }} Functor application -----------------------------------------------------


-- {{ Not a functor application -----------------------------------------------
instance
  ( Monoid x
  ) => GApplicative n f g (Rec x x) (Rec x x) (Rec x x)
  where
  gpure :: forall (x :: k).
(f ~ g, Rec x x ~ Rec x x) =>
Proxy n
-> Proxy f
-> Proxy (Rec x x)
-> Proxy (Rec x x)
-> (forall (a :: k). f a)
-> Rec x x x
gpure Proxy n
_ Proxy f
_ Proxy (Rec x x)
_ Proxy (Rec x x)
_ forall (a :: k). f a
_
    = forall {k} p a (x :: k). K1 R a x -> Rec p a x
Rec (forall k i c (p :: k). c -> K1 i c p
K1 forall a. Monoid a => a
mempty)
  {-# INLINE gpure #-}

  gprod :: forall (x :: k).
Proxy n
-> Proxy f -> Proxy g -> Rec x x x -> Rec x x x -> Rec x x x
gprod Proxy n
_ Proxy f
_ Proxy g
_ (Rec (K1 x
l)) (Rec (K1 x
r))
    = forall {k} p a (x :: k). K1 R a x -> Rec p a x
Rec (forall k i c (p :: k). c -> K1 i c p
K1 (x
l forall a. Semigroup a => a -> a -> a
<> x
r))
  {-# INLINE gprod #-}
-- }} Not a functor application -----------------------------------------------