{-# 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 :: 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)
    = repfg x -> M1 i c repfg x
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 (Proxy n -> Proxy f -> Proxy g -> repf x -> repg x -> repfg 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 =>
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 :: 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
    = repf x -> M1 i c repf x
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 (Proxy n
-> Proxy f
-> Proxy repf
-> Proxy repfg
-> (forall (a :: k). f a)
-> repf 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 (Proxy repf
forall k (t :: k). Proxy t
Proxy @repf) (Proxy repfg
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 :: 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 = U1 x
forall k (p :: k). U1 p
U1
  {-# INLINE gprod #-}

  gpure :: 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
_ = U1 x
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 :: 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) lfg x -> rfg x -> (:*:) lfg rfg x
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 = Proxy n -> Proxy f -> Proxy g -> lf x -> lg x -> lfg 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 =>
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 = Proxy n -> Proxy f -> Proxy g -> rf x -> rg x -> rfg 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 =>
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 :: 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
    =   Proxy n
-> Proxy f
-> Proxy lf
-> Proxy lfg
-> (forall (a :: k). f a)
-> lf 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 (Proxy lf
forall k (t :: k). Proxy t
Proxy @lf) (Proxy lfg
forall k (t :: k). Proxy t
Proxy @lfg) forall (a :: k). f a
x
    lf x -> rf x -> (:*:) lf rf x
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: Proxy n
-> Proxy f
-> Proxy rf
-> Proxy rfg
-> (forall (a :: k). f a)
-> rf 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 (Proxy rf
forall k (t :: k). Proxy t
Proxy @rf) (Proxy rfg
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 :: 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
    = K1 R (f a) x -> Rec (P n f a) (f a) x
forall k p a (x :: k). K1 R a x -> Rec p a x
Rec (f a -> K1 R (f a) x
forall k i c (p :: k). c -> K1 i c p
K1 f a
forall (a :: k). f a
x)
  {-# INLINE gpure #-}

  gprod :: 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))
    = K1 R (Product f g a) x
-> Rec (P n (Product f g) a) (Product f g a) x
forall k p a (x :: k). K1 R a x -> Rec p a x
Rec (Product f g a -> K1 R (Product f g a) x
forall k i c (p :: k). c -> K1 i c p
K1 (f a -> g a -> Product f g a
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 :: 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
    = K1 R (h (f a)) x -> Rec (h (P n f a)) (h (f a)) x
forall k p a (x :: k). K1 R a x -> Rec p a x
Rec (h (f a) -> K1 R (h (f a)) x
forall k i c (p :: k). c -> K1 i c p
K1 (h (f a) -> K1 R (h (f a)) x) -> h (f a) -> K1 R (h (f a)) x
forall a b. (a -> b) -> a -> b
$ f a -> h (f a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure f a
forall (a :: k). f a
x)
  {-# INLINE gpure #-}

  gprod :: 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))
    = K1 R (h (Product f g a)) x
-> Rec (h (P n (Product f g) a)) (h (Product f g a)) x
forall k p a (x :: k). K1 R a x -> Rec p a x
Rec (h (Product f g a) -> K1 R (h (Product f g a)) x
forall k i c (p :: k). c -> K1 i c p
K1 (f a -> g a -> Product f g a
forall k (f :: k -> *) (g :: k -> *) (a :: k).
f a -> g a -> Product f g a
Pair (f a -> g a -> Product f g a)
-> h (f a) -> h (g a -> Product f g a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> h (f a)
fa h (g a -> Product f g a) -> h (g a) -> h (Product f g a)
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 :: 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
_
    = K1 R x x -> Rec x x x
forall k p a (x :: k). K1 R a x -> Rec p a x
Rec (x -> K1 R x x
forall k i c (p :: k). c -> K1 i c p
K1 x
forall a. Monoid a => a
mempty)
  {-# INLINE gpure #-}

  gprod :: 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))
    = K1 R x x -> Rec x x x
forall k p a (x :: k). K1 R a x -> Rec p a x
Rec (x -> K1 R x x
forall k i c (p :: k). c -> K1 i c p
K1 (x
l x -> x -> x
forall a. Semigroup a => a -> a -> a
<> x
r))
  {-# INLINE gprod #-}
-- }} Not a functor application -----------------------------------------------