{-# LANGUAGE PolyKinds    #-}
{-# LANGUAGE TypeFamilies #-}
module Barbies.Generics.Distributive
  ( GDistributive(..)
  )

where

import Data.Generics.GenericN
import Data.Proxy (Proxy (..))

import Data.Functor.Compose   (Compose (..))
import Data.Distributive      (Distributive(..))

import GHC.TypeLits (Nat)

class (Functor f) => GDistributive (n :: Nat) f repbg repbfg where
  gdistribute :: Proxy n -> f (repbg x) -> repbfg x

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

instance
  ( GDistributive n f bg bfg
  ) => GDistributive n f (M1 i c bg) (M1 i c bfg)
  where
  gdistribute :: forall (x :: k). Proxy n -> f (M1 i c bg x) -> M1 i c bfg x
gdistribute Proxy n
pn = forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (n :: Nat) (f :: * -> *) (repbg :: k -> *)
       (repbfg :: k -> *) (x :: k).
GDistributive n f repbg repbfg =>
Proxy n -> f (repbg x) -> repbfg x
gdistribute Proxy n
pn forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall k i (c :: Meta) (f :: k -> *) (p :: k). M1 i c f p -> f p
unM1
  {-# INLINE gdistribute #-}


instance
  ( Functor f
  ) => GDistributive n f U1 U1
  where
  gdistribute :: forall (x :: k). Proxy n -> f (U1 x) -> U1 x
gdistribute Proxy n
_ = forall a b. a -> b -> a
const forall k (p :: k). U1 p
U1
  {-# INLINE gdistribute #-}


fstF :: (l :*: r) a -> l a
fstF :: forall {k} (l :: k -> *) (r :: k -> *) (a :: k). (:*:) l r a -> l a
fstF (l a
x :*: r a
_y) = l a
x

sndF :: (l :*: r) a -> r a
sndF :: forall {k} (l :: k -> *) (r :: k -> *) (a :: k). (:*:) l r a -> r a
sndF (l a
_x :*: r a
y) = r a
y

instance
  ( GDistributive n f l l'
  , GDistributive n f r r'
  )
  => GDistributive n f (l :*: r) (l' :*: r')
  where
  gdistribute :: forall (x :: k). Proxy n -> f ((:*:) l r x) -> (:*:) l' r' x
gdistribute Proxy n
pn f ((:*:) l r x)
lr = forall {k} (n :: Nat) (f :: * -> *) (repbg :: k -> *)
       (repbfg :: k -> *) (x :: k).
GDistributive n f repbg repbfg =>
Proxy n -> f (repbg x) -> repbfg x
gdistribute Proxy n
pn (forall {k} (l :: k -> *) (r :: k -> *) (a :: k). (:*:) l r a -> l a
fstF forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f ((:*:) l r x)
lr) forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: forall {k} (n :: Nat) (f :: * -> *) (repbg :: k -> *)
       (repbfg :: k -> *) (x :: k).
GDistributive n f repbg repbfg =>
Proxy n -> f (repbg x) -> repbfg x
gdistribute Proxy n
pn (forall {k} (l :: k -> *) (r :: k -> *) (a :: k). (:*:) l r a -> r a
sndF forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f ((:*:) l r x)
lr)
  {-# INLINE gdistribute #-}


-- ---------------------------------------------------------
-- The interesting cases.
-- There are more interesting cases for specific values of n
-- ---------------------------------------------------------

type P = Param

instance
  ( Functor f
  ) =>
  GDistributive n f (Rec (P n g a) (g a)) (Rec (P n (Compose f g) a) (Compose f g a))
  where
  gdistribute :: forall (x :: k).
Proxy n
-> f (Rec (P n g a) (g a) x)
-> Rec (P n (Compose f g) a) (Compose f g a) x
gdistribute Proxy n
_ = forall {k} p a (x :: k). K1 R a x -> Rec p a x
Rec forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k i c (p :: k). c -> K1 i c p
K1 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} {k1} (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. a -> a
id forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall k i c (p :: k). K1 i c p -> c
unK1 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} p a (x :: k). Rec p a x -> K1 R a x
unRec)
  {-# INLINE gdistribute #-}

instance
  ( Functor f
  , Distributive h
  ) =>
  GDistributive n f (Rec (h (P n g a)) (h (g a))) (Rec (h (P n (Compose f g) a)) (h (Compose f g a)))
  where
  gdistribute :: forall (x :: k).
Proxy n
-> f (Rec (h (P n g a)) (h (g a)) x)
-> Rec (h (P n (Compose f g) a)) (h (Compose f g a)) x
gdistribute Proxy n
_ = forall {k} p a (x :: k). K1 R a x -> Rec p a x
Rec forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k i c (p :: k). c -> K1 i c p
K1 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall {k} {k1} (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (g :: * -> *) (f :: * -> *) a.
(Distributive g, Functor f) =>
f (g a) -> g (f a)
distribute forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall k i c (p :: k). K1 i c p -> c
unK1 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} p a (x :: k). Rec p a x -> K1 R a x
unRec)
  {-# INLINE gdistribute #-}