Day.hs

{-# LANGUAGE AllowAmbiguousTypes #-}

-- | A third way to combine two flavors, alongside 'Proarrow.Optic.Prod.ProdFl' and
-- 'Proarrow.Optic.Sum.SumFl': via the Day convolution. Unlike those two, it keeps both witnesses
-- in the same ambient categories @j@\/@k@. It needs 'Monoidal' structure there to split objects
-- across the two witnesses, where the others pair\/sum two independent categories.
module Proarrow.Optic.Day where

import Prelude (($))

import Proarrow.Category.Monoidal (Monoidal (..), type (**))
import Proarrow.Core (CAT, CategoryOf (..), (\\), type (+->))
import Proarrow.Object (pattern Objs)
import Proarrow.Optic (FLAVOR, Flavor, Optic, Prostrong (..), legs2prof, withLegs)
import Proarrow.Profunctor.Instance.Composition ((:.:) (..))
import Proarrow.Profunctor.Instance.Day (Day, day)
import Proarrow.Profunctor.Instance.Identity (Id (..))

type DayFl :: FLAVOR j k -> FLAVOR j k -> FLAVOR j k
class DayFl w1 w2 (p :: k +-> k) (q :: j +-> j)
instance (w1 p1 q1, w2 p2 q2) => DayFl w1 w2 (Day p1 p2) (Day q1 q2)
instance (CategoryOf k, CategoryOf j) => DayFl w1 w2 (Id :: CAT k) (Id :: CAT j)
instance (DayFl w1 w2 f f', DayFl w1 w2 g g') => DayFl w1 w2 (f :.: g) (g' :.: f')

dayOptic
  :: forall {j} {k} (w1 :: FLAVOR j k) (w2 :: FLAVOR j k) s1 t1 a1 b1 s2 t2 a2 b2
   . (Monoidal j, Monoidal k, Flavor w1, Flavor w2)
  => Optic (Prostrong w1) s1 t1 a1 b1
  -> Optic (Prostrong w2) s2 t2 a2 b2
  -> Optic (Prostrong (DayFl w1 w2)) (s1 ** s2) (t1 ** t2) (a1 ** a2) (b1 ** b2)
dayOptic o1 o2 =
  withLegs @w1 o1 \l1@Objs r1@Objs ->
    withLegs @w2 o2 \l2@Objs r2@Objs ->
      withOb2 @k @a1 @a2 $
        withOb2 @j @b1 @b2 $
          legs2prof @(DayFl w1 w2) (day l1 l2) (day r1 r2) \\ l1 \\ r1 \\ l2 \\ r2