{-# LANGUAGE PolyKinds    #-}
{-# LANGUAGE TypeFamilies #-}
{-# OPTIONS_GHC -Wno-orphans #-}
module Barbies.Internal.FunctorB
  ( FunctorB(..)
  , gbmapDefault
  , CanDeriveFunctorB
  )

where

import Barbies.Generics.Functor (GFunctor(..))

import Data.Functor.Compose   (Compose (..))
import Data.Functor.Const     (Const (..))
import Data.Functor.Constant  (Constant (..))
import Data.Functor.Product   (Product (..))
import Data.Functor.Sum       (Sum (..))
import Data.Generics.GenericN
import Data.Proxy             (Proxy (..))
import Data.Kind              (Type)

-- | Barbie-types that can be mapped over. Instances of 'FunctorB' should
--   satisfy the following laws:
--
-- @
-- 'bmap' 'id' = 'id'
-- 'bmap' f . 'bmap' g = 'bmap' (f . g)
-- @
--
-- There is a default 'bmap' implementation for 'Generic' types, so
-- instances can derived automatically.
class FunctorB (b :: (k -> Type) -> Type) where
  bmap :: (forall a . f a -> g a) -> b f -> b g

  default bmap
    :: forall f g
    .  CanDeriveFunctorB b f g
    => (forall a . f a -> g a) -> b f -> b g
  bmap = forall {k} (b :: (k -> *) -> *) (f :: k -> *) (g :: k -> *).
CanDeriveFunctorB b f g =>
(forall (a :: k). f a -> g a) -> b f -> b g
gbmapDefault

-- | @'CanDeriveFunctorB' 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 f@ can contain fields of type @b f@ as long as there exists a
--       @'FunctorB' b@ instance. In particular, recursive usages of @B f@
--       are allowed.
--
--     * @B f@ can also contain usages of @b f@ under a @'Functor' h@.
--       For example, one could use @'Maybe' (B f)@ when defining @B f@.
type CanDeriveFunctorB b f g
  = ( GenericP 0 (b f)
    , GenericP 0 (b g)
    , GFunctor 0 f g (RepP 0 (b f)) (RepP 0 (b g))
    )

-- | Default implementation of 'bmap' based on 'Generic'.
gbmapDefault
  :: CanDeriveFunctorB b f g
  => (forall a . f a -> g a) -> b f -> b g
gbmapDefault :: forall {k} (b :: (k -> *) -> *) (f :: k -> *) (g :: k -> *).
CanDeriveFunctorB b f g =>
(forall (a :: k). f a -> g a) -> b f -> b g
gbmapDefault forall (a :: k). f a -> g a
f
  = forall (n :: Nat) a x. GenericP n a => Proxy n -> RepP n a x -> a
toP (forall {k} (t :: k). Proxy t
Proxy @0) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} {k} (n :: Nat) (f :: k -> *) (g :: k -> *)
       (repbf :: k -> *) (repbg :: k -> *) (x :: k).
GFunctor n f g repbf repbg =>
Proxy n -> (forall (a :: k). f a -> g a) -> repbf x -> repbg x
gmap (forall {k} (t :: k). Proxy t
Proxy @0) forall (a :: k). f a -> g a
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (n :: Nat) a x. GenericP n a => Proxy n -> a -> RepP n a x
fromP (forall {k} (t :: k). Proxy t
Proxy @0)
{-# INLINE gbmapDefault #-}

-- ------------------------------------------------------------
-- Generic derivation: Special cases for FunctorB
-- -----------------------------------------------------------

type P = Param

-- b' is b, maybe with 'Param' annotations
instance
  ( FunctorB b
  ) => GFunctor 0 f g (Rec (b' (P 0 f)) (b f))
                      (Rec (b' (P 0 g)) (b g))
  where
  gmap :: forall (x :: k).
Proxy 0
-> (forall (a :: k). f a -> g a)
-> Rec (b' (P 0 f)) (b f) x
-> Rec (b' (P 0 g)) (b g) x
gmap Proxy 0
_ forall (a :: k). f a -> g a
h (Rec (K1 b f
bf)) = 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 -> *).
FunctorB b =>
(forall (a :: k). f a -> g a) -> b f -> b g
bmap forall (a :: k). f a -> g a
h b f
bf))
  {-# INLINE gmap #-}

-- h' and b' are essentially  h and b, but maybe
-- with 'Param' annotations
instance
  ( Functor h
  , FunctorB b
  ) => GFunctor 0 f g (Rec (h' (b' (P 0 f))) (h (b f)))
                      (Rec (h' (b' (P 0 g))) (h (b g)))
  where
  gmap :: forall (x :: k).
Proxy 0
-> (forall (a :: k). f a -> g a)
-> Rec (h' (b' (P 0 f))) (h (b f)) x
-> Rec (h' (b' (P 0 g))) (h (b g)) x
gmap Proxy 0
_ forall (a :: k). f a -> g a
h (Rec (K1 h (b f)
hbf)) = 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 b. Functor f => (a -> b) -> f a -> f b
fmap (forall k (b :: (k -> *) -> *) (f :: k -> *) (g :: k -> *).
FunctorB b =>
(forall (a :: k). f a -> g a) -> b f -> b g
bmap forall (a :: k). f a -> g a
h) h (b f)
hbf))
  {-# INLINE gmap #-}

-- This is the same as the previous instance, but for nested (normal-flavoured)
-- functors.
instance
  ( Functor h
  , Functor m
  , FunctorB b
  ) => GFunctor 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))))
  where
  gmap :: forall (x :: k).
Proxy 0
-> (forall (a :: k). f a -> g a)
-> Rec (m' (h' (b' (P 0 f)))) (m (h (b f))) x
-> Rec (m' (h' (b' (P 0 g)))) (m (h (b g))) x
gmap Proxy 0
_ forall (a :: k). f a -> g a
h (Rec (K1 m (h (b f))
hbf)) = 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 b. Functor f => (a -> b) -> f a -> f b
fmap (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall k (b :: (k -> *) -> *) (f :: k -> *) (g :: k -> *).
FunctorB b =>
(forall (a :: k). f a -> g a) -> b f -> b g
bmap forall (a :: k). f a -> g a
h)) m (h (b f))
hbf))
  {-# INLINE gmap #-}


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

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

instance (FunctorB a, FunctorB b) => FunctorB (Product a b) where
  bmap :: forall (f :: k -> *) (g :: k -> *).
(forall (a :: k). f a -> g a) -> Product a b f -> Product a b g
bmap forall (a :: k). f a -> g a
f (Pair a f
x b f
y) = 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 -> *).
FunctorB b =>
(forall (a :: k). f a -> g a) -> b f -> b g
bmap forall (a :: k). f a -> g a
f a f
x) (forall k (b :: (k -> *) -> *) (f :: k -> *) (g :: k -> *).
FunctorB b =>
(forall (a :: k). f a -> g a) -> b f -> b g
bmap forall (a :: k). f a -> g a
f b f
y)
  {-# INLINE bmap #-}

instance (FunctorB a, FunctorB b) => FunctorB (Sum a b) where
  bmap :: forall (f :: k -> *) (g :: k -> *).
(forall (a :: k). f a -> g a) -> Sum a b f -> Sum a b g
bmap forall (a :: k). f a -> g a
f (InL a f
x) = forall {k} (f :: k -> *) (g :: k -> *) (a :: k). f a -> Sum f g a
InL (forall k (b :: (k -> *) -> *) (f :: k -> *) (g :: k -> *).
FunctorB b =>
(forall (a :: k). f a -> g a) -> b f -> b g
bmap forall (a :: k). f a -> g a
f a f
x)
  bmap forall (a :: k). f a -> g a
f (InR b f
x) = forall {k} (f :: k -> *) (g :: k -> *) (a :: k). g a -> Sum f g a
InR (forall k (b :: (k -> *) -> *) (f :: k -> *) (g :: k -> *).
FunctorB b =>
(forall (a :: k). f a -> g a) -> b f -> b g
bmap forall (a :: k). f a -> g a
f b f
x)
  {-# INLINE bmap #-}

instance FunctorB (Const x) where
  bmap :: forall (f :: k -> *) (g :: k -> *).
(forall (a :: k). f a -> g a) -> Const x f -> Const x g
bmap forall (a :: k). f a -> g a
_ (Const x
x) = forall {k} a (b :: k). a -> Const a b
Const x
x
  {-# INLINE bmap #-}

instance (Functor f, FunctorB b) => FunctorB (f `Compose` b) where
  bmap :: forall (f :: k -> *) (g :: k -> *).
(forall (a :: k). f a -> g a) -> Compose f b f -> Compose f b g
bmap forall (a :: k). f a -> g a
h (Compose f (b f)
x) = forall {k} {k1} (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose (forall k (b :: (k -> *) -> *) (f :: k -> *) (g :: k -> *).
FunctorB b =>
(forall (a :: k). f a -> g a) -> b f -> b g
bmap forall (a :: k). f a -> g a
h forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f (b f)
x)
  {-# INLINE bmap #-}


-- --------------------------------
-- Instances for transformer types
-- --------------------------------

instance FunctorB (Constant x) where
  bmap :: forall (f :: k -> *) (g :: k -> *).
(forall (a :: k). f a -> g a) -> Constant x f -> Constant x g
bmap forall (a :: k). f a -> g a
_ (Constant x
x) = forall {k} a (b :: k). a -> Constant a b
Constant x
x
  {-# INLINE bmap #-}