{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE DataKinds #-}
module Data.Profunctor.Cartesian.Free(
    FreeMonoidal(..),

    FreeCartesian,
    liftFreeCartesian,
    foldFreeCartesian,

    FreeCocartesian,
    liftFreeCocartesian,
    foldFreeCocartesian,

    ForgetCartesian(..),
    ForgetCocartesian(..)
) where

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

-- * Free monoidal profunctor

-- | Constructs free monoidal profunctor with specified monoid. Each parameters of @FreeMonoidal t i p@ stands for:
--
-- - @t@ for the monoidal product
-- - @i@ for the unit of the monoidal product @t@
-- - @p@ for the profunctor generating @FreeMonoidal@
-- 
-- For example, @FreeMonoidal (,) () p@ is the free 'Cartesian' profunctor.
data FreeMonoidal t i p a b =
    Neutral (a -> i) (i -> b)
  | Cons (Day t p (FreeMonoidal t i p) a b)

deriving instance Functor (FreeMonoidal t i p a)


instance Profunctor (FreeMonoidal t i p) where
    dimap :: forall a b c d.
(a -> b)
-> (c -> d) -> FreeMonoidal t i p b c -> FreeMonoidal t i p a d
dimap a -> b
f c -> d
g FreeMonoidal t i p b c
fp = case FreeMonoidal t i p b c
fp of
        Neutral b -> i
a i -> c
b -> (a -> i) -> (i -> d) -> FreeMonoidal t i p a d
forall (t :: * -> * -> *) i (p :: * -> * -> *) a b.
(a -> i) -> (i -> b) -> FreeMonoidal t i p a b
Neutral (b -> i
a (b -> i) -> (a -> b) -> a -> i
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> b
f) (c -> d
g (c -> d) -> (i -> c) -> i -> d
forall b c a. (b -> c) -> (a -> b) -> a -> c
. i -> c
b)
        Cons Day t p (FreeMonoidal t i p) b c
ps' -> Day t p (FreeMonoidal t i p) a d -> FreeMonoidal t i p a d
forall (t :: * -> * -> *) i (p :: * -> * -> *) a b.
Day t p (FreeMonoidal t i p) a b -> FreeMonoidal t i p a b
Cons ((a -> b)
-> (c -> d)
-> Day t p (FreeMonoidal t i p) b c
-> Day t p (FreeMonoidal t i p) a d
forall a b c d.
(a -> b)
-> (c -> d)
-> Day t p (FreeMonoidal t i p) b c
-> Day t p (FreeMonoidal t i p) a d
forall (p :: * -> * -> *) a b c d.
Profunctor p =>
(a -> b) -> (c -> d) -> p b c -> p a d
dimap a -> b
f c -> d
g Day t p (FreeMonoidal t i p) b c
ps')

instance ProfunctorFunctor (FreeMonoidal t i) where
  promap :: forall (p :: * -> * -> *) (q :: * -> * -> *).
Profunctor p =>
(p :-> q) -> FreeMonoidal t i p :-> FreeMonoidal t i q
promap p :-> q
pq FreeMonoidal t i p a b
ps = case FreeMonoidal t i p a b
ps of
    Neutral a -> i
a i -> b
b -> (a -> i) -> (i -> b) -> FreeMonoidal t i q a b
forall (t :: * -> * -> *) i (p :: * -> * -> *) a b.
(a -> i) -> (i -> b) -> FreeMonoidal t i p a b
Neutral a -> i
a i -> b
b
    Cons (Day p a1 b1
p FreeMonoidal t i p a2 b2
ps' a -> t a1 a2
opA t b1 b2 -> b
opB) -> Day t q (FreeMonoidal t i q) a b -> FreeMonoidal t i q a b
forall (t :: * -> * -> *) i (p :: * -> * -> *) a b.
Day t p (FreeMonoidal t i p) a b -> FreeMonoidal t i p a b
Cons (Day t q (FreeMonoidal t i q) a b -> FreeMonoidal t i q a b)
-> Day t q (FreeMonoidal t i q) a b -> FreeMonoidal t i q a b
forall a b. (a -> b) -> a -> b
$ q a1 b1
-> FreeMonoidal t i q a2 b2
-> (a -> t a1 a2)
-> (t b1 b2 -> b)
-> Day t q (FreeMonoidal t i q) a 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 a1 b1 -> q a1 b1
p :-> q
pq p a1 b1
p) ((p :-> q) -> FreeMonoidal t i p :-> FreeMonoidal t i q
forall {k} {k1} (t :: (* -> * -> *) -> k -> k1 -> *)
       (p :: * -> * -> *) (q :: * -> * -> *).
(ProfunctorFunctor t, Profunctor p) =>
(p :-> q) -> t p :-> t q
forall (p :: * -> * -> *) (q :: * -> * -> *).
Profunctor p =>
(p :-> q) -> FreeMonoidal t i p :-> FreeMonoidal t i q
promap p a b -> q a b
p :-> q
pq FreeMonoidal t i p a2 b2
ps') a -> t a1 a2
opA t b1 b2 -> b
opB

-- * Free Cartesian

-- | Free Cartesian profunctor is 'FreeMonoidal' profunctor with respect to
--   @(,)@.
type FreeCartesian = FreeMonoidal (,) ()

instance Cartesian (FreeCartesian p) where
    proUnit :: forall a. FreeCartesian p a ()
proUnit = (a -> ()) -> (() -> ()) -> FreeMonoidal (,) () p a ()
forall (t :: * -> * -> *) i (p :: * -> * -> *) a b.
(a -> i) -> (i -> b) -> FreeMonoidal t i p a b
Neutral (() -> a -> ()
forall a b. a -> b -> a
const ()) () -> ()
forall a. a -> a
id
    Neutral a -> ()
_ () -> b
b *** :: forall a b a' b'.
FreeCartesian p a b
-> FreeCartesian p a' b' -> FreeCartesian p (a, a') (b, b')
*** FreeCartesian p a' b'
qs = ((a, a') -> a')
-> (b' -> (b, b'))
-> FreeCartesian p a' b'
-> FreeMonoidal (,) () p (a, a') (b, b')
forall a b c d.
(a -> b)
-> (c -> d)
-> FreeMonoidal (,) () p b c
-> FreeMonoidal (,) () p a d
forall (p :: * -> * -> *) a b c d.
Profunctor p =>
(a -> b) -> (c -> d) -> p b c -> p a d
dimap (a, a') -> a'
forall a b. (a, b) -> b
snd (() -> b
b (),) FreeCartesian p a' b'
qs
    Cons (Day p a1 b1
p FreeMonoidal (,) () p a2 b2
ps a -> (a1, a2)
opA (b1, b2) -> b
opB) *** FreeCartesian p a' b'
qs = Day (,) p (FreeCartesian p) (a, a') (b, b')
-> FreeMonoidal (,) () p (a, a') (b, b')
forall (t :: * -> * -> *) i (p :: * -> * -> *) a b.
Day t p (FreeMonoidal t i p) a b -> FreeMonoidal t i p a b
Cons (Day (,) p (FreeCartesian p) (a, a') (b, b')
 -> FreeMonoidal (,) () p (a, a') (b, b'))
-> Day (,) p (FreeCartesian p) (a, a') (b, b')
-> FreeMonoidal (,) () p (a, a') (b, b')
forall a b. (a -> b) -> a -> b
$ p a1 b1
-> FreeMonoidal (,) () p (a2, a') (b2, b')
-> ((a, a') -> (a1, (a2, a')))
-> ((b1, (b2, b')) -> (b, b'))
-> Day (,) p (FreeCartesian p) (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 a1 b1
p (FreeMonoidal (,) () p a2 b2
ps FreeMonoidal (,) () p a2 b2
-> FreeCartesian p a' b' -> FreeMonoidal (,) () p (a2, a') (b2, b')
forall a b a' b'.
FreeCartesian p a b
-> FreeCartesian p a' b' -> FreeCartesian p (a, a') (b, b')
forall (p :: * -> * -> *) a b a' b'.
Cartesian p =>
p a b -> p a' b' -> p (a, a') (b, b')
*** FreeCartesian p a' b'
qs) (((a1, a2), a') -> (a1, (a2, a'))
forall a b c. ((a, b), c) -> (a, (b, c))
assocTup (((a1, a2), a') -> (a1, (a2, a')))
-> ((a, a') -> ((a1, a2), a')) -> (a, a') -> (a1, (a2, a'))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> (a1, a2)) -> (a, a') -> ((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 -> (a1, a2)
opA) (((b1, b2) -> b) -> ((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 (b1, b2) -> b
opB (((b1, b2), b') -> (b, b'))
-> ((b1, (b2, b')) -> ((b1, b2), b')) -> (b1, (b2, b')) -> (b, b')
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (b1, (b2, b')) -> ((b1, b2), b')
forall a b c. (a, (b, c)) -> ((a, b), c)
unassocTup)

assocTup :: ((a,b), c) -> (a, (b,c))
assocTup :: forall a b c. ((a, b), c) -> (a, (b, c))
assocTup ((a
a,b
b), c
c) = (a
a, (b
b,c
c))

unassocTup :: (a, (b,c)) ->  ((a,b), c)
unassocTup :: forall a b c. (a, (b, c)) -> ((a, b), c)
unassocTup (a
a, (b
b,c
c)) = ((a
a,b
b), c
c)

liftFreeCartesian :: p :-> FreeCartesian p
liftFreeCartesian :: forall (p :: * -> * -> *) a b. p a b -> FreeCartesian p a b
liftFreeCartesian p a b
p = Day (,) p (FreeMonoidal (,) () p) a b -> FreeMonoidal (,) () p a b
forall (t :: * -> * -> *) i (p :: * -> * -> *) a b.
Day t p (FreeMonoidal t i p) a b -> FreeMonoidal t i p a b
Cons (Day (,) p (FreeMonoidal (,) () p) a b
 -> FreeMonoidal (,) () p a b)
-> Day (,) p (FreeMonoidal (,) () p) a b
-> FreeMonoidal (,) () p a b
forall a b. (a -> b) -> a -> b
$ p a b
-> FreeMonoidal (,) () p () ()
-> (a -> (a, ()))
-> ((b, ()) -> b)
-> Day (,) p (FreeMonoidal (,) () p) a 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
p FreeMonoidal (,) () p () ()
forall a. FreeMonoidal (,) () p a ()
forall (p :: * -> * -> *) a. Cartesian p => p a ()
proUnit (, ()) (b, ()) -> b
forall a b. (a, b) -> a
fst

foldFreeCartesian :: Cartesian q => (p :-> q) -> FreeCartesian p :-> q
foldFreeCartesian :: forall (q :: * -> * -> *) (p :: * -> * -> *).
Cartesian q =>
(p :-> q) -> FreeCartesian p :-> q
foldFreeCartesian p :-> q
_ (Neutral a -> ()
_ () -> b
b) = (() -> b) -> q a () -> q a b
forall b c a. (b -> c) -> q a b -> q a c
forall (p :: * -> * -> *) b c a.
Profunctor p =>
(b -> c) -> p a b -> p a c
rmap () -> b
b q a ()
forall a. q a ()
forall (p :: * -> * -> *) a. Cartesian p => p a ()
proUnit
foldFreeCartesian p :-> q
handle (Cons Day (,) p (FreeMonoidal (,) () p) a b
ps) = (p :-> q)
-> (FreeMonoidal (,) () p :-> q)
-> Day (,) p (FreeMonoidal (,) () p) :-> q
forall (r :: * -> * -> *) (p :: * -> * -> *) (q :: * -> * -> *).
Cartesian r =>
(p :-> r) -> (q :-> r) -> Day (,) p q :-> r
prodDay p a b -> q a b
p :-> q
handle ((p :-> q) -> FreeMonoidal (,) () p :-> q
forall (q :: * -> * -> *) (p :: * -> * -> *).
Cartesian q =>
(p :-> q) -> FreeCartesian p :-> q
foldFreeCartesian p a b -> q a b
p :-> q
handle) Day (,) p (FreeMonoidal (,) () p) a b
ps

instance ProfunctorMonad FreeCartesian where
  proreturn :: forall (p :: * -> * -> *). Profunctor p => p :-> FreeCartesian p
proreturn = p a b -> FreeCartesian p a b
forall (p :: * -> * -> *) a b. p a b -> FreeCartesian p a b
liftFreeCartesian
  projoin :: forall (p :: * -> * -> *).
Profunctor p =>
FreeCartesian (FreeCartesian p) :-> FreeCartesian p
projoin = (FreeMonoidal (,) () p :-> FreeMonoidal (,) () p)
-> FreeCartesian (FreeMonoidal (,) () p) :-> FreeMonoidal (,) () p
forall (q :: * -> * -> *) (p :: * -> * -> *).
Cartesian q =>
(p :-> q) -> FreeCartesian p :-> q
foldFreeCartesian FreeCartesian p a b -> FreeCartesian p a b
forall a. a -> a
FreeMonoidal (,) () p :-> FreeMonoidal (,) () p
id

-- * Free Cocartesian profunctor


-- | Free Cocartesian profunctor is 'FreeMonoidal' profunctor with respect to
--   @Either@.
-- 
-- ==== Caution about 'Cartesian' instance
-- 
-- Note that @'FreeCocartesian' p@ have an instance of 'Cartesian', by distributing
-- product on sums to sum of products of individual profunctors.
-- When it is desirable to disable @Cartesian@ instance of @FreeCocartesian p@,
-- use 'ForgetCartesian' to ignore @Cartesian@ instance of @p@.
--
-- Because there are some profunctors which are both @Cartesian@ and @Cocartesian@
-- but do not satisfy distributive laws,
-- using 'FreeCocartesian' with such profunctors might cause a surprising behavior.
--
-- For example, @'Data.Bifunctor.Joker.Joker' []@ is not distributive,
-- as @Alternative []@ is not distributive as shown below.
-- 
-- >>> 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 @Cartesian p@, 'foldFreeCocartesian' does not preserve
-- the @Cartesian@ operations. The following equation does not have to hold.
--
-- @
-- -- Not necessarily holds!
-- foldFreeCocartesian id (ps *** qs)
--  == foldFreeCocartesian id ps *** foldFreeCocartesian id qs
-- @
-- 
type FreeCocartesian = FreeMonoidal Either Void

instance Profunctor p => Cocartesian (FreeCocartesian p) where
    proEmpty :: forall b. FreeCocartesian p Void b
proEmpty = (Void -> Void) -> (Void -> b) -> FreeMonoidal Either Void p Void b
forall (t :: * -> * -> *) i (p :: * -> * -> *) a b.
(a -> i) -> (i -> b) -> FreeMonoidal t i p a b
Neutral Void -> Void
forall a. a -> a
id Void -> b
forall a. Void -> a
absurd
    Neutral a -> Void
z Void -> b
_ +++ :: forall a b a' b'.
FreeCocartesian p a b
-> FreeCocartesian p a' b'
-> FreeCocartesian p (Either a a') (Either b b')
+++ FreeCocartesian p a' b'
qs = (Either a a' -> a')
-> (b' -> Either b b')
-> FreeCocartesian p a' b'
-> FreeMonoidal Either Void p (Either a a') (Either b b')
forall a b c d.
(a -> b)
-> (c -> d)
-> FreeMonoidal Either Void p b c
-> FreeMonoidal Either Void p a d
forall (p :: * -> * -> *) a b c d.
Profunctor p =>
(a -> b) -> (c -> d) -> p b c -> p a d
dimap ((a -> a') -> (a' -> a') -> Either a a' -> a'
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (Void -> a'
forall a. Void -> a
absurd (Void -> a') -> (a -> Void) -> a -> a'
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Void
z) a' -> a'
forall a. a -> a
id) b' -> Either b b'
forall a b. b -> Either a b
Right FreeCocartesian p a' b'
qs
    Cons (Day p a1 b1
p FreeMonoidal Either Void p a2 b2
ps' a -> Either a1 a2
opA Either b1 b2 -> b
opB) +++ FreeCocartesian p a' b'
qs = Day Either p (FreeCocartesian p) (Either a a') (Either b b')
-> FreeMonoidal Either Void p (Either a a') (Either b b')
forall (t :: * -> * -> *) i (p :: * -> * -> *) a b.
Day t p (FreeMonoidal t i p) a b -> FreeMonoidal t i p a b
Cons (Day Either p (FreeCocartesian p) (Either a a') (Either b b')
 -> FreeMonoidal Either Void p (Either a a') (Either b b'))
-> Day Either p (FreeCocartesian p) (Either a a') (Either b b')
-> FreeMonoidal Either Void p (Either a a') (Either b b')
forall a b. (a -> b) -> a -> b
$ p a1 b1
-> FreeMonoidal Either Void p (Either a2 a') (Either b2 b')
-> (Either a a' -> Either a1 (Either a2 a'))
-> (Either b1 (Either b2 b') -> Either b b')
-> Day Either p (FreeCocartesian p) (Either a a') (Either 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 a1 b1
p (FreeMonoidal Either Void p a2 b2
ps' FreeMonoidal Either Void p a2 b2
-> FreeCocartesian p a' b'
-> FreeMonoidal Either Void p (Either a2 a') (Either b2 b')
forall a b a' b'.
FreeCocartesian p a b
-> FreeCocartesian p a' b'
-> FreeCocartesian p (Either a a') (Either b b')
forall (p :: * -> * -> *) a b a' b'.
Cocartesian p =>
p a b -> p a' b' -> p (Either a a') (Either b b')
+++ FreeCocartesian p a' b'
qs) (Either (Either a1 a2) a' -> Either a1 (Either a2 a')
forall a b c. Either (Either a b) c -> Either a (Either b c)
assocEither (Either (Either a1 a2) a' -> Either a1 (Either a2 a'))
-> (Either a a' -> Either (Either a1 a2) a')
-> Either a a'
-> Either a1 (Either a2 a')
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> Either a1 a2) -> Either a a' -> Either (Either a1 a2) a'
forall a b c. (a -> b) -> Either a c -> Either 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 (Either b1 b2) b' -> Either b b'
forall a b c. (a -> b) -> Either a c -> Either b c
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first Either b1 b2 -> b
opB (Either (Either b1 b2) b' -> Either b b')
-> (Either b1 (Either b2 b') -> Either (Either b1 b2) b')
-> Either b1 (Either b2 b')
-> Either b b'
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Either b1 (Either b2 b') -> Either (Either b1 b2) b'
forall a b c. Either a (Either b c) -> Either (Either a b) c
unassocEither)

instance Cartesian p => Cartesian (FreeCocartesian p) where
    proUnit :: forall a. FreeCocartesian p a ()
proUnit = p a () -> FreeCocartesian p a ()
forall (p :: * -> * -> *) a b. p a b -> FreeCocartesian p a b
liftFreeCocartesian p a ()
forall a. p a ()
forall (p :: * -> * -> *) a. Cartesian p => p a ()
proUnit
    *** :: forall a b a' b'.
FreeCocartesian p a b
-> FreeCocartesian p a' b' -> FreeCocartesian p (a, a') (b, b')
(***) = FreeCocartesian p a b
-> FreeCocartesian p a' b' -> FreeCocartesian p (a, a') (b, b')
forall (p :: * -> * -> *) a b a' b'.
Cartesian p =>
FreeCocartesian p a b
-> FreeCocartesian p a' b' -> FreeCocartesian p (a, a') (b, b')
multCocartesian

assocEither :: Either (Either a b) c -> Either a (Either b c)
assocEither :: forall a b c. Either (Either a b) c -> Either a (Either b c)
assocEither = (Either a b -> Either a (Either b c))
-> (c -> Either a (Either b c))
-> Either (Either a b) c
-> Either a (Either b c)
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either ((b -> Either b c) -> Either a b -> Either a (Either b c)
forall b c a. (b -> c) -> Either a b -> Either a c
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second b -> Either b c
forall a b. a -> Either a b
Left) (Either b c -> Either a (Either b c)
forall a b. b -> Either a b
Right (Either b c -> Either a (Either b c))
-> (c -> Either b c) -> c -> Either a (Either b c)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. c -> Either b c
forall a b. b -> Either a b
Right)

unassocEither :: Either a (Either b c) -> Either (Either a b) c
unassocEither :: forall a b c. Either a (Either b c) -> Either (Either a b) c
unassocEither = (a -> Either (Either a b) c)
-> (Either b c -> Either (Either a b) c)
-> Either a (Either b c)
-> Either (Either a b) c
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (Either a b -> Either (Either a b) c
forall a b. a -> Either a b
Left (Either a b -> Either (Either a b) c)
-> (a -> Either a b) -> a -> Either (Either a b) c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Either a b
forall a b. a -> Either a b
Left) ((b -> Either a b) -> Either b c -> Either (Either a b) c
forall a b c. (a -> b) -> Either a c -> Either b c
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first b -> Either a b
forall a b. b -> Either a b
Right)

liftFreeCocartesian :: p :-> FreeCocartesian p
liftFreeCocartesian :: forall (p :: * -> * -> *) a b. p a b -> FreeCocartesian p a b
liftFreeCocartesian p a b
p = Day Either p (FreeMonoidal Either Void p) a b
-> FreeMonoidal Either Void p a b
forall (t :: * -> * -> *) i (p :: * -> * -> *) a b.
Day t p (FreeMonoidal t i p) a b -> FreeMonoidal t i p a b
Cons (Day Either p (FreeMonoidal Either Void p) a b
 -> FreeMonoidal Either Void p a b)
-> Day Either p (FreeMonoidal Either Void p) a b
-> FreeMonoidal Either Void p a b
forall a b. (a -> b) -> a -> b
$ p a b
-> FreeMonoidal Either Void p Void Void
-> (a -> Either a Void)
-> (Either b Void -> b)
-> Day Either p (FreeMonoidal Either Void p) a 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
p ((Void -> Void)
-> (Void -> Void) -> FreeMonoidal Either Void p Void Void
forall (t :: * -> * -> *) i (p :: * -> * -> *) a b.
(a -> i) -> (i -> b) -> FreeMonoidal t i p a b
Neutral Void -> Void
forall a. a -> a
id Void -> Void
forall a. Void -> a
absurd) a -> Either a Void
forall a b. a -> Either a b
Left ((b -> b) -> (Void -> b) -> Either b Void -> b
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either b -> b
forall a. a -> a
id Void -> b
forall a. Void -> a
absurd)

foldFreeCocartesian :: (Cocartesian q) => (p :-> q) -> FreeCocartesian p :-> q
foldFreeCocartesian :: forall (q :: * -> * -> *) (p :: * -> * -> *).
Cocartesian q =>
(p :-> q) -> FreeCocartesian p :-> q
foldFreeCocartesian p :-> q
handle FreeCocartesian p a b
ps = case FreeCocartesian p a b
ps of
    Neutral a -> Void
z Void -> b
_ -> (a -> Void) -> q Void b -> q a b
forall a b c. (a -> b) -> q b c -> q a c
forall (p :: * -> * -> *) a b c.
Profunctor p =>
(a -> b) -> p b c -> p a c
lmap a -> Void
z q Void b
forall b. q Void b
forall (p :: * -> * -> *) b. Cocartesian p => p Void b
proEmpty
    Cons (Day p a1 b1
p FreeMonoidal Either Void p a2 b2
ps' a -> Either a1 a2
opA Either b1 b2 -> b
opB) -> (a -> Either a1 a2)
-> (Either b1 b2 -> b) -> q (Either a1 a2) (Either b1 b2) -> q a b
forall a b c d. (a -> b) -> (c -> d) -> q b c -> q a d
forall (p :: * -> * -> *) a b c d.
Profunctor p =>
(a -> b) -> (c -> d) -> p b c -> p a d
dimap a -> Either a1 a2
opA Either b1 b2 -> b
opB (p a1 b1 -> q a1 b1
p :-> q
handle p a1 b1
p q a1 b1 -> q a2 b2 -> q (Either a1 a2) (Either b1 b2)
forall a b a' b'. q a b -> q a' b' -> q (Either a a') (Either b b')
forall (p :: * -> * -> *) a b a' b'.
Cocartesian p =>
p a b -> p a' b' -> p (Either a a') (Either b b')
+++ (p :-> q) -> FreeMonoidal Either Void p :-> q
forall (q :: * -> * -> *) (p :: * -> * -> *).
Cocartesian q =>
(p :-> q) -> FreeCocartesian p :-> q
foldFreeCocartesian p a b -> q a b
p :-> q
handle FreeMonoidal Either Void p a2 b2
ps')

distLeftFree :: Cartesian p => p a b -> FreeCocartesian p a' b' -> FreeCocartesian p (a,a') (b,b')
distLeftFree :: forall (p :: * -> * -> *) a b a' b'.
Cartesian p =>
p a b
-> FreeCocartesian p a' b' -> FreeCocartesian p (a, a') (b, b')
distLeftFree p a b
_ (Neutral a' -> Void
z Void -> b'
_) = ((a, a') -> Void)
-> FreeMonoidal Either Void p Void (b, b')
-> FreeMonoidal Either Void p (a, a') (b, b')
forall a b c.
(a -> b)
-> FreeMonoidal Either Void p b c -> FreeMonoidal Either Void p 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) FreeMonoidal Either Void p Void (b, b')
forall b. FreeMonoidal Either Void p Void b
forall (p :: * -> * -> *) b. Cocartesian p => p Void b
proEmpty
distLeftFree p a b
p (Cons (Day p a1 b1
q FreeMonoidal Either Void p a2 b2
qs' a' -> Either a1 a2
opA Either b1 b2 -> b'
opB)) = Day Either p (FreeMonoidal Either Void p) (a, a') (b, b')
-> FreeMonoidal Either Void p (a, a') (b, b')
forall (t :: * -> * -> *) i (p :: * -> * -> *) a b.
Day t p (FreeMonoidal t i p) a b -> FreeMonoidal t i p a b
Cons (Day Either p (FreeMonoidal Either Void p) (a, a') (b, b')
 -> FreeMonoidal Either Void p (a, a') (b, b'))
-> Day Either p (FreeMonoidal Either Void p) (a, a') (b, b')
-> FreeMonoidal Either Void p (a, a') (b, b')
forall a b. (a -> b) -> a -> b
$ p (a, a1) (b, b1)
-> FreeMonoidal Either Void p (a, a2) (b, b2)
-> ((a, a') -> Either (a, a1) (a, a2))
-> (Either (b, b1) (b, b2) -> (b, b'))
-> Day Either p (FreeMonoidal Either Void p) (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
p p a b -> p a1 b1 -> p (a, a1) (b, b1)
forall a b a' b'. p a b -> p a' b' -> p (a, a') (b, b')
forall (p :: * -> * -> *) a b a' b'.
Cartesian p =>
p a b -> p a' b' -> p (a, a') (b, b')
*** p a1 b1
q) (p a b
-> FreeMonoidal Either Void p a2 b2
-> FreeMonoidal Either Void p (a, a2) (b, b2)
forall (p :: * -> * -> *) a b a' b'.
Cartesian p =>
p a b
-> FreeCocartesian p a' b' -> FreeCocartesian p (a, a') (b, b')
distLeftFree p a b
p FreeMonoidal Either Void p a2 b2
qs') ((a, Either a1 a2) -> Either (a, a1) (a, a2)
forall a b1 b2. (a, Either b1 b2) -> Either (a, b1) (a, b2)
distL ((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 a b1 b2. Either (a, b1) (a, b2) -> (a, Either b1 b2)
undistL)

distR :: (Either a1 a2, b) -> Either (a1, b) (a2, b)
distR :: forall a1 a2 b. (Either a1 a2, b) -> Either (a1, b) (a2, b)
distR (Either a1 a2
ea, b
b) = (a1 -> (a1, b))
-> (a2 -> (a2, b)) -> Either a1 a2 -> Either (a1, b) (a2, b)
forall a b c d. (a -> b) -> (c -> d) -> Either a c -> Either b d
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap (, b
b) (, b
b) Either a1 a2
ea

undistR :: Either (a1, b) (a2, b) -> (Either a1 a2, b)
undistR :: forall a1 b a2. Either (a1, b) (a2, b) -> (Either a1 a2, b)
undistR = ((a1, b) -> (Either a1 a2, b))
-> ((a2, b) -> (Either a1 a2, b))
-> Either (a1, b) (a2, b)
-> (Either a1 a2, b)
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either ((a1 -> Either a1 a2) -> (a1, b) -> (Either a1 a2, 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 a1 -> Either a1 a2
forall a b. a -> Either a b
Left) ((a2 -> Either a1 a2) -> (a2, b) -> (Either a1 a2, 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 a2 -> Either a1 a2
forall a b. b -> Either a b
Right)

distL :: (a, Either b1 b2) -> Either (a, b1) (a, b2)
distL :: forall a b1 b2. (a, Either b1 b2) -> Either (a, b1) (a, b2)
distL (a
a,Either b1 b2
b) = (b1 -> (a, b1))
-> (b2 -> (a, b2)) -> Either b1 b2 -> Either (a, b1) (a, b2)
forall a b c d. (a -> b) -> (c -> d) -> Either a c -> Either b d
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap (a
a,) (a
a,) Either b1 b2
b

undistL :: Either (a, b1) (a, b2) -> (a, Either b1 b2)
undistL :: forall a b1 b2. Either (a, b1) (a, b2) -> (a, Either b1 b2)
undistL = ((a, b1) -> (a, Either b1 b2))
-> ((a, b2) -> (a, Either b1 b2))
-> Either (a, b1) (a, b2)
-> (a, Either b1 b2)
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either ((b1 -> Either b1 b2) -> (a, b1) -> (a, Either b1 b2)
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 b1 -> Either b1 b2
forall a b. a -> Either a b
Left) ((b2 -> Either b1 b2) -> (a, b2) -> (a, Either b1 b2)
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 b2 -> Either b1 b2
forall a b. b -> Either a b
Right)

multCocartesian :: Cartesian p => FreeCocartesian p a b -> FreeCocartesian p a' b' -> FreeCocartesian p (a,a') (b,b')
multCocartesian :: forall (p :: * -> * -> *) a b a' b'.
Cartesian p =>
FreeCocartesian p a b
-> FreeCocartesian p a' b' -> FreeCocartesian p (a, a') (b, b')
multCocartesian (Neutral a -> Void
z Void -> b
_) FreeCocartesian p a' b'
_ = ((a, a') -> Void)
-> FreeMonoidal Either Void p Void (b, b')
-> FreeMonoidal Either Void p (a, a') (b, b')
forall a b c.
(a -> b)
-> FreeMonoidal Either Void p b c -> FreeMonoidal Either Void p 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) FreeMonoidal Either Void p Void (b, b')
forall b. FreeMonoidal Either Void p Void b
forall (p :: * -> * -> *) b. Cocartesian p => p Void b
proEmpty
multCocartesian (Cons (Day p a1 b1
p FreeMonoidal Either Void p a2 b2
ps' a -> Either a1 a2
opA Either b1 b2 -> b
opB)) FreeCocartesian p a' b'
qs = ((a, a') -> Either (a1, a') (a2, a'))
-> (Either (b1, b') (b2, b') -> (b, b'))
-> FreeMonoidal
     Either Void p (Either (a1, a') (a2, a')) (Either (b1, b') (b2, b'))
-> FreeMonoidal Either Void p (a, a') (b, b')
forall a b c d.
(a -> b)
-> (c -> d)
-> FreeMonoidal Either Void p b c
-> FreeMonoidal Either Void p a d
forall (p :: * -> * -> *) a b c d.
Profunctor p =>
(a -> b) -> (c -> d) -> p b c -> p a d
dimap ((Either a1 a2, a') -> Either (a1, a') (a2, a')
forall a1 a2 b. (Either a1 a2, b) -> Either (a1, b) (a2, b)
distR ((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 a1 b a2. Either (a1, b) (a2, b) -> (Either a1 a2, b)
undistR) (FreeMonoidal
   Either Void p (Either (a1, a') (a2, a')) (Either (b1, b') (b2, b'))
 -> FreeMonoidal Either Void p (a, a') (b, b'))
-> FreeMonoidal
     Either Void p (Either (a1, a') (a2, a')) (Either (b1, b') (b2, b'))
-> FreeMonoidal Either Void p (a, a') (b, b')
forall a b. (a -> b) -> a -> b
$ p a1 b1
-> FreeCocartesian p a' b' -> FreeCocartesian p (a1, a') (b1, b')
forall (p :: * -> * -> *) a b a' b'.
Cartesian p =>
p a b
-> FreeCocartesian p a' b' -> FreeCocartesian p (a, a') (b, b')
distLeftFree p a1 b1
p FreeCocartesian p a' b'
qs FreeCocartesian p (a1, a') (b1, b')
-> FreeMonoidal Either Void p (a2, a') (b2, b')
-> FreeMonoidal
     Either Void p (Either (a1, a') (a2, a')) (Either (b1, b') (b2, b'))
forall a b a' b'.
FreeMonoidal Either Void p a b
-> FreeMonoidal Either Void p a' b'
-> FreeMonoidal Either Void p (Either a a') (Either b b')
forall (p :: * -> * -> *) a b a' b'.
Cocartesian p =>
p a b -> p a' b' -> p (Either a a') (Either b b')
+++ (FreeMonoidal Either Void p a2 b2
ps' FreeMonoidal Either Void p a2 b2
-> FreeCocartesian p a' b'
-> FreeMonoidal Either Void p (a2, a') (b2, b')
forall a b a' b'.
FreeMonoidal Either Void p a b
-> FreeMonoidal Either Void p a' b'
-> FreeMonoidal Either Void p (a, a') (b, b')
forall (p :: * -> * -> *) a b a' b'.
Cartesian p =>
p a b -> p a' b' -> p (a, a') (b, b')
*** FreeCocartesian p a' b'
qs)

instance ProfunctorMonad FreeCocartesian where
    proreturn :: forall (p :: * -> * -> *). Profunctor p => p :-> FreeCocartesian p
proreturn = p a b -> FreeCocartesian p a b
forall (p :: * -> * -> *) a b. p a b -> FreeCocartesian p a b
liftFreeCocartesian
    projoin :: forall (p :: * -> * -> *).
Profunctor p =>
FreeCocartesian (FreeCocartesian p) :-> FreeCocartesian p
projoin = (FreeMonoidal Either Void p :-> FreeMonoidal Either Void p)
-> FreeCocartesian (FreeMonoidal Either Void p)
   :-> FreeMonoidal Either Void p
forall (q :: * -> * -> *) (p :: * -> * -> *).
Cocartesian q =>
(p :-> q) -> FreeCocartesian p :-> q
foldFreeCocartesian FreeCocartesian p a b -> FreeCocartesian p a b
forall a. a -> a
FreeMonoidal Either Void p :-> FreeMonoidal Either Void p
id

-- | Forgets 'Cartesian' instance from a 'Profunctor'.
newtype ForgetCartesian p a b = ForgetCartesian { forall (p :: * -> * -> *) a b. ForgetCartesian p a b -> p a b
recallCartesian :: p a b }
  deriving newtype ((forall a b.
 (a -> b) -> ForgetCartesian p a a -> ForgetCartesian p a b)
-> (forall a b.
    a -> ForgetCartesian p a b -> ForgetCartesian p a a)
-> Functor (ForgetCartesian p a)
forall a b. a -> ForgetCartesian p a b -> ForgetCartesian p a a
forall a b.
(a -> b) -> ForgetCartesian p a a -> ForgetCartesian 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.
Functor (p a) =>
a -> ForgetCartesian p a b -> ForgetCartesian p a a
forall (p :: * -> * -> *) a a b.
Functor (p a) =>
(a -> b) -> ForgetCartesian p a a -> ForgetCartesian p a b
$cfmap :: forall (p :: * -> * -> *) a a b.
Functor (p a) =>
(a -> b) -> ForgetCartesian p a a -> ForgetCartesian p a b
fmap :: forall a b.
(a -> b) -> ForgetCartesian p a a -> ForgetCartesian p a b
$c<$ :: forall (p :: * -> * -> *) a a b.
Functor (p a) =>
a -> ForgetCartesian p a b -> ForgetCartesian p a a
<$ :: forall a b. a -> ForgetCartesian p a b -> ForgetCartesian p a a
Functor, (forall a b c d.
 (a -> b)
 -> (c -> d) -> ForgetCartesian p b c -> ForgetCartesian p a d)
-> (forall a b c.
    (a -> b) -> ForgetCartesian p b c -> ForgetCartesian p a c)
-> (forall b c a.
    (b -> c) -> ForgetCartesian p a b -> ForgetCartesian p a c)
-> (forall a b c (q :: * -> * -> *).
    Coercible c b =>
    q b c -> ForgetCartesian p a b -> ForgetCartesian p a c)
-> (forall a b c (q :: * -> * -> *).
    Coercible b a =>
    ForgetCartesian p b c -> q a b -> ForgetCartesian p a c)
-> Profunctor (ForgetCartesian p)
forall a b c.
(a -> b) -> ForgetCartesian p b c -> ForgetCartesian p a c
forall b c a.
(b -> c) -> ForgetCartesian p a b -> ForgetCartesian p a c
forall a b c d.
(a -> b)
-> (c -> d) -> ForgetCartesian p b c -> ForgetCartesian p a d
forall a b c (q :: * -> * -> *).
Coercible b a =>
ForgetCartesian p b c -> q a b -> ForgetCartesian p a c
forall a b c (q :: * -> * -> *).
Coercible c b =>
q b c -> ForgetCartesian p a b -> ForgetCartesian p a c
forall (p :: * -> * -> *) a b c.
Profunctor p =>
(a -> b) -> ForgetCartesian p b c -> ForgetCartesian p a c
forall (p :: * -> * -> *) b c a.
Profunctor p =>
(b -> c) -> ForgetCartesian p a b -> ForgetCartesian p a c
forall (p :: * -> * -> *) a b c d.
Profunctor p =>
(a -> b)
-> (c -> d) -> ForgetCartesian p b c -> ForgetCartesian p a d
forall (p :: * -> * -> *) a b c (q :: * -> * -> *).
(Profunctor p, Coercible b a) =>
ForgetCartesian p b c -> q a b -> ForgetCartesian p a c
forall (p :: * -> * -> *) a b c (q :: * -> * -> *).
(Profunctor p, Coercible c b) =>
q b c -> ForgetCartesian p a b -> ForgetCartesian 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
$cdimap :: forall (p :: * -> * -> *) a b c d.
Profunctor p =>
(a -> b)
-> (c -> d) -> ForgetCartesian p b c -> ForgetCartesian p a d
dimap :: forall a b c d.
(a -> b)
-> (c -> d) -> ForgetCartesian p b c -> ForgetCartesian p a d
$clmap :: forall (p :: * -> * -> *) a b c.
Profunctor p =>
(a -> b) -> ForgetCartesian p b c -> ForgetCartesian p a c
lmap :: forall a b c.
(a -> b) -> ForgetCartesian p b c -> ForgetCartesian p a c
$crmap :: forall (p :: * -> * -> *) b c a.
Profunctor p =>
(b -> c) -> ForgetCartesian p a b -> ForgetCartesian p a c
rmap :: forall b c a.
(b -> c) -> ForgetCartesian p a b -> ForgetCartesian p a c
$c#. :: forall (p :: * -> * -> *) a b c (q :: * -> * -> *).
(Profunctor p, Coercible c b) =>
q b c -> ForgetCartesian p a b -> ForgetCartesian p a c
#. :: forall a b c (q :: * -> * -> *).
Coercible c b =>
q b c -> ForgetCartesian p a b -> ForgetCartesian p a c
$c.# :: forall (p :: * -> * -> *) a b c (q :: * -> * -> *).
(Profunctor p, Coercible b a) =>
ForgetCartesian p b c -> q a b -> ForgetCartesian p a c
.# :: forall a b c (q :: * -> * -> *).
Coercible b a =>
ForgetCartesian p b c -> q a b -> ForgetCartesian p a c
Profunctor, Profunctor (ForgetCartesian p)
Profunctor (ForgetCartesian p) =>
(forall b. ForgetCartesian p Void b)
-> (forall a a1 a2 b1 b2 b.
    (a -> Either a1 a2)
    -> (Either b1 b2 -> b)
    -> ForgetCartesian p a1 b1
    -> ForgetCartesian p a2 b2
    -> ForgetCartesian p a b)
-> (forall a b a' b'.
    ForgetCartesian p a b
    -> ForgetCartesian p a' b'
    -> ForgetCartesian p (Either a a') (Either b b'))
-> (forall a b a'.
    ForgetCartesian p a b
    -> ForgetCartesian p a' b -> ForgetCartesian p (Either a a') b)
-> (forall (n :: Nat) a b.
    KnownNat n =>
    ForgetCartesian p a b
    -> ForgetCartesian p (Finite n, a) (Finite n, b))
-> Cocartesian (ForgetCartesian p)
forall (n :: Nat) a b.
KnownNat n =>
ForgetCartesian p a b
-> ForgetCartesian p (Finite n, a) (Finite n, b)
forall b. ForgetCartesian p Void b
forall a b a'.
ForgetCartesian p a b
-> ForgetCartesian p a' b -> ForgetCartesian p (Either a a') b
forall a b a' b'.
ForgetCartesian p a b
-> ForgetCartesian p a' b'
-> ForgetCartesian p (Either a a') (Either b b')
forall a a1 a2 b1 b2 b.
(a -> Either a1 a2)
-> (Either b1 b2 -> b)
-> ForgetCartesian p a1 b1
-> ForgetCartesian p a2 b2
-> ForgetCartesian p a b
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 :: * -> * -> *).
Cocartesian p =>
Profunctor (ForgetCartesian p)
forall (p :: * -> * -> *) (n :: Nat) a b.
(Cocartesian p, KnownNat n) =>
ForgetCartesian p a b
-> ForgetCartesian p (Finite n, a) (Finite n, b)
forall (p :: * -> * -> *) b.
Cocartesian p =>
ForgetCartesian p Void b
forall (p :: * -> * -> *) a b a'.
Cocartesian p =>
ForgetCartesian p a b
-> ForgetCartesian p a' b -> ForgetCartesian p (Either a a') b
forall (p :: * -> * -> *) a b a' b'.
Cocartesian p =>
ForgetCartesian p a b
-> ForgetCartesian p a' b'
-> ForgetCartesian p (Either a a') (Either b b')
forall (p :: * -> * -> *) a a1 a2 b1 b2 b.
Cocartesian p =>
(a -> Either a1 a2)
-> (Either b1 b2 -> b)
-> ForgetCartesian p a1 b1
-> ForgetCartesian p a2 b2
-> ForgetCartesian p a b
$cproEmpty :: forall (p :: * -> * -> *) b.
Cocartesian p =>
ForgetCartesian p Void b
proEmpty :: forall b. ForgetCartesian p Void b
$cproSum :: forall (p :: * -> * -> *) a a1 a2 b1 b2 b.
Cocartesian p =>
(a -> Either a1 a2)
-> (Either b1 b2 -> b)
-> ForgetCartesian p a1 b1
-> ForgetCartesian p a2 b2
-> ForgetCartesian p a b
proSum :: forall a a1 a2 b1 b2 b.
(a -> Either a1 a2)
-> (Either b1 b2 -> b)
-> ForgetCartesian p a1 b1
-> ForgetCartesian p a2 b2
-> ForgetCartesian p a b
$c+++ :: forall (p :: * -> * -> *) a b a' b'.
Cocartesian p =>
ForgetCartesian p a b
-> ForgetCartesian p a' b'
-> ForgetCartesian p (Either a a') (Either b b')
+++ :: forall a b a' b'.
ForgetCartesian p a b
-> ForgetCartesian p a' b'
-> ForgetCartesian p (Either a a') (Either b b')
$c||| :: forall (p :: * -> * -> *) a b a'.
Cocartesian p =>
ForgetCartesian p a b
-> ForgetCartesian p a' b -> ForgetCartesian p (Either a a') b
||| :: forall a b a'.
ForgetCartesian p a b
-> ForgetCartesian p a' b -> ForgetCartesian p (Either a a') b
$cproTimes :: forall (p :: * -> * -> *) (n :: Nat) a b.
(Cocartesian p, KnownNat n) =>
ForgetCartesian p a b
-> ForgetCartesian p (Finite n, a) (Finite n, b)
proTimes :: forall (n :: Nat) a b.
KnownNat n =>
ForgetCartesian p a b
-> ForgetCartesian p (Finite n, a) (Finite n, b)
Cocartesian)
  -- DO NOT add "deriving Cartesian" clause!

-- | Forgets 'Cocartesian' instance from a 'Profunctor'.
newtype ForgetCocartesian p a b = ForgetCocartesian { forall (p :: * -> * -> *) a b. ForgetCocartesian p a b -> p a b
recallCocartesian :: p a b }
  deriving newtype ((forall a b.
 (a -> b) -> ForgetCocartesian p a a -> ForgetCocartesian p a b)
-> (forall a b.
    a -> ForgetCocartesian p a b -> ForgetCocartesian p a a)
-> Functor (ForgetCocartesian p a)
forall a b. a -> ForgetCocartesian p a b -> ForgetCocartesian p a a
forall a b.
(a -> b) -> ForgetCocartesian p a a -> ForgetCocartesian 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.
Functor (p a) =>
a -> ForgetCocartesian p a b -> ForgetCocartesian p a a
forall (p :: * -> * -> *) a a b.
Functor (p a) =>
(a -> b) -> ForgetCocartesian p a a -> ForgetCocartesian p a b
$cfmap :: forall (p :: * -> * -> *) a a b.
Functor (p a) =>
(a -> b) -> ForgetCocartesian p a a -> ForgetCocartesian p a b
fmap :: forall a b.
(a -> b) -> ForgetCocartesian p a a -> ForgetCocartesian p a b
$c<$ :: forall (p :: * -> * -> *) a a b.
Functor (p a) =>
a -> ForgetCocartesian p a b -> ForgetCocartesian p a a
<$ :: forall a b. a -> ForgetCocartesian p a b -> ForgetCocartesian p a a
Functor, (forall a b c d.
 (a -> b)
 -> (c -> d) -> ForgetCocartesian p b c -> ForgetCocartesian p a d)
-> (forall a b c.
    (a -> b) -> ForgetCocartesian p b c -> ForgetCocartesian p a c)
-> (forall b c a.
    (b -> c) -> ForgetCocartesian p a b -> ForgetCocartesian p a c)
-> (forall a b c (q :: * -> * -> *).
    Coercible c b =>
    q b c -> ForgetCocartesian p a b -> ForgetCocartesian p a c)
-> (forall a b c (q :: * -> * -> *).
    Coercible b a =>
    ForgetCocartesian p b c -> q a b -> ForgetCocartesian p a c)
-> Profunctor (ForgetCocartesian p)
forall a b c.
(a -> b) -> ForgetCocartesian p b c -> ForgetCocartesian p a c
forall b c a.
(b -> c) -> ForgetCocartesian p a b -> ForgetCocartesian p a c
forall a b c d.
(a -> b)
-> (c -> d) -> ForgetCocartesian p b c -> ForgetCocartesian p a d
forall a b c (q :: * -> * -> *).
Coercible b a =>
ForgetCocartesian p b c -> q a b -> ForgetCocartesian p a c
forall a b c (q :: * -> * -> *).
Coercible c b =>
q b c -> ForgetCocartesian p a b -> ForgetCocartesian p a c
forall (p :: * -> * -> *) a b c.
Profunctor p =>
(a -> b) -> ForgetCocartesian p b c -> ForgetCocartesian p a c
forall (p :: * -> * -> *) b c a.
Profunctor p =>
(b -> c) -> ForgetCocartesian p a b -> ForgetCocartesian p a c
forall (p :: * -> * -> *) a b c d.
Profunctor p =>
(a -> b)
-> (c -> d) -> ForgetCocartesian p b c -> ForgetCocartesian p a d
forall (p :: * -> * -> *) a b c (q :: * -> * -> *).
(Profunctor p, Coercible b a) =>
ForgetCocartesian p b c -> q a b -> ForgetCocartesian p a c
forall (p :: * -> * -> *) a b c (q :: * -> * -> *).
(Profunctor p, Coercible c b) =>
q b c -> ForgetCocartesian p a b -> ForgetCocartesian 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
$cdimap :: forall (p :: * -> * -> *) a b c d.
Profunctor p =>
(a -> b)
-> (c -> d) -> ForgetCocartesian p b c -> ForgetCocartesian p a d
dimap :: forall a b c d.
(a -> b)
-> (c -> d) -> ForgetCocartesian p b c -> ForgetCocartesian p a d
$clmap :: forall (p :: * -> * -> *) a b c.
Profunctor p =>
(a -> b) -> ForgetCocartesian p b c -> ForgetCocartesian p a c
lmap :: forall a b c.
(a -> b) -> ForgetCocartesian p b c -> ForgetCocartesian p a c
$crmap :: forall (p :: * -> * -> *) b c a.
Profunctor p =>
(b -> c) -> ForgetCocartesian p a b -> ForgetCocartesian p a c
rmap :: forall b c a.
(b -> c) -> ForgetCocartesian p a b -> ForgetCocartesian p a c
$c#. :: forall (p :: * -> * -> *) a b c (q :: * -> * -> *).
(Profunctor p, Coercible c b) =>
q b c -> ForgetCocartesian p a b -> ForgetCocartesian p a c
#. :: forall a b c (q :: * -> * -> *).
Coercible c b =>
q b c -> ForgetCocartesian p a b -> ForgetCocartesian p a c
$c.# :: forall (p :: * -> * -> *) a b c (q :: * -> * -> *).
(Profunctor p, Coercible b a) =>
ForgetCocartesian p b c -> q a b -> ForgetCocartesian p a c
.# :: forall a b c (q :: * -> * -> *).
Coercible b a =>
ForgetCocartesian p b c -> q a b -> ForgetCocartesian p a c
Profunctor, Profunctor (ForgetCocartesian p)
Profunctor (ForgetCocartesian p) =>
(forall a. ForgetCocartesian p a ())
-> (forall a a1 a2 b1 b2 b.
    (a -> (a1, a2))
    -> ((b1, b2) -> b)
    -> ForgetCocartesian p a1 b1
    -> ForgetCocartesian p a2 b2
    -> ForgetCocartesian p a b)
-> (forall a b a' b'.
    ForgetCocartesian p a b
    -> ForgetCocartesian p a' b'
    -> ForgetCocartesian p (a, a') (b, b'))
-> (forall a b b'.
    ForgetCocartesian p a b
    -> ForgetCocartesian p a b' -> ForgetCocartesian p a (b, b'))
-> (forall (n :: Nat) a b.
    KnownNat n =>
    ForgetCocartesian p a b
    -> ForgetCocartesian p (Finite n -> a) (Finite n -> b))
-> Cartesian (ForgetCocartesian p)
forall (n :: Nat) a b.
KnownNat n =>
ForgetCocartesian p a b
-> ForgetCocartesian p (Finite n -> a) (Finite n -> b)
forall a. ForgetCocartesian p a ()
forall a b b'.
ForgetCocartesian p a b
-> ForgetCocartesian p a b' -> ForgetCocartesian p a (b, b')
forall a b a' b'.
ForgetCocartesian p a b
-> ForgetCocartesian p a' b' -> ForgetCocartesian p (a, a') (b, b')
forall a a1 a2 b1 b2 b.
(a -> (a1, a2))
-> ((b1, b2) -> b)
-> ForgetCocartesian p a1 b1
-> ForgetCocartesian p a2 b2
-> ForgetCocartesian p a b
forall (p :: * -> * -> *).
Profunctor p =>
(forall a. p a ())
-> (forall a a1 a2 b1 b2 b.
    (a -> (a1, a2)) -> ((b1, b2) -> b) -> p a1 b1 -> p a2 b2 -> p a b)
-> (forall a b a' b'. p a b -> p a' b' -> p (a, a') (b, b'))
-> (forall a b b'. p a b -> p a b' -> p a (b, b'))
-> (forall (n :: Nat) a b.
    KnownNat n =>
    p a b -> p (Finite n -> a) (Finite n -> b))
-> Cartesian p
forall (p :: * -> * -> *).
Cartesian p =>
Profunctor (ForgetCocartesian p)
forall (p :: * -> * -> *) (n :: Nat) a b.
(Cartesian p, KnownNat n) =>
ForgetCocartesian p a b
-> ForgetCocartesian p (Finite n -> a) (Finite n -> b)
forall (p :: * -> * -> *) a.
Cartesian p =>
ForgetCocartesian p a ()
forall (p :: * -> * -> *) a b b'.
Cartesian p =>
ForgetCocartesian p a b
-> ForgetCocartesian p a b' -> ForgetCocartesian p a (b, b')
forall (p :: * -> * -> *) a b a' b'.
Cartesian p =>
ForgetCocartesian p a b
-> ForgetCocartesian p a' b' -> ForgetCocartesian p (a, a') (b, b')
forall (p :: * -> * -> *) a a1 a2 b1 b2 b.
Cartesian p =>
(a -> (a1, a2))
-> ((b1, b2) -> b)
-> ForgetCocartesian p a1 b1
-> ForgetCocartesian p a2 b2
-> ForgetCocartesian p a b
$cproUnit :: forall (p :: * -> * -> *) a.
Cartesian p =>
ForgetCocartesian p a ()
proUnit :: forall a. ForgetCocartesian p a ()
$cproProduct :: forall (p :: * -> * -> *) a a1 a2 b1 b2 b.
Cartesian p =>
(a -> (a1, a2))
-> ((b1, b2) -> b)
-> ForgetCocartesian p a1 b1
-> ForgetCocartesian p a2 b2
-> ForgetCocartesian p a b
proProduct :: forall a a1 a2 b1 b2 b.
(a -> (a1, a2))
-> ((b1, b2) -> b)
-> ForgetCocartesian p a1 b1
-> ForgetCocartesian p a2 b2
-> ForgetCocartesian p a b
$c*** :: forall (p :: * -> * -> *) a b a' b'.
Cartesian p =>
ForgetCocartesian p a b
-> ForgetCocartesian p a' b' -> ForgetCocartesian p (a, a') (b, b')
*** :: forall a b a' b'.
ForgetCocartesian p a b
-> ForgetCocartesian p a' b' -> ForgetCocartesian p (a, a') (b, b')
$c&&& :: forall (p :: * -> * -> *) a b b'.
Cartesian p =>
ForgetCocartesian p a b
-> ForgetCocartesian p a b' -> ForgetCocartesian p a (b, b')
&&& :: forall a b b'.
ForgetCocartesian p a b
-> ForgetCocartesian p a b' -> ForgetCocartesian p a (b, b')
$cproPower :: forall (p :: * -> * -> *) (n :: Nat) a b.
(Cartesian p, KnownNat n) =>
ForgetCocartesian p a b
-> ForgetCocartesian p (Finite n -> a) (Finite n -> b)
proPower :: forall (n :: Nat) a b.
KnownNat n =>
ForgetCocartesian p a b
-> ForgetCocartesian p (Finite n -> a) (Finite n -> b)
Cartesian)
  -- DO NOT add "deriving Cocartesian" clause!