Monoidal.hs

{-# LANGUAGE CPP #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE MonoLocalBinds #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TypeFamilies #-}

-- | Rank-2 monoidal functors: the analogue of "Data.Functor.Monoidal" one level
-- up, for higher-kinded data @b :: (Type -> Type) -> Type@.
--
-- A rank-2 functor is a functor \(B : [\mathcal{Hask}, \mathcal{Hask}] \to \mathcal{Hask}\)
-- from the functor category to @Hask@; @b f@ reinterprets each field of the
-- record @b@ through @f@. "Kindly.Rank2" already supplies the functorial action
-- (@'Kindly.bmap1' :: (forall x. f x -> g x) -> b f -> b g@). This module adds the
-- /monoidal/ structure on top of it, the same way "Data.Functor.Monoidal" adds
-- 'Data.Functor.Monoidal.combine' \/ 'Data.Functor.Monoidal.introduce' on top of
-- an ordinary 'Functor'.
--
-- The classes keep the same parameter shape as their rank-1 siblings, only
-- lifted a kind: the domain tensor @tC@ now acts on functors while the codomain
-- tensor @tD@ still acts on @Hask@. A product-shaped record is monoidal at three
-- instantiations, all derivable from the record's 'GHC.Generics' structure:
--
-- * __Covariant product__, @'Monoidal' (->) 'Product' 'Data.Proxy.Proxy' (,) () b@.
--   This is @barbies@' @ApplicativeB@: 'combine' zips two records field-wise into
--   'Data.Functor.Product.Pair's (@bprod@) and 'introduce' fills every field with
--   'Data.Proxy.Proxy' (@bpure Proxy@).
--
-- * __Coproduct__, @'Monoidal' (->) 'Sum' V1 'Either' 'Data.Void.Void' b@. 'combine'
--   injects a whole record of @f@ or a whole record of @g@ into a record of
--   @'Sum' f g@, all on one side (@'gcombineSum'@). 'introduce' is
--   'Data.Void.absurd'.
--
-- * __These__, @'Monoidal' (->) 'These1' V1 'These' 'Data.Void.Void' b@. 'combine'
--   follows the outer 'These'. A record of @f@ becomes all-'This1', a record of
--   @g@ all-'That1', and a pair of records a field-wise 'These1'
--   (@'gcombineThese'@). 'introduce' is 'Data.Void.absurd'.
--
-- * __Oplax product__ (the @'Op'@ dual of the first), @'Monoidal' 'Op' 'Product' 'Data.Proxy.Proxy' (,) () b@.
--   'combine' unzips a record of 'Data.Functor.Product.Pair's back into two
--   records (@'gsplitProduct'@). 'introduce' is @'Op' ('const' ())@.
--
-- The coproduct and These have no oplax dual here. A record of independent
-- @'Sum' f g@ or @'These1' f g@ fields picks per field, so there is no single
-- @'Either' (b f) (b g)@ or @'These' (b f) (b g)@ to project back to. The
-- @Divisible@ \/ @Decidable@-style contravariant-functor duals need @f@ in
-- negative position, which is not the @f a@ field shape the generic machinery
-- walks. Neither is provided.
--
-- The generic derivation covers records whose fields all have the shape @f a@.
-- Sums and nested HKD fields are not supported, matching
-- "Data.Functor.Rank2.Traversable".
module Data.Functor.Rank2.Monoidal
  ( -- * Semigroupal
    Semigroupal (..),

    -- * Unital
    Unital (..),

    -- * Monoidal
    Monoidal,

    -- * Generic derivation helpers
    gcombineProduct,
    gsplitProduct,
    gcombineSum,
    gcombineThese,
  )
where

--------------------------------------------------------------------------------

import Data.Either (Either (..), either)
import Data.Function ((.))
import Data.Functor.Product (Product (..))
import Data.Functor.Sum (Sum (..))
import Data.Functor.These (These1 (..))
import Data.Kind (Constraint, Type)
import Data.Proxy (Proxy (..))
import Data.These (These (..), these)
#if MIN_VERSION_base(4,17,0)
-- On GHC 9.4+ (@base >= 4.17@) @~@ is an ordinary type operator rather than
-- built-in syntax, so under @NoImplicitPrelude@ it must be brought into scope.
-- Earlier GHCs still treat @~@ as built-in syntax and do not export it.
import Data.Type.Equality (type (~))
#endif
import GHC.Generics (Generic (..), K1 (..), M1 (..), U1 (..), type (:*:) (..))

--------------------------------------------------------------------------------

-- $setup
-- >>> :set -XDeriveGeneric -XStandaloneDeriving -XFlexibleContexts -XMultiParamTypeClasses -XTypeApplications
-- >>> import Prelude
-- >>> import GHC.Generics (Generic)
-- >>> import Data.Functor.Product (Product (..))
-- >>> import Data.Functor.Sum (Sum (..))
-- >>> import Data.Functor.These (These1 (..))
-- >>> import Data.Proxy (Proxy (..))
-- >>> import Data.These (These (..))
-- >>> :{
-- data Rec f = Rec {rFst :: f Int, rSnd :: f Bool} deriving Generic
-- deriving instance (Show (f Int), Show (f Bool)) => Show (Rec f)
-- instance Semigroupal (->) Product (,) Rec
-- instance Unital (->) Proxy () Rec
-- instance Monoidal (->) Product Proxy (,) () Rec
-- instance Semigroupal (->) Sum Either Rec where combine = gcombineSum
-- instance Semigroupal (->) These1 These Rec where combine = gcombineThese
-- :}

--------------------------------------------------------------------------------

-- | The rank-2 analogue of 'Data.Functor.Monoidal.Semigroupal'. Given a
-- monoidal structure \(\otimes\) on the functor category and \(\bullet\) on
-- @Hask@, a rank-2 functor @b@ is 'Semigroupal' if it carries a natural
-- transformation \(\phi_{f,g} : b\ f \bullet b\ g \to b\ (f \otimes g)\), which
-- we call 'combine'.
--
-- The parameters mirror the rank-1 class one kind up:
--
-- * @cat@ is the codomain category (@Hask@, or 'Op' for the oplax duals).
-- * @tC@ is the domain tensor, acting on functors (e.g. 'Product', 'Sum').
-- * @tD@ is the codomain tensor, acting on @Hask@ (e.g. @(,)@, 'Either').
-- * @b@ is the higher-kinded record.
--
-- The empty-instance default derives the covariant 'Product' instantiation. For
-- the coproduct and oplax-product instantiations, supply @'combine'@ from the
-- exported generic helpers (see 'gcombineSum' and 'gsplitProduct').
type Semigroupal ::
  (Type -> Type -> Type) ->
  ((Type -> Type) -> (Type -> Type) -> (Type -> Type)) ->
  (Type -> Type -> Type) ->
  ((Type -> Type) -> Type) ->
  Constraint
class Semigroupal cat tC tD b where
  -- | ==== __Examples__
  --
  -- Zip two records field-wise (the covariant 'Product' instantiation):
  --
  -- >>> combine @(->) @Product @(,) (Rec (Just 1) (Just True), Rec [10, 20] [False])
  -- Rec {rFst = Pair (Just 1) [10,20], rSnd = Pair (Just True) [False]}
  --
  -- Inject a whole record onto one side of a 'Sum' (the coproduct instantiation):
  --
  -- >>> combine @(->) @Sum @Either (Left (Rec (Just 1) (Just True)) :: Either (Rec Maybe) (Rec []))
  -- Rec {rFst = InL (Just 1), rSnd = InL (Just True)}
  --
  -- Merge two records field-wise through a 'These' (the These instantiation):
  --
  -- >>> combine @(->) @These1 @These (These (Rec (Just 1) (Just True)) (Rec [10] [False]) :: These (Rec Maybe) (Rec []))
  -- Rec {rFst = These1 (Just 1) [10], rSnd = These1 (Just True) [False]}
  combine :: forall f g. cat (tD (b f) (b g)) (b (tC f g))
  default combine ::
    forall f g.
    ( cat ~ (->),
      tC ~ Product,
      tD ~ (,),
      Generic (b f),
      Generic (b g),
      Generic (b (Product f g)),
      GSemigroupal (Rep (b f)) (Rep (b g)) (Rep (b (Product f g)))
    ) =>
    cat (tD (b f) (b g)) (b (tC f g))
  combine = gcombineProduct

--------------------------------------------------------------------------------

-- | The rank-2 analogue of 'Data.Functor.Monoidal.Unital'. A rank-2 functor
-- @b@ is 'Unital' if it carries a morphism from the codomain unit to @b@ at the
-- domain unit, which we call 'introduce'.
--
-- * @cat@ is the codomain category (@Hask@, or 'Op' for the oplax duals).
-- * @iC@ is the domain unit, a functor (the unit of @tC@; 'Proxy' for 'Product',
--   @V1@ for 'Sum').
-- * @iD@ is the codomain unit (the unit of @tD@; @()@ for @(,)@, 'Data.Void.Void'
--   for 'Either').
-- * @b@ is the higher-kinded record.
--
-- The empty-instance default derives the covariant 'Proxy' unit. The coproduct
-- unit is @'introduce' = 'Data.Void.absurd'@ and the oplax-product unit is
-- @'introduce' = 'Op' ('const' ())@. Both are trivial enough to write inline.
type Unital ::
  (Type -> Type -> Type) ->
  (Type -> Type) ->
  Type ->
  ((Type -> Type) -> Type) ->
  Constraint
class Unital cat iC iD b where
  -- | ==== __Examples__
  --
  -- >>> introduce @(->) @Proxy @() @Rec ()
  -- Rec {rFst = Proxy, rSnd = Proxy}
  introduce :: cat iD (b iC)
  default introduce ::
    ( cat ~ (->),
      iC ~ Proxy,
      iD ~ (),
      Generic (b Proxy),
      GUnital (Rep (b Proxy))
    ) =>
    cat iD (b iC)
  introduce () = to gintroduce

--------------------------------------------------------------------------------

-- | The rank-2 analogue of 'Data.Functor.Monoidal.Monoidal'. A rank-2 functor
-- that is both 'Semigroupal' and 'Unital', preserving the monoidal structure
-- between the functor category and @Hask@. At
-- @'Monoidal' (->) 'Product' 'Proxy' (,) () b@ this is @barbies@' @ApplicativeB@.
type Monoidal ::
  (Type -> Type -> Type) ->
  ((Type -> Type) -> (Type -> Type) -> (Type -> Type)) ->
  (Type -> Type) ->
  (Type -> Type -> Type) ->
  Type ->
  ((Type -> Type) -> Type) ->
  Constraint
class
  ( Semigroupal cat tC tD b,
    Unital cat iC iD b
  ) =>
  Monoidal cat tC iC tD iD b

--------------------------------------------------------------------------------
-- Generic derivation helpers.

-- | Generic covariant product 'combine': zip two records field-wise into
-- 'Data.Functor.Product.Pair's. This is the default for
-- @'Semigroupal' (->) 'Product' (,)@.
--
-- ==== __Examples__
--
-- >>> gcombineProduct (Rec (Just 1) (Just True), Rec [10] [False])
-- Rec {rFst = Pair (Just 1) [10], rSnd = Pair (Just True) [False]}
gcombineProduct ::
  ( Generic (b f),
    Generic (b g),
    Generic (b (Product f g)),
    GSemigroupal (Rep (b f)) (Rep (b g)) (Rep (b (Product f g)))
  ) =>
  (b f, b g) ->
  b (Product f g)
gcombineProduct (bf, bg) = to (gcombine (from bf, from bg))

-- | Generic oplax product 'combine': unzip a record of
-- 'Data.Functor.Product.Pair's back into two records. Wrap in 'Op' for
-- @'Semigroupal' 'Op' 'Product' (,)@: @combine = 'Op' 'gsplitProduct'@.
--
-- ==== __Examples__
--
-- >>> gsplitProduct (Rec (Pair (Just 1) [10]) (Pair (Just True) [False]))
-- (Rec {rFst = Just 1, rSnd = Just True},Rec {rFst = [10], rSnd = [False]})
gsplitProduct ::
  ( Generic (b f),
    Generic (b g),
    Generic (b (Product f g)),
    GSemigroupal (Rep (b f)) (Rep (b g)) (Rep (b (Product f g)))
  ) =>
  b (Product f g) ->
  (b f, b g)
gsplitProduct bfg = case gsplit (from bfg) of (l, r) -> (to l, to r)

-- | Generic coproduct 'combine': inject a whole record of @f@ or a whole record
-- of @g@ into a record of @'Sum' f g@, all on one side. This is @combine@ for
-- @'Semigroupal' (->) 'Sum' 'Either'@.
--
-- ==== __Examples__
--
-- >>> gcombineSum (Right (Rec [10] [False]) :: Either (Rec Maybe) (Rec []))
-- Rec {rFst = InR [10], rSnd = InR [False]}
gcombineSum ::
  ( Generic (b f),
    Generic (b g),
    Generic (b (Sum f g)),
    GCoproduct (Rep (b f)) (Rep (b g)) (Rep (b (Sum f g)))
  ) =>
  Either (b f) (b g) ->
  b (Sum f g)
gcombineSum = either (to . ginjectL . from) (to . ginjectR . from)

-- | Generic These 'combine': following the outer 'These', send a record of @f@
-- to an all-'This1' record, a record of @g@ to an all-'That1' record, or a pair
-- of records to a field-wise 'These1' record of @'These1' f g@. This is
-- @combine@ for @'Semigroupal' (->) 'These1' 'These'@.
--
-- ==== __Examples__
--
-- >>> gcombineThese (This (Rec (Just 1) (Just True)) :: These (Rec Maybe) (Rec []))
-- Rec {rFst = This1 (Just 1), rSnd = This1 (Just True)}
--
-- >>> gcombineThese (That (Rec [10] [False]) :: These (Rec Maybe) (Rec []))
-- Rec {rFst = That1 [10], rSnd = That1 [False]}
--
-- >>> gcombineThese (These (Rec (Just 1) (Just True)) (Rec [10] [False]) :: These (Rec Maybe) (Rec []))
-- Rec {rFst = These1 (Just 1) [10], rSnd = These1 (Just True) [False]}
gcombineThese ::
  ( Generic (b f),
    Generic (b g),
    Generic (b (These1 f g)),
    GThese (Rep (b f)) (Rep (b g)) (Rep (b (These1 f g)))
  ) =>
  These (b f) (b g) ->
  b (These1 f g)
gcombineThese =
  these
    (to . gthis . from)
    (to . gthat . from)
    (\bf bg -> to (gthese (from bf) (from bg)))

--------------------------------------------------------------------------------
-- Generic workers for the product tensor (zip and its inverse split).

-- | Generic worker for the 'Product' tensor. The three representations are
-- @'Rep' (b f)@, @'Rep' (b g)@, and @'Rep' (b (Product f g))@. They are
-- structurally identical up to the field interpretation, which 'gcombine' fuses
-- into a 'Data.Functor.Product.Pair' and 'gsplit' takes apart.
type GSemigroupal :: (Type -> Type) -> (Type -> Type) -> (Type -> Type) -> Constraint
class GSemigroupal repf repg reph where
  gcombine :: (repf x, repg x) -> reph x
  gsplit :: reph x -> (repf x, repg x)

instance (GSemigroupal repf repg reph) => GSemigroupal (M1 i c repf) (M1 i c repg) (M1 i c reph) where
  gcombine (M1 a, M1 b) = M1 (gcombine (a, b))
  gsplit (M1 a) = case gsplit a of (l, r) -> (M1 l, M1 r)

instance (GSemigroupal f1 g1 h1, GSemigroupal f2 g2 h2) => GSemigroupal (f1 :*: f2) (g1 :*: g2) (h1 :*: h2) where
  gcombine (a1 :*: a2, b1 :*: b2) = gcombine (a1, b1) :*: gcombine (a2, b2)
  gsplit (a1 :*: a2) = case (gsplit a1, gsplit a2) of ((l1, r1), (l2, r2)) -> (l1 :*: l2, r1 :*: r2)

instance GSemigroupal (K1 i (p a)) (K1 i (q a)) (K1 i (Product p q a)) where
  gcombine (K1 pa, K1 qa) = K1 (Pair pa qa)
  gsplit (K1 (Pair pa qa)) = (K1 pa, K1 qa)

instance GSemigroupal U1 U1 U1 where
  gcombine (U1, U1) = U1
  gsplit U1 = (U1, U1)

--------------------------------------------------------------------------------
-- Generic worker for the coproduct tensor (all-left \/ all-right injection).

-- | Generic worker for the 'Sum' tensor. 'ginjectL' sends a record of @f@ to a
-- record of @'Sum' f g@ with every field 'InL'; 'ginjectR' does the same with
-- 'InR'.
type GCoproduct :: (Type -> Type) -> (Type -> Type) -> (Type -> Type) -> Constraint
class GCoproduct repf repg reph | reph -> repf repg where
  ginjectL :: repf x -> reph x
  ginjectR :: repg x -> reph x

instance (GCoproduct repf repg reph) => GCoproduct (M1 i c repf) (M1 i c repg) (M1 i c reph) where
  ginjectL (M1 a) = M1 (ginjectL a)
  ginjectR (M1 a) = M1 (ginjectR a)

instance (GCoproduct f1 g1 h1, GCoproduct f2 g2 h2) => GCoproduct (f1 :*: f2) (g1 :*: g2) (h1 :*: h2) where
  ginjectL (a1 :*: a2) = ginjectL a1 :*: ginjectL a2
  ginjectR (a1 :*: a2) = ginjectR a1 :*: ginjectR a2

instance GCoproduct (K1 i (f a)) (K1 i (g a)) (K1 i (Sum f g a)) where
  ginjectL (K1 fa) = K1 (InL fa)
  ginjectR (K1 ga) = K1 (InR ga)

instance GCoproduct U1 U1 U1 where
  ginjectL U1 = U1
  ginjectR U1 = U1

--------------------------------------------------------------------------------
-- Generic worker for the These tensor (per-side injection following an outer These).

-- | Generic worker for the 'These1' tensor. 'gthis' sends a record of @f@ to an
-- all-'This1' record, 'gthat' a record of @g@ to an all-'That1' record, and
-- 'gthese' a pair of records to a field-wise 'These1' record.
type GThese :: (Type -> Type) -> (Type -> Type) -> (Type -> Type) -> Constraint
class GThese repf repg reph | reph -> repf repg where
  gthis :: repf x -> reph x
  gthat :: repg x -> reph x
  gthese :: repf x -> repg x -> reph x

instance (GThese repf repg reph) => GThese (M1 i c repf) (M1 i c repg) (M1 i c reph) where
  gthis (M1 a) = M1 (gthis a)
  gthat (M1 a) = M1 (gthat a)
  gthese (M1 a) (M1 b) = M1 (gthese a b)

instance (GThese f1 g1 h1, GThese f2 g2 h2) => GThese (f1 :*: f2) (g1 :*: g2) (h1 :*: h2) where
  gthis (a1 :*: a2) = gthis a1 :*: gthis a2
  gthat (a1 :*: a2) = gthat a1 :*: gthat a2
  gthese (a1 :*: a2) (b1 :*: b2) = gthese a1 b1 :*: gthese a2 b2

instance GThese (K1 i (f a)) (K1 i (g a)) (K1 i (These1 f g a)) where
  gthis (K1 fa) = K1 (This1 fa)
  gthat (K1 ga) = K1 (That1 ga)
  gthese (K1 fa) (K1 ga) = K1 (These1 fa ga)

instance GThese U1 U1 U1 where
  gthis U1 = U1
  gthat U1 = U1
  gthese U1 U1 = U1

--------------------------------------------------------------------------------
-- Generic worker for the unit (fill every field with the domain unit).

-- | Generic worker for 'introduce' at the covariant 'Proxy' unit: fills every
-- field of @'Rep' (b Proxy)@ with 'Proxy'.
type GUnital :: (Type -> Type) -> Constraint
class GUnital rep where
  gintroduce :: rep x

instance (GUnital rep) => GUnital (M1 i c rep) where
  gintroduce = M1 gintroduce

instance (GUnital f, GUnital g) => GUnital (f :*: g) where
  gintroduce = gintroduce :*: gintroduce

instance GUnital (K1 i (Proxy a)) where
  gintroduce = K1 Proxy

instance GUnital U1 where
  gintroduce = U1