{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE ImportQualifiedPost #-}

module Data.Profunctor.Bicartesian.Free(
  FreeBicartesian(..),
  liftF, foldFree,

  -- * Utilities
  ProductOp,
  multF
) where

import Data.Profunctor (Profunctor(..), (:->))
import Data.Profunctor.Cartesian
import Data.Bifunctor (Bifunctor(..))
import Data.Profunctor.Monad
import Data.Profunctor.Day

import Data.Profunctor.Cocartesian.Free (FreeCocartesian)
import Data.Profunctor.Cocartesian.Free qualified as CF

-- | Free Bicartesian profunctor (with caveat -- see below) a Cartesian profunctor.
-- 
-- ==== Law issues:
-- 
-- @'FreeBicartesian' p@ can be thought of as a way to add 'Cocartesian' operations
-- on @'Cartesian' p@ by taking "formal sums" of multplie values of @p a b@.
-- 
-- Products on sums of multiple values are normalized to sum of products **as if**
-- it satisfy both left and right /distribution/ laws and /zero/ laws.
-- For example, the result of
-- 
-- @
-- (p1 +++ p2) *** (q1 +++ q2)
-- @
-- 
-- is normalized to
--
-- @
-- (p1 *** q1) +++ (p1 *** q2) +++ (p2 *** q1) +++ (p2 *** q2)
-- @
--
-- up to isomorphisms of parameters of these profunctors.
--
-- Because there are some profunctors which are both @Cartesian@ and @Cocartesian@
-- but do not satisfy distributive laws,
-- interpreting 'FreeBicartesian' into such a profunctor might cause a surprising behavior.
--
-- For example, @'Data.Bifunctor.Joker.Joker' []@ does not satisfy /right distribution/,
-- inheriting @Alternative []@ does not.
-- 
-- >>> import Control.Applicative
-- >>> let x = [id, id]
-- >>> let y = [1]; z = [2]
-- >>> x <*> (y <|> z)
-- [1,2,1,2]
-- >>> (x <*> y) <|> (x <*> z)
-- [1,1,2,2]
-- 
-- With such non-distributive @p@, 'foldFree' does not preserve
-- the @Cartesian@ operations. The following equation does not have to hold.
--
-- @
-- -- Not necessarily holds!
-- foldFree id (ps *** qs)
--  == foldFree id ps *** foldFree id qs
-- @
-- 
-- It is guaranteed that @'foldFree' f@ preserves both @Cartesian@ and
-- @Cocartesian@ operations if it is intepreting into a Bicartesian profunctor,
-- in other words both @Cartesian p@ and @Cocartesian p@ which satisfy these additional laws.
--
-- - @Cocartesian@ instance is commutative
-- - /Left zero/, /Right zero/, /Left distribution/, /Right distribution/
-- 
-- There are no guarantees if any of these conditions are not met. 
newtype FreeBicartesian p a b = FreeBicartesian {
    forall (p :: * -> * -> *) a b.
FreeBicartesian p a b -> FreeCocartesian p a b
runFreeBicartesian :: FreeCocartesian p a b
  }
  deriving newtype ((forall a b.
 (a -> b) -> FreeBicartesian p a a -> FreeBicartesian p a b)
-> (forall a b.
    a -> FreeBicartesian p a b -> FreeBicartesian p a a)
-> Functor (FreeBicartesian p a)
forall a b. a -> FreeBicartesian p a b -> FreeBicartesian p a a
forall a b.
(a -> b) -> FreeBicartesian p a a -> FreeBicartesian p a b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
forall (p :: * -> * -> *) a a b.
a -> FreeBicartesian p a b -> FreeBicartesian p a a
forall (p :: * -> * -> *) a a b.
(a -> b) -> FreeBicartesian p a a -> FreeBicartesian p a b
$cfmap :: forall (p :: * -> * -> *) a a b.
(a -> b) -> FreeBicartesian p a a -> FreeBicartesian p a b
fmap :: forall a b.
(a -> b) -> FreeBicartesian p a a -> FreeBicartesian p a b
$c<$ :: forall (p :: * -> * -> *) a a b.
a -> FreeBicartesian p a b -> FreeBicartesian p a a
<$ :: forall a b. a -> FreeBicartesian p a b -> FreeBicartesian p a a
Functor, (forall a b c d.
 (a -> b)
 -> (c -> d) -> FreeBicartesian p b c -> FreeBicartesian p a d)
-> (forall a b c.
    (a -> b) -> FreeBicartesian p b c -> FreeBicartesian p a c)
-> (forall b c a.
    (b -> c) -> FreeBicartesian p a b -> FreeBicartesian p a c)
-> (forall a b c (q :: * -> * -> *).
    Coercible c b =>
    q b c -> FreeBicartesian p a b -> FreeBicartesian p a c)
-> (forall a b c (q :: * -> * -> *).
    Coercible b a =>
    FreeBicartesian p b c -> q a b -> FreeBicartesian p a c)
-> Profunctor (FreeBicartesian p)
forall a b c.
(a -> b) -> FreeBicartesian p b c -> FreeBicartesian p a c
forall b c a.
(b -> c) -> FreeBicartesian p a b -> FreeBicartesian p a c
forall a b c d.
(a -> b)
-> (c -> d) -> FreeBicartesian p b c -> FreeBicartesian p a d
forall a b c (q :: * -> * -> *).
Coercible b a =>
FreeBicartesian p b c -> q a b -> FreeBicartesian p a c
forall a b c (q :: * -> * -> *).
Coercible c b =>
q b c -> FreeBicartesian p a b -> FreeBicartesian p a c
forall (p :: * -> * -> *).
(forall a b c d. (a -> b) -> (c -> d) -> p b c -> p a d)
-> (forall a b c. (a -> b) -> p b c -> p a c)
-> (forall b c a. (b -> c) -> p a b -> p a c)
-> (forall a b c (q :: * -> * -> *).
    Coercible c b =>
    q b c -> p a b -> p a c)
-> (forall a b c (q :: * -> * -> *).
    Coercible b a =>
    p b c -> q a b -> p a c)
-> Profunctor p
forall (p :: * -> * -> *) a b c.
(a -> b) -> FreeBicartesian p b c -> FreeBicartesian p a c
forall (p :: * -> * -> *) b c a.
(b -> c) -> FreeBicartesian p a b -> FreeBicartesian p a c
forall (p :: * -> * -> *) a b c d.
(a -> b)
-> (c -> d) -> FreeBicartesian p b c -> FreeBicartesian p a d
forall (p :: * -> * -> *) a b c (q :: * -> * -> *).
Coercible b a =>
FreeBicartesian p b c -> q a b -> FreeBicartesian p a c
forall (p :: * -> * -> *) a b c (q :: * -> * -> *).
Coercible c b =>
q b c -> FreeBicartesian p a b -> FreeBicartesian p a c
$cdimap :: forall (p :: * -> * -> *) a b c d.
(a -> b)
-> (c -> d) -> FreeBicartesian p b c -> FreeBicartesian p a d
dimap :: forall a b c d.
(a -> b)
-> (c -> d) -> FreeBicartesian p b c -> FreeBicartesian p a d
$clmap :: forall (p :: * -> * -> *) a b c.
(a -> b) -> FreeBicartesian p b c -> FreeBicartesian p a c
lmap :: forall a b c.
(a -> b) -> FreeBicartesian p b c -> FreeBicartesian p a c
$crmap :: forall (p :: * -> * -> *) b c a.
(b -> c) -> FreeBicartesian p a b -> FreeBicartesian p a c
rmap :: forall b c a.
(b -> c) -> FreeBicartesian p a b -> FreeBicartesian p a c
$c#. :: forall (p :: * -> * -> *) a b c (q :: * -> * -> *).
Coercible c b =>
q b c -> FreeBicartesian p a b -> FreeBicartesian p a c
#. :: forall a b c (q :: * -> * -> *).
Coercible c b =>
q b c -> FreeBicartesian p a b -> FreeBicartesian p a c
$c.# :: forall (p :: * -> * -> *) a b c (q :: * -> * -> *).
Coercible b a =>
FreeBicartesian p b c -> q a b -> FreeBicartesian p a c
.# :: forall a b c (q :: * -> * -> *).
Coercible b a =>
FreeBicartesian p b c -> q a b -> FreeBicartesian p a c
Profunctor, (forall (p :: * -> * -> *) (q :: * -> * -> *).
 Profunctor p =>
 (p :-> q) -> FreeBicartesian p :-> FreeBicartesian q)
-> ProfunctorFunctor FreeBicartesian
forall {k} {k1} (t :: (* -> * -> *) -> k -> k1 -> *).
(forall (p :: * -> * -> *) (q :: * -> * -> *).
 Profunctor p =>
 (p :-> q) -> t p :-> t q)
-> ProfunctorFunctor t
forall (p :: * -> * -> *) (q :: * -> * -> *).
Profunctor p =>
(p :-> q) -> FreeBicartesian p :-> FreeBicartesian q
$cpromap :: forall (p :: * -> * -> *) (q :: * -> * -> *).
Profunctor p =>
(p :-> q) -> FreeBicartesian p :-> FreeBicartesian q
promap :: forall (p :: * -> * -> *) (q :: * -> * -> *).
Profunctor p =>
(p :-> q) -> FreeBicartesian p :-> FreeBicartesian q
ProfunctorFunctor, ProfunctorFunctor FreeBicartesian
ProfunctorFunctor FreeBicartesian =>
(forall (p :: * -> * -> *).
 Profunctor p =>
 p :-> FreeBicartesian p)
-> (forall (p :: * -> * -> *).
    Profunctor p =>
    FreeBicartesian (FreeBicartesian p) :-> FreeBicartesian p)
-> ProfunctorMonad FreeBicartesian
forall (p :: * -> * -> *). Profunctor p => p :-> FreeBicartesian p
forall (p :: * -> * -> *).
Profunctor p =>
FreeBicartesian (FreeBicartesian p) :-> FreeBicartesian p
forall (t :: (* -> * -> *) -> * -> * -> *).
ProfunctorFunctor t =>
(forall (p :: * -> * -> *). Profunctor p => p :-> t p)
-> (forall (p :: * -> * -> *). Profunctor p => t (t p) :-> t p)
-> ProfunctorMonad t
$cproreturn :: forall (p :: * -> * -> *). Profunctor p => p :-> FreeBicartesian p
proreturn :: forall (p :: * -> * -> *). Profunctor p => p :-> FreeBicartesian p
$cprojoin :: forall (p :: * -> * -> *).
Profunctor p =>
FreeBicartesian (FreeBicartesian p) :-> FreeBicartesian p
projoin :: forall (p :: * -> * -> *).
Profunctor p =>
FreeBicartesian (FreeBicartesian p) :-> FreeBicartesian p
ProfunctorMonad, Profunctor (FreeBicartesian p)
Profunctor (FreeBicartesian p) =>
(forall b. FreeBicartesian p Void b)
-> (forall a a1 a2 b1 b2 b.
    (a -> Either a1 a2)
    -> (Either b1 b2 -> b)
    -> FreeBicartesian p a1 b1
    -> FreeBicartesian p a2 b2
    -> FreeBicartesian p a b)
-> (forall a b a' b'.
    FreeBicartesian p a b
    -> FreeBicartesian p a' b'
    -> FreeBicartesian p (Either a a') (Either b b'))
-> (forall a b a'.
    FreeBicartesian p a b
    -> FreeBicartesian p a' b -> FreeBicartesian p (Either a a') b)
-> (forall (n :: Nat) a b.
    KnownNat n =>
    FreeBicartesian p a b
    -> FreeBicartesian p (Finite n, a) (Finite n, b))
-> Cocartesian (FreeBicartesian p)
forall (n :: Nat) a b.
KnownNat n =>
FreeBicartesian p a b
-> FreeBicartesian p (Finite n, a) (Finite n, b)
forall b. FreeBicartesian p Void b
forall a b a'.
FreeBicartesian p a b
-> FreeBicartesian p a' b -> FreeBicartesian p (Either a a') b
forall a b a' b'.
FreeBicartesian p a b
-> FreeBicartesian p a' b'
-> FreeBicartesian p (Either a a') (Either b b')
forall a a1 a2 b1 b2 b.
(a -> Either a1 a2)
-> (Either b1 b2 -> b)
-> FreeBicartesian p a1 b1
-> FreeBicartesian p a2 b2
-> FreeBicartesian p a b
forall (p :: * -> * -> *).
Profunctor p =>
Profunctor (FreeBicartesian p)
forall (p :: * -> * -> *).
Profunctor p =>
(forall b. p Void b)
-> (forall a a1 a2 b1 b2 b.
    (a -> Either a1 a2)
    -> (Either b1 b2 -> b) -> p a1 b1 -> p a2 b2 -> p a b)
-> (forall a b a' b'.
    p a b -> p a' b' -> p (Either a a') (Either b b'))
-> (forall a b a'. p a b -> p a' b -> p (Either a a') b)
-> (forall (n :: Nat) a b.
    KnownNat n =>
    p a b -> p (Finite n, a) (Finite n, b))
-> Cocartesian p
forall (p :: * -> * -> *) (n :: Nat) a b.
(Profunctor p, KnownNat n) =>
FreeBicartesian p a b
-> FreeBicartesian p (Finite n, a) (Finite n, b)
forall (p :: * -> * -> *) b.
Profunctor p =>
FreeBicartesian p Void b
forall (p :: * -> * -> *) a b a'.
Profunctor p =>
FreeBicartesian p a b
-> FreeBicartesian p a' b -> FreeBicartesian p (Either a a') b
forall (p :: * -> * -> *) a b a' b'.
Profunctor p =>
FreeBicartesian p a b
-> FreeBicartesian p a' b'
-> FreeBicartesian p (Either a a') (Either b b')
forall (p :: * -> * -> *) a a1 a2 b1 b2 b.
Profunctor p =>
(a -> Either a1 a2)
-> (Either b1 b2 -> b)
-> FreeBicartesian p a1 b1
-> FreeBicartesian p a2 b2
-> FreeBicartesian p a b
$cproEmpty :: forall (p :: * -> * -> *) b.
Profunctor p =>
FreeBicartesian p Void b
proEmpty :: forall b. FreeBicartesian p Void b
$cproSum :: forall (p :: * -> * -> *) a a1 a2 b1 b2 b.
Profunctor p =>
(a -> Either a1 a2)
-> (Either b1 b2 -> b)
-> FreeBicartesian p a1 b1
-> FreeBicartesian p a2 b2
-> FreeBicartesian p a b
proSum :: forall a a1 a2 b1 b2 b.
(a -> Either a1 a2)
-> (Either b1 b2 -> b)
-> FreeBicartesian p a1 b1
-> FreeBicartesian p a2 b2
-> FreeBicartesian p a b
$c+++ :: forall (p :: * -> * -> *) a b a' b'.
Profunctor p =>
FreeBicartesian p a b
-> FreeBicartesian p a' b'
-> FreeBicartesian p (Either a a') (Either b b')
+++ :: forall a b a' b'.
FreeBicartesian p a b
-> FreeBicartesian p a' b'
-> FreeBicartesian p (Either a a') (Either b b')
$c||| :: forall (p :: * -> * -> *) a b a'.
Profunctor p =>
FreeBicartesian p a b
-> FreeBicartesian p a' b -> FreeBicartesian p (Either a a') b
||| :: forall a b a'.
FreeBicartesian p a b
-> FreeBicartesian p a' b -> FreeBicartesian p (Either a a') b
$cproTimes :: forall (p :: * -> * -> *) (n :: Nat) a b.
(Profunctor p, KnownNat n) =>
FreeBicartesian p a b
-> FreeBicartesian p (Finite n, a) (Finite n, b)
proTimes :: forall (n :: Nat) a b.
KnownNat n =>
FreeBicartesian p a b
-> FreeBicartesian p (Finite n, a) (Finite n, b)
Cocartesian)

liftF :: p a b -> FreeBicartesian p a b
liftF :: forall (p :: * -> * -> *) a b. p a b -> FreeBicartesian p a b
liftF = FreeCocartesian p a b -> FreeBicartesian p a b
forall (p :: * -> * -> *) a b.
FreeCocartesian p a b -> FreeBicartesian p a b
FreeBicartesian (FreeCocartesian p a b -> FreeBicartesian p a b)
-> (p a b -> FreeCocartesian p a b)
-> p a b
-> FreeBicartesian p a b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. p a b -> FreeCocartesian p a b
forall (p :: * -> * -> *) a b. p a b -> FreeCocartesian p a b
CF.liftF

-- | Interpret a @FreeBicartesian p@ into a Bicartesian profunction @q@.
--
-- It is guaranteed that @'foldFree' f@ preserves both @Cartesian@ and
-- @Cocartesian@ operations if @q@ is a Bicartesian profunctor.
-- There are no guarantees if any of extra laws to be a Bicartesian are not met. 
foldFree :: (Cartesian q, Cocartesian q) => (p :-> q) -> (FreeBicartesian p :-> q)
foldFree :: forall (q :: * -> * -> *) (p :: * -> * -> *).
(Cartesian q, Cocartesian q) =>
(p :-> q) -> FreeBicartesian p :-> q
foldFree p :-> q
h = (p :-> q) -> FreeCocartesian p :-> q
forall (q :: * -> * -> *) (p :: * -> * -> *).
Cocartesian q =>
(p :-> q) -> FreeCocartesian p :-> q
CF.foldFree p a b -> q a b
p :-> q
h (FreeCocartesian p a b -> q a b)
-> (FreeBicartesian p a b -> FreeCocartesian p a b)
-> FreeBicartesian p a b
-> q a b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FreeBicartesian p a b -> FreeCocartesian p a b
forall (p :: * -> * -> *) a b.
FreeBicartesian p a b -> FreeCocartesian p a b
runFreeBicartesian

instance Cartesian p => Applicative (FreeBicartesian p a) where
  pure :: forall a. a -> FreeBicartesian p a a
pure = a -> FreeBicartesian p a a
forall (p :: * -> * -> *) b a. Cartesian p => b -> p a b
pureDefault
  liftA2 :: forall a b c.
(a -> b -> c)
-> FreeBicartesian p a a
-> FreeBicartesian p a b
-> FreeBicartesian p a c
liftA2 = (a -> b -> c)
-> FreeBicartesian p a a
-> FreeBicartesian p a b
-> FreeBicartesian p a c
forall (p :: * -> * -> *) a b c x.
Cartesian p =>
(a -> b -> c) -> p x a -> p x b -> p x c
liftA2Default

instance Cartesian p => Cartesian (FreeBicartesian p) where
  proUnit :: forall a. FreeBicartesian p a ()
proUnit = p a () -> FreeBicartesian p a ()
forall (p :: * -> * -> *) a b. p a b -> FreeBicartesian p a b
liftF p a ()
forall a. p a ()
forall (p :: * -> * -> *) a. Cartesian p => p a ()
proUnit
  FreeBicartesian FreeCocartesian p a b
ps *** :: forall a b a' b'.
FreeBicartesian p a b
-> FreeBicartesian p a' b' -> FreeBicartesian p (a, a') (b, b')
*** FreeBicartesian FreeCocartesian p a' b'
qs = FreeCocartesian p (a, a') (b, b')
-> FreeBicartesian p (a, a') (b, b')
forall (p :: * -> * -> *) a b.
FreeCocartesian p a b -> FreeBicartesian p a b
FreeBicartesian (FreeCocartesian p (a, a') (b, b')
 -> FreeBicartesian p (a, a') (b, b'))
-> FreeCocartesian p (a, a') (b, b')
-> FreeBicartesian p (a, a') (b, b')
forall a b. (a -> b) -> a -> b
$ ProductOp p p p
-> FreeCocartesian p a b
-> FreeCocartesian p a' b'
-> FreeCocartesian p (a, a') (b, b')
forall (p :: * -> * -> *) (q :: * -> * -> *) (r :: * -> * -> *) a b
       a' b'.
ProductOp p q r
-> FreeCocartesian p a b
-> FreeCocartesian q a' b'
-> FreeCocartesian r (a, a') (b, b')
multF p a1 b1 -> p a2 b2 -> p (a1, a2) (b1, b2)
ProductOp p p p
forall (p :: * -> * -> *) a b a' b'.
Cartesian p =>
p a b -> p a' b' -> p (a, a') (b, b')
(***) FreeCocartesian p a b
ps FreeCocartesian p a' b'
qs

type ProductOp p q r = forall a1 b1 a2 b2. p a1 b1 -> q a2 b2 -> r (a1,a2) (b1,b2)

multF :: ProductOp p q r -> FreeCocartesian p a b -> FreeCocartesian q a' b' -> FreeCocartesian r (a,a') (b,b')
multF :: forall (p :: * -> * -> *) (q :: * -> * -> *) (r :: * -> * -> *) a b
       a' b'.
ProductOp p q r
-> FreeCocartesian p a b
-> FreeCocartesian q a' b'
-> FreeCocartesian r (a, a') (b, b')
multF ProductOp p q r
_    (CF.Neutral a -> Void
z) FreeCocartesian q a' b'
_ = ((a, a') -> Void)
-> FreeCocartesian r Void (b, b')
-> FreeCocartesian r (a, a') (b, b')
forall a b c.
(a -> b) -> FreeCocartesian r b c -> FreeCocartesian r a c
forall (p :: * -> * -> *) a b c.
Profunctor p =>
(a -> b) -> p b c -> p a c
lmap (a -> Void
z (a -> Void) -> ((a, a') -> a) -> (a, a') -> Void
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a, a') -> a
forall a b. (a, b) -> a
fst) FreeCocartesian r Void (b, b')
forall (p :: * -> * -> *) b. FreeCocartesian p Void b
CF.emptyF
multF ProductOp p q r
prod (CF.Cons (Day p a1 b1
p FreeCocartesian p a2 b2
ps' a -> Either a1 a2
opA Either b1 b2 -> b
opB)) FreeCocartesian q a' b'
qs
  = Day Either (FreeCocartesian r) (FreeCocartesian r) (a, a') (b, b')
-> FreeCocartesian r (a, a') (b, b')
forall (p :: * -> * -> *) a b.
Day Either (FreeCocartesian p) (FreeCocartesian p) a b
-> FreeCocartesian p a b
CF.sumDayF (Day Either (FreeCocartesian r) (FreeCocartesian r) (a, a') (b, b')
 -> FreeCocartesian r (a, a') (b, b'))
-> Day
     Either (FreeCocartesian r) (FreeCocartesian r) (a, a') (b, b')
-> FreeCocartesian r (a, a') (b, b')
forall a b. (a -> b) -> a -> b
$ FreeCocartesian r (a1, a') (b1, b')
-> FreeCocartesian r (a2, a') (b2, b')
-> ((a, a') -> Either (a1, a') (a2, a'))
-> (Either (b1, b') (b2, b') -> (b, b'))
-> Day
     Either (FreeCocartesian r) (FreeCocartesian r) (a, a') (b, b')
forall (p :: * -> * -> *) a1 b1 (q :: * -> * -> *) a2 b2 a
       (t :: * -> * -> *) b.
p a1 b1
-> q a2 b2 -> (a -> t a1 a2) -> (t b1 b2 -> b) -> Day t p q a b
Day (ProductOp p q r
-> p a1 b1
-> FreeCocartesian q a' b'
-> FreeCocartesian r (a1, a') (b1, b')
forall (p :: * -> * -> *) (q :: * -> * -> *) (r :: * -> * -> *) a b
       a' b'.
ProductOp p q r
-> p a b
-> FreeCocartesian q a' b'
-> FreeCocartesian r (a, a') (b, b')
distLeftFree p a1 b1 -> q a2 b2 -> r (a1, a2) (b1, b2)
ProductOp p q r
prod p a1 b1
p FreeCocartesian q a' b'
qs) (ProductOp p q r
-> FreeCocartesian p a2 b2
-> FreeCocartesian q a' b'
-> FreeCocartesian r (a2, a') (b2, b')
forall (p :: * -> * -> *) (q :: * -> * -> *) (r :: * -> * -> *) a b
       a' b'.
ProductOp p q r
-> FreeCocartesian p a b
-> FreeCocartesian q a' b'
-> FreeCocartesian r (a, a') (b, b')
multF p a1 b1 -> q a2 b2 -> r (a1, a2) (b1, b2)
ProductOp p q r
prod FreeCocartesian p a2 b2
ps' FreeCocartesian q a' b'
qs) ((Either a1 a2, a') -> Either (a1, a') (a2, a')
forall a b c. (Either a b, c) -> Either (a, c) (b, c)
distL ((Either a1 a2, a') -> Either (a1, a') (a2, a'))
-> ((a, a') -> (Either a1 a2, a'))
-> (a, a')
-> Either (a1, a') (a2, a')
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> Either a1 a2) -> (a, a') -> (Either a1 a2, a')
forall a b c. (a -> b) -> (a, c) -> (b, c)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first a -> Either a1 a2
opA) ((Either b1 b2 -> b) -> (Either b1 b2, b') -> (b, b')
forall a b c. (a -> b) -> (a, c) -> (b, c)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first Either b1 b2 -> b
opB ((Either b1 b2, b') -> (b, b'))
-> (Either (b1, b') (b2, b') -> (Either b1 b2, b'))
-> Either (b1, b') (b2, b')
-> (b, b')
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Either (b1, b') (b2, b') -> (Either b1 b2, b')
forall a c b. Either (a, c) (b, c) -> (Either a b, c)
undistL)

distLeftFree :: ProductOp p q r -> p a b -> FreeCocartesian q a' b' -> FreeCocartesian r (a,a') (b,b')
distLeftFree :: forall (p :: * -> * -> *) (q :: * -> * -> *) (r :: * -> * -> *) a b
       a' b'.
ProductOp p q r
-> p a b
-> FreeCocartesian q a' b'
-> FreeCocartesian r (a, a') (b, b')
distLeftFree ProductOp p q r
_    p a b
_ (CF.Neutral a' -> Void
z) = ((a, a') -> Void)
-> FreeCocartesian r Void (b, b')
-> FreeCocartesian r (a, a') (b, b')
forall a b c.
(a -> b) -> FreeCocartesian r b c -> FreeCocartesian r a c
forall (p :: * -> * -> *) a b c.
Profunctor p =>
(a -> b) -> p b c -> p a c
lmap (a' -> Void
z (a' -> Void) -> ((a, a') -> a') -> (a, a') -> Void
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a, a') -> a'
forall a b. (a, b) -> b
snd) FreeCocartesian r Void (b, b')
forall (p :: * -> * -> *) b. FreeCocartesian p Void b
CF.emptyF
distLeftFree ProductOp p q r
prod p a b
p (CF.Cons (Day q a1 b1
q FreeCocartesian q a2 b2
qs' a' -> Either a1 a2
opA Either b1 b2 -> b'
opB)) = Day Either r (FreeCocartesian r) (a, a') (b, b')
-> FreeCocartesian r (a, a') (b, b')
forall (p :: * -> * -> *) a b.
Day Either p (FreeCocartesian p) a b -> FreeCocartesian p a b
CF.Cons (Day Either r (FreeCocartesian r) (a, a') (b, b')
 -> FreeCocartesian r (a, a') (b, b'))
-> Day Either r (FreeCocartesian r) (a, a') (b, b')
-> FreeCocartesian r (a, a') (b, b')
forall a b. (a -> b) -> a -> b
$ r (a, a1) (b, b1)
-> FreeCocartesian r (a, a2) (b, b2)
-> ((a, a') -> Either (a, a1) (a, a2))
-> (Either (b, b1) (b, b2) -> (b, b'))
-> Day Either r (FreeCocartesian r) (a, a') (b, b')
forall (p :: * -> * -> *) a1 b1 (q :: * -> * -> *) a2 b2 a
       (t :: * -> * -> *) b.
p a1 b1
-> q a2 b2 -> (a -> t a1 a2) -> (t b1 b2 -> b) -> Day t p q a b
Day (p a b -> q a1 b1 -> r (a, a1) (b, b1)
ProductOp p q r
prod p a b
p q a1 b1
q) (ProductOp p q r
-> p a b
-> FreeCocartesian q a2 b2
-> FreeCocartesian r (a, a2) (b, b2)
forall (p :: * -> * -> *) (q :: * -> * -> *) (r :: * -> * -> *) a b
       a' b'.
ProductOp p q r
-> p a b
-> FreeCocartesian q a' b'
-> FreeCocartesian r (a, a') (b, b')
distLeftFree p a1 b1 -> q a2 b2 -> r (a1, a2) (b1, b2)
ProductOp p q r
prod p a b
p FreeCocartesian q a2 b2
qs') ((a, Either a1 a2) -> Either (a, a1) (a, a2)
forall c a b. (c, Either a b) -> Either (c, a) (c, b)
distR ((a, Either a1 a2) -> Either (a, a1) (a, a2))
-> ((a, a') -> (a, Either a1 a2))
-> (a, a')
-> Either (a, a1) (a, a2)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a' -> Either a1 a2) -> (a, a') -> (a, Either a1 a2)
forall b c a. (b -> c) -> (a, b) -> (a, c)
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second a' -> Either a1 a2
opA) ((Either b1 b2 -> b') -> (b, Either b1 b2) -> (b, b')
forall b c a. (b -> c) -> (a, b) -> (a, c)
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second Either b1 b2 -> b'
opB ((b, Either b1 b2) -> (b, b'))
-> (Either (b, b1) (b, b2) -> (b, Either b1 b2))
-> Either (b, b1) (b, b2)
-> (b, b')
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Either (b, b1) (b, b2) -> (b, Either b1 b2)
forall c a b. Either (c, a) (c, b) -> (c, Either a b)
undistR)