{-# LANGUAGE PolyKinds    #-}
{-# LANGUAGE TypeFamilies #-}
{-# OPTIONS_GHC -Wno-orphans #-}
module Barbies.Internal.ApplicativeB
  ( ApplicativeB(bpure, bprod)
  , bzip, bunzip, bzipWith, bzipWith3, bzipWith4

  , CanDeriveApplicativeB
  , gbprodDefault, gbpureDefault
  )

where

import Barbies.Generics.Applicative(GApplicative(..))
import Barbies.Internal.FunctorB (FunctorB (..))

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

import Data.Generics.GenericN

-- | A 'FunctorB' with application, providing operations to:
--
--     * embed an "empty" value ('bpure')
--
--     * align and combine values ('bprod')
--
--  It should satisfy the following laws:
--
--  [Naturality of 'bprod']
--
-- @
-- 'bmap' (\('Pair' a b) -> 'Pair' (f a) (g b)) (u `'bprod'` v) = 'bmap' f u `'bprod'` 'bmap' g v
-- @
--
--
--  [Left and right identity]
--
-- @
-- 'bmap' (\('Pair' _ b) -> b) ('bpure' e `'bprod'` v) = v
-- 'bmap' (\('Pair' a _) -> a) (u `'bprod'` 'bpure' e) = u
-- @
--
-- [Associativity]
--
-- @
-- 'bmap' (\('Pair' a ('Pair' b c)) -> 'Pair' ('Pair' a b) c) (u `'bprod'` (v `'bprod'` w)) = (u `'bprod'` v) `'bprod'` w
-- @
--
--  It is to 'FunctorB' in the same way as 'Applicative'
--  relates to 'Functor'. For a presentation of 'Applicative' as
--  a monoidal functor, see Section 7 of
--  <http://www.soi.city.ac.uk/~ross/papers/Applicative.html Applicative Programming with Effects>.
--
-- There is a default implementation of 'bprod' and 'bpure' based on 'Generic'.
-- Intuitively, it works on types where the value of `bpure` is uniquely defined.
-- This corresponds rougly to record types (in the presence of sums, there would
-- be several candidates for `bpure`), where every field is either a 'Monoid' or
-- covered by the argument @f@.
class FunctorB b => ApplicativeB (b :: (k -> Type) -> Type) where
  bpure
    :: (forall a . f a)
    -> b f

  bprod
    :: b f
    -> b g
    -> b (f `Product` g)

  default bpure
    :: CanDeriveApplicativeB b f f
    => (forall a . f a)
    -> b f
  bpure = forall {k} (b :: (k -> *) -> *) (f :: k -> *).
CanDeriveApplicativeB b f f =>
(forall (a :: k). f a) -> b f
gbpureDefault

  default bprod
    :: CanDeriveApplicativeB b f g
    => b f
    -> b
    g -> b (f `Product` g)
  bprod = forall {k} (b :: (k -> *) -> *) (f :: k -> *) (g :: k -> *).
CanDeriveApplicativeB b f g =>
b f -> b g -> b (Product f g)
gbprodDefault


-- | An alias of 'bprod', since this is like a 'zip'.
bzip
  :: ApplicativeB b
  => b f
  -> b g
  -> b (f `Product` g)
bzip :: forall {k} (b :: (k -> *) -> *) (f :: k -> *) (g :: k -> *).
ApplicativeB b =>
b f -> b g -> b (Product f g)
bzip = forall k (b :: (k -> *) -> *) (f :: k -> *) (g :: k -> *).
ApplicativeB b =>
b f -> b g -> b (Product f g)
bprod

-- | An equivalent of 'unzip'.
bunzip
  :: ApplicativeB b
  => b (f `Product` g)
  -> (b f, b g)
bunzip :: forall {k} (b :: (k -> *) -> *) (f :: k -> *) (g :: k -> *).
ApplicativeB b =>
b (Product f g) -> (b f, b g)
bunzip b (Product f g)
bfg
  = (forall k (b :: (k -> *) -> *) (f :: k -> *) (g :: k -> *).
FunctorB b =>
(forall (a :: k). f a -> g a) -> b f -> b g
bmap (\(Pair f a
a g a
_) -> f a
a) b (Product f g)
bfg, forall k (b :: (k -> *) -> *) (f :: k -> *) (g :: k -> *).
FunctorB b =>
(forall (a :: k). f a -> g a) -> b f -> b g
bmap (\(Pair f a
_ g a
b) -> g a
b) b (Product f g)
bfg)

-- | An equivalent of 'Data.List.zipWith'.
bzipWith
  :: ApplicativeB b
  => (forall a. f a -> g a -> h a)
  -> b f
  -> b g
  -> b h
bzipWith :: forall {k} (b :: (k -> *) -> *) (f :: k -> *) (g :: k -> *)
       (h :: k -> *).
ApplicativeB b =>
(forall (a :: k). f a -> g a -> h a) -> b f -> b g -> b h
bzipWith forall (a :: k). f a -> g a -> h a
f b f
bf b g
bg
  = forall k (b :: (k -> *) -> *) (f :: k -> *) (g :: k -> *).
FunctorB b =>
(forall (a :: k). f a -> g a) -> b f -> b g
bmap (\(Pair f a
fa g a
ga) -> forall (a :: k). f a -> g a -> h a
f f a
fa g a
ga) (b f
bf forall k (b :: (k -> *) -> *) (f :: k -> *) (g :: k -> *).
ApplicativeB b =>
b f -> b g -> b (Product f g)
`bprod` b g
bg)

-- | An equivalent of 'Data.List.zipWith3'.
bzipWith3
  :: ApplicativeB b
  => (forall a. f a -> g a -> h a -> i a)
  -> b f
  -> b g
  -> b h
  -> b i
bzipWith3 :: forall {k} (b :: (k -> *) -> *) (f :: k -> *) (g :: k -> *)
       (h :: k -> *) (i :: k -> *).
ApplicativeB b =>
(forall (a :: k). f a -> g a -> h a -> i a)
-> b f -> b g -> b h -> b i
bzipWith3 forall (a :: k). f a -> g a -> h a -> i a
f b f
bf b g
bg b h
bh
  = forall k (b :: (k -> *) -> *) (f :: k -> *) (g :: k -> *).
FunctorB b =>
(forall (a :: k). f a -> g a) -> b f -> b g
bmap (\(Pair (Pair f a
fa g a
ga) h a
ha) -> forall (a :: k). f a -> g a -> h a -> i a
f f a
fa g a
ga h a
ha)
         (b f
bf forall k (b :: (k -> *) -> *) (f :: k -> *) (g :: k -> *).
ApplicativeB b =>
b f -> b g -> b (Product f g)
`bprod` b g
bg forall k (b :: (k -> *) -> *) (f :: k -> *) (g :: k -> *).
ApplicativeB b =>
b f -> b g -> b (Product f g)
`bprod` b h
bh)


-- | An equivalent of 'Data.List.zipWith4'.
bzipWith4
  :: ApplicativeB b
  => (forall a. f a -> g a -> h a -> i a -> j a)
  -> b f
  -> b g
  -> b h
  -> b
  i -> b j
bzipWith4 :: forall {k} (b :: (k -> *) -> *) (f :: k -> *) (g :: k -> *)
       (h :: k -> *) (i :: k -> *) (j :: k -> *).
ApplicativeB b =>
(forall (a :: k). f a -> g a -> h a -> i a -> j a)
-> b f -> b g -> b h -> b i -> b j
bzipWith4 forall (a :: k). f a -> g a -> h a -> i a -> j a
f b f
bf b g
bg b h
bh b i
bi
  = forall k (b :: (k -> *) -> *) (f :: k -> *) (g :: k -> *).
FunctorB b =>
(forall (a :: k). f a -> g a) -> b f -> b g
bmap (\(Pair (Pair (Pair f a
fa g a
ga) h a
ha) i a
ia) -> forall (a :: k). f a -> g a -> h a -> i a -> j a
f f a
fa g a
ga h a
ha i a
ia)
         (b f
bf forall k (b :: (k -> *) -> *) (f :: k -> *) (g :: k -> *).
ApplicativeB b =>
b f -> b g -> b (Product f g)
`bprod` b g
bg forall k (b :: (k -> *) -> *) (f :: k -> *) (g :: k -> *).
ApplicativeB b =>
b f -> b g -> b (Product f g)
`bprod` b h
bh forall k (b :: (k -> *) -> *) (f :: k -> *) (g :: k -> *).
ApplicativeB b =>
b f -> b g -> b (Product f g)
`bprod` b i
bi)


-- | @'CanDeriveApplicativeB' B f g@ is in practice a predicate about @B@ only.
--   Intuitively, it says that the following holds, for any arbitrary @f@:
--
--     * There is an instance of @'Generic' (B f)@.
--
--     * @B@ has only one constructor (that is, it is not a sum-type).
--
--     * Every field of @B f@ is either a monoid, or of the form @f a@, for
--       some type @a@.
type CanDeriveApplicativeB b f g
  = ( GenericP 0 (b f)
    , GenericP 0 (b g)
    , GenericP 0 (b (f `Product` g))
    , GApplicative 0 f g (RepP 0 (b f)) (RepP 0 (b g)) (RepP 0 (b (f `Product` g)))
    )


-- ======================================
-- Generic derivation of instances
-- ======================================

-- | Default implementation of 'bprod' based on 'Generic'.
gbprodDefault
  :: forall b f g
  .  CanDeriveApplicativeB b f g
  => b f
  -> b g
  -> b (f `Product` g)
gbprodDefault :: forall {k} (b :: (k -> *) -> *) (f :: k -> *) (g :: k -> *).
CanDeriveApplicativeB b f g =>
b f -> b g -> b (Product f g)
gbprodDefault b f
l b g
r
  = forall (n :: Natural) a x.
GenericP n a =>
Proxy n -> RepP n a x -> a
toP Proxy 0
p0 forall a b. (a -> b) -> a -> b
$ 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 0
p0 (forall {k} (t :: k). Proxy t
Proxy @f) (forall {k} (t :: k). Proxy t
Proxy @g) (forall (n :: Natural) a x.
GenericP n a =>
Proxy n -> a -> RepP n a x
fromP Proxy 0
p0 b f
l) (forall (n :: Natural) a x.
GenericP n a =>
Proxy n -> a -> RepP n a x
fromP Proxy 0
p0 b g
r)
  where
    p0 :: Proxy 0
p0 = forall {k} (t :: k). Proxy t
Proxy @0
{-# INLINE gbprodDefault #-}

gbpureDefault
  :: forall b f
  .  CanDeriveApplicativeB b f f
  => (forall a . f a)
  -> b f
gbpureDefault :: forall {k} (b :: (k -> *) -> *) (f :: k -> *).
CanDeriveApplicativeB b f f =>
(forall (a :: k). f a) -> b f
gbpureDefault forall (a :: k). f a
fa
  = forall (n :: Natural) a x.
GenericP n a =>
Proxy n -> RepP n a x -> a
toP (forall {k} (t :: k). Proxy t
Proxy @0) forall a b. (a -> b) -> a -> b
$ 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
      (forall {k} (t :: k). Proxy t
Proxy @0)
      (forall {k} (t :: k). Proxy t
Proxy @f)
      (forall {k} (t :: k). Proxy t
Proxy @(RepP 0 (b f)))
      (forall {k} (t :: k). Proxy t
Proxy @(RepP 0 (b (f `Product` f))))
      forall (a :: k). f a
fa
{-# INLINE gbpureDefault #-}


-- ------------------------------------------------------------
-- Generic derivation: Special cases for ApplicativeB
-- -------------------------------------------------------------

type P = Param

instance
  (  ApplicativeB b
  ) => GApplicative 0 f g (Rec (b (P 0 f)) (b f))
                          (Rec (b (P 0 g)) (b g))
                          (Rec (b (P 0 (f `Product` g))) (b (f `Product` g)))
  where
  gpure :: forall (x :: k).
(f ~ g, Rec (b (P 0 f)) (b f) ~ Rec (b (P 0 g)) (b g)) =>
Proxy 0
-> Proxy f
-> Proxy (Rec (b (P 0 f)) (b f))
-> Proxy (Rec (b (P 0 (Product f g))) (b (Product f g)))
-> (forall (a :: k). f a)
-> Rec (b (P 0 f)) (b f) x
gpure Proxy 0
_ Proxy f
_ Proxy (Rec (b (P 0 f)) (b f))
_ Proxy (Rec (b (P 0 (Product f g))) (b (Product f g)))
_ forall (a :: k). f a
fa
    = 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 (b :: (k -> *) -> *) (f :: k -> *).
ApplicativeB b =>
(forall (a :: k). f a) -> b f
bpure forall (a :: k). f a
fa))
  {-# INLINE gpure #-}

  gprod :: forall (x :: k).
Proxy 0
-> Proxy f
-> Proxy g
-> Rec (b (P 0 f)) (b f) x
-> Rec (b (P 0 g)) (b g) x
-> Rec (b (P 0 (Product f g))) (b (Product f g)) x
gprod Proxy 0
_ Proxy f
_ Proxy g
_ (Rec (K1 b f
bf)) (Rec (K1 b g
bg))
    = 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 (b f
bf forall k (b :: (k -> *) -> *) (f :: k -> *) (g :: k -> *).
ApplicativeB b =>
b f -> b g -> b (Product f g)
`bprod` b g
bg))
  {-# INLINE gprod #-}



instance
  ( Applicative h
  , ApplicativeB b
  ) => GApplicative 0 f g (Rec (h (b (P 0 f))) (h (b f)))
                          (Rec (h (b (P 0 g))) (h (b g)))
                          (Rec (h (b (P 0 (f `Product` g)))) (h (b (f `Product` g))))
  where
  gpure :: forall (x :: k).
(f ~ g,
 Rec (h (b (P 0 f))) (h (b f)) ~ Rec (h (b (P 0 g))) (h (b g))) =>
Proxy 0
-> Proxy f
-> Proxy (Rec (h (b (P 0 f))) (h (b f)))
-> Proxy (Rec (h (b (P 0 (Product f g)))) (h (b (Product f g))))
-> (forall (a :: k). f a)
-> Rec (h (b (P 0 f))) (h (b f)) x
gpure Proxy 0
_ Proxy f
_ Proxy (Rec (h (b (P 0 f))) (h (b f)))
_ Proxy (Rec (h (b (P 0 (Product f g)))) (h (b (Product f g))))
_ forall (a :: k). f a
fa
    = 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 (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall k (b :: (k -> *) -> *) (f :: k -> *).
ApplicativeB b =>
(forall (a :: k). f a) -> b f
bpure forall (a :: k). f a
fa))
  {-# INLINE gpure #-}

  gprod :: forall (x :: k).
Proxy 0
-> Proxy f
-> Proxy g
-> Rec (h (b (P 0 f))) (h (b f)) x
-> Rec (h (b (P 0 g))) (h (b g)) x
-> Rec (h (b (P 0 (Product f g)))) (h (b (Product f g))) x
gprod Proxy 0
_ Proxy f
_ Proxy g
_ (Rec (K1 h (b f)
hbf)) (Rec (K1 h (b g)
hbg))
    = 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 (b :: (k -> *) -> *) (f :: k -> *) (g :: k -> *).
ApplicativeB b =>
b f -> b g -> b (Product f g)
bprod forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> h (b f)
hbf forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> h (b g)
hbg))
  {-# INLINE gprod #-}

-- This is the same as the previous instance, but for nested Applicatives.
instance
  ( Applicative h
  , Applicative m
  , ApplicativeB b
  ) => GApplicative 0 f g (Rec (m (h (b (P 0 f)))) (m (h (b f))))
                          (Rec (m (h (b (P 0 g)))) (m (h (b g))))
                          (Rec (m (h (b (P 0 (f `Product` g))))) (m (h (b (f `Product` g)))))
  where
  gpure :: forall (x :: k).
(f ~ g,
 Rec (m (h (b (P 0 f)))) (m (h (b f)))
 ~ Rec (m (h (b (P 0 g)))) (m (h (b g)))) =>
Proxy 0
-> Proxy f
-> Proxy (Rec (m (h (b (P 0 f)))) (m (h (b f))))
-> Proxy
     (Rec (m (h (b (P 0 (Product f g))))) (m (h (b (Product f g)))))
-> (forall (a :: k). f a)
-> Rec (m (h (b (P 0 f)))) (m (h (b f))) x
gpure Proxy 0
_ Proxy f
_ Proxy (Rec (m (h (b (P 0 f)))) (m (h (b f))))
_ Proxy
  (Rec (m (h (b (P 0 (Product f g))))) (m (h (b (Product f g)))))
_ 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 (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall k (b :: (k -> *) -> *) (f :: k -> *).
ApplicativeB b =>
(forall (a :: k). f a) -> b f
bpure forall (a :: k). f a
x))
  {-# INLINE gpure #-}

  gprod :: forall (x :: k).
Proxy 0
-> Proxy f
-> Proxy g
-> Rec (m (h (b (P 0 f)))) (m (h (b f))) x
-> Rec (m (h (b (P 0 g)))) (m (h (b g))) x
-> Rec (m (h (b (P 0 (Product f g))))) (m (h (b (Product f g)))) x
gprod Proxy 0
_ Proxy f
_ Proxy g
_ (Rec (K1 m (h (b f))
hbf)) (Rec (K1 m (h (b g))
hbg))
    = 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 :: * -> *} {b :: (k -> *) -> *} {f :: k -> *}
       {g :: k -> *}.
(Applicative f, ApplicativeB b) =>
f (b f) -> f (b g) -> f (b (Product f g))
go forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m (h (b f))
hbf forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> m (h (b g))
hbg))
    where
      go :: f (b f) -> f (b g) -> f (b (Product f g))
go f (b f)
a f (b g)
b = forall k (b :: (k -> *) -> *) (f :: k -> *) (g :: k -> *).
ApplicativeB b =>
b f -> b g -> b (Product f g)
bprod forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f (b f)
a forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> f (b g)
b
  {-# INLINE gprod #-}


-- --------------------------------
-- Instances for base types
-- --------------------------------

instance ApplicativeB Proxy where
  bpure :: forall (f :: k -> *). (forall (a :: k). f a) -> Proxy f
bpure forall (a :: k). f a
_ = forall {k} (t :: k). Proxy t
Proxy
  {-# INLINE bpure #-}

  bprod :: forall (f :: k -> *) (g :: k -> *).
Proxy f -> Proxy g -> Proxy (Product f g)
bprod Proxy f
_ Proxy g
_ = forall {k} (t :: k). Proxy t
Proxy
  {-# INLINE bprod #-}

instance Monoid a => ApplicativeB (Const a) where
  bpure :: forall (f :: k -> *). (forall (a :: k). f a) -> Const a f
bpure forall (a :: k). f a
_
    = forall {k} a (b :: k). a -> Const a b
Const forall a. Monoid a => a
mempty
  {-# INLINE bpure #-}

  bprod :: forall (f :: k -> *) (g :: k -> *).
Const a f -> Const a g -> Const a (Product f g)
bprod (Const a
l) (Const a
r)
    = forall {k} a (b :: k). a -> Const a b
Const (a
l forall a. Monoid a => a -> a -> a
`mappend` a
r)
  {-# INLINE bprod #-}

instance (ApplicativeB a, ApplicativeB b) => ApplicativeB (Product a b) where
  bpure :: forall (f :: k -> *). (forall (a :: k). f a) -> Product a b f
bpure forall (a :: k). f a
x
    = forall {k} (f :: k -> *) (g :: k -> *) (a :: k).
f a -> g a -> Product f g a
Pair (forall k (b :: (k -> *) -> *) (f :: k -> *).
ApplicativeB b =>
(forall (a :: k). f a) -> b f
bpure forall (a :: k). f a
x) (forall k (b :: (k -> *) -> *) (f :: k -> *).
ApplicativeB b =>
(forall (a :: k). f a) -> b f
bpure forall (a :: k). f a
x)
  {-# INLINE bpure #-}

  bprod :: forall (f :: k -> *) (g :: k -> *).
Product a b f -> Product a b g -> Product a b (Product f g)
bprod (Pair a f
ll b f
lr) (Pair a g
rl b g
rr)
    = forall {k} (f :: k -> *) (g :: k -> *) (a :: k).
f a -> g a -> Product f g a
Pair (forall k (b :: (k -> *) -> *) (f :: k -> *) (g :: k -> *).
ApplicativeB b =>
b f -> b g -> b (Product f g)
bprod a f
ll a g
rl) (forall k (b :: (k -> *) -> *) (f :: k -> *) (g :: k -> *).
ApplicativeB b =>
b f -> b g -> b (Product f g)
bprod b f
lr b g
rr)
  {-# INLINE bprod #-}


-- --------------------------------
-- Instances for base types
-- --------------------------------

instance Monoid a => ApplicativeB (Constant a) where
  bpure :: forall (f :: k -> *). (forall (a :: k). f a) -> Constant a f
bpure forall (a :: k). f a
_
    = forall {k} a (b :: k). a -> Constant a b
Constant forall a. Monoid a => a
mempty
  {-# INLINE bpure #-}

  bprod :: forall (f :: k -> *) (g :: k -> *).
Constant a f -> Constant a g -> Constant a (Product f g)
bprod (Constant a
l) (Constant a
r)
    = forall {k} a (b :: k). a -> Constant a b
Constant (a
l forall a. Monoid a => a -> a -> a
`mappend` a
r)
  {-# INLINE bprod #-}