{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE FlexibleInstances #-}
module Data.Profunctor.Cocartesian.Free(
    -- * The free 'Cocartesian' profunctors
    FreeCocartesian(..),
    liftF, foldFree,
    emptyF, sumF,

    -- ** Distributive 'Cartesian' on @FreeCocartesian p@
    multF,

    -- * Newtype wrapper
    ForgetCocartesian(..),

    -- * Utility functions handling product @(,)@ and coproduct @Either@ of
    --   Haskell types

    assocEither, unassocEither,
    distL, undistL,
    distR, undistR
) 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 Cocartesian

-- | 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 'Data.Profunctor.Cartesian.Free.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
-- @
-- 
data FreeCocartesian p a b =
    Neutral (a -> Void)
  | Cons (Day Either p (FreeCocartesian p) a b)
  deriving (forall a b.
 (a -> b) -> FreeCocartesian p a a -> FreeCocartesian p a b)
-> (forall a b.
    a -> FreeCocartesian p a b -> FreeCocartesian p a a)
-> Functor (FreeCocartesian p a)
forall a b. a -> FreeCocartesian p a b -> FreeCocartesian p a a
forall a b.
(a -> b) -> FreeCocartesian p a a -> FreeCocartesian 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 -> FreeCocartesian p a b -> FreeCocartesian p a a
forall (p :: * -> * -> *) a a b.
(a -> b) -> FreeCocartesian p a a -> FreeCocartesian p a b
$cfmap :: forall (p :: * -> * -> *) a a b.
(a -> b) -> FreeCocartesian p a a -> FreeCocartesian p a b
fmap :: forall a b.
(a -> b) -> FreeCocartesian p a a -> FreeCocartesian p a b
$c<$ :: forall (p :: * -> * -> *) a a b.
a -> FreeCocartesian p a b -> FreeCocartesian p a a
<$ :: forall a b. a -> FreeCocartesian p a b -> FreeCocartesian p a a
Functor

instance Cartesian p => Applicative (FreeCocartesian p a) where
  pure :: forall a. a -> FreeCocartesian p a a
pure = a -> FreeCocartesian p a a
forall (p :: * -> * -> *) b a. Cartesian p => b -> p a b
pureDefault
  liftA2 :: forall a b c.
(a -> b -> c)
-> FreeCocartesian p a a
-> FreeCocartesian p a b
-> FreeCocartesian p a c
liftA2 = (a -> b -> c)
-> FreeCocartesian p a a
-> FreeCocartesian p a b
-> FreeCocartesian 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 Profunctor (FreeCocartesian p) where
    dimap :: forall a b c d.
(a -> b)
-> (c -> d) -> FreeCocartesian p b c -> FreeCocartesian p a d
dimap a -> b
f c -> d
g FreeCocartesian p b c
fp = case FreeCocartesian p b c
fp of
        Neutral b -> Void
a -> (a -> Void) -> FreeCocartesian p a d
forall (p :: * -> * -> *) a b. (a -> Void) -> FreeCocartesian p a b
Neutral (b -> Void
a (b -> Void) -> (a -> b) -> a -> Void
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> b
f)
        Cons Day Either p (FreeCocartesian p) b c
ps' -> Day Either p (FreeCocartesian p) a d -> FreeCocartesian p a d
forall (p :: * -> * -> *) a b.
Day Either p (FreeCocartesian p) a b -> FreeCocartesian p a b
Cons ((a -> b)
-> (c -> d)
-> Day Either p (FreeCocartesian p) b c
-> Day Either p (FreeCocartesian p) a d
forall a b c d.
(a -> b)
-> (c -> d)
-> Day Either p (FreeCocartesian p) b c
-> Day Either p (FreeCocartesian 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 Either p (FreeCocartesian p) b c
ps')

instance ProfunctorFunctor FreeCocartesian where
  promap :: forall (p :: * -> * -> *) (q :: * -> * -> *).
Profunctor p =>
(p :-> q) -> FreeCocartesian p :-> FreeCocartesian q
promap p :-> q
pq FreeCocartesian p a b
ps = case FreeCocartesian p a b
ps of
    Neutral a -> Void
a -> (a -> Void) -> FreeCocartesian q a b
forall (p :: * -> * -> *) a b. (a -> Void) -> FreeCocartesian p a b
Neutral a -> Void
a
    Cons (Day p a1 b1
p FreeCocartesian p a2 b2
ps' a -> Either a1 a2
opA Either b1 b2 -> b
opB) -> Day Either q (FreeCocartesian q) a b -> FreeCocartesian q a b
forall (p :: * -> * -> *) a b.
Day Either p (FreeCocartesian p) a b -> FreeCocartesian p a b
Cons (Day Either q (FreeCocartesian q) a b -> FreeCocartesian q a b)
-> Day Either q (FreeCocartesian q) a b -> FreeCocartesian q a b
forall a b. (a -> b) -> a -> b
$ q a1 b1
-> FreeCocartesian q a2 b2
-> (a -> Either a1 a2)
-> (Either b1 b2 -> b)
-> Day Either q (FreeCocartesian 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) -> FreeCocartesian p :-> FreeCocartesian 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) -> FreeCocartesian p :-> FreeCocartesian q
promap p a b -> q a b
p :-> q
pq FreeCocartesian p a2 b2
ps') a -> Either a1 a2
opA Either b1 b2 -> b
opB

emptyF :: FreeCocartesian p Void b
emptyF :: forall (p :: * -> * -> *) b. FreeCocartesian p Void b
emptyF = (Void -> Void) -> FreeCocartesian p Void b
forall (p :: * -> * -> *) a b. (a -> Void) -> FreeCocartesian p a b
Neutral Void -> Void
forall a. a -> a
id

sumF :: FreeCocartesian p a b -> FreeCocartesian p a' b' -> FreeCocartesian p (Either a a') (Either b b')
sumF :: forall (p :: * -> * -> *) a b a' b'.
FreeCocartesian p a b
-> FreeCocartesian p a' b'
-> FreeCocartesian p (Either a a') (Either b b')
sumF FreeCocartesian p a b
ps FreeCocartesian p a' b'
qs = case FreeCocartesian p a b
ps of
  Neutral a -> Void
z -> (Either a a' -> a')
-> (b' -> Either b b')
-> FreeCocartesian p a' b'
-> FreeCocartesian p (Either a a') (Either b b')
forall a b c d.
(a -> b)
-> (c -> d) -> FreeCocartesian p b c -> FreeCocartesian 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 FreeCocartesian p a2 b2
ps' a -> Either a1 a2
opA Either b1 b2 -> b
opB) ->
    Day Either p (FreeCocartesian p) (Either a a') (Either b b')
-> FreeCocartesian p (Either a a') (Either b b')
forall (p :: * -> * -> *) a b.
Day Either p (FreeCocartesian p) a b -> FreeCocartesian p a b
Cons (Day Either p (FreeCocartesian p) (Either a a') (Either b b')
 -> FreeCocartesian p (Either a a') (Either b b'))
-> Day Either p (FreeCocartesian p) (Either a a') (Either b b')
-> FreeCocartesian p (Either a a') (Either b b')
forall a b. (a -> b) -> a -> b
$ p a1 b1
-> FreeCocartesian 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 (FreeCocartesian p a2 b2
-> FreeCocartesian p a' b'
-> FreeCocartesian p (Either a2 a') (Either b2 b')
forall (p :: * -> * -> *) a b a' b'.
FreeCocartesian p a b
-> FreeCocartesian p a' b'
-> FreeCocartesian p (Either a a') (Either b b')
sumF FreeCocartesian p a2 b2
ps' 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)

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)

instance Profunctor p => Cocartesian (FreeCocartesian p) where
    proEmpty :: forall b. FreeCocartesian p Void b
proEmpty = FreeCocartesian p Void b
forall (p :: * -> * -> *) b. FreeCocartesian p Void b
emptyF
    +++ :: 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
-> FreeCocartesian p a' b'
-> FreeCocartesian p (Either a a') (Either b b')
forall (p :: * -> * -> *) a b a' b'.
FreeCocartesian p a b
-> FreeCocartesian p a' b'
-> FreeCocartesian p (Either a a') (Either b b')
sumF

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
liftF 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')
(***) = 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')
(***)

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
_    (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
emptyF
multF ProductOp p q r
prod (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
  = ((a, a') -> Either (a1, a') (a2, a'))
-> (Either (b1, b') (b2, b') -> (b, b'))
-> FreeCocartesian
     r (Either (a1, a') (a2, a')) (Either (b1, b') (b2, b'))
-> FreeCocartesian r (a, a') (b, b')
forall a b c d.
(a -> b)
-> (c -> d) -> FreeCocartesian r b c -> FreeCocartesian r 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) (FreeCocartesian
   r (Either (a1, a') (a2, a')) (Either (b1, b') (b2, b'))
 -> FreeCocartesian r (a, a') (b, b'))
-> FreeCocartesian
     r (Either (a1, a') (a2, a')) (Either (b1, b') (b2, 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')
-> FreeCocartesian
     r (Either (a1, a') (a2, a')) (Either (b1, b') (b2, b'))
forall (p :: * -> * -> *) a b a' b'.
FreeCocartesian p a b
-> FreeCocartesian p a' b'
-> FreeCocartesian p (Either a a') (Either b b')
sumF (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)

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
_ (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
emptyF
distLeftFree ProductOp p q r
prod p a b
p (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
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 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)

-- * ProfunctorMonad structures

liftF :: p :-> FreeCocartesian p
liftF :: forall (p :: * -> * -> *) a b. p a b -> FreeCocartesian p a b
liftF p a b
p = Day Either p (FreeCocartesian p) a b -> FreeCocartesian p a b
forall (p :: * -> * -> *) a b.
Day Either p (FreeCocartesian p) a b -> FreeCocartesian p a b
Cons (Day Either p (FreeCocartesian p) a b -> FreeCocartesian p a b)
-> Day Either p (FreeCocartesian p) a b -> FreeCocartesian p a b
forall a b. (a -> b) -> a -> b
$ p a b
-> FreeCocartesian p Void Void
-> (a -> Either a Void)
-> (Either b Void -> b)
-> Day Either p (FreeCocartesian 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 FreeCocartesian p Void Void
forall (p :: * -> * -> *) b. FreeCocartesian p Void b
emptyF 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)

foldFree :: (Cocartesian q) => (p :-> q) -> FreeCocartesian p :-> q
foldFree :: forall (q :: * -> * -> *) (p :: * -> * -> *).
Cocartesian q =>
(p :-> q) -> FreeCocartesian p :-> q
foldFree p :-> q
handle FreeCocartesian p a b
ps = case FreeCocartesian p a b
ps of
    Neutral a -> Void
z -> (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 FreeCocartesian 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) -> FreeCocartesian p :-> q
forall (q :: * -> * -> *) (p :: * -> * -> *).
Cocartesian q =>
(p :-> q) -> FreeCocartesian p :-> q
foldFree p a b -> q a b
p :-> q
handle FreeCocartesian p a2 b2
ps')

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
liftF
    projoin :: forall (p :: * -> * -> *).
Profunctor p =>
FreeCocartesian (FreeCocartesian p) :-> FreeCocartesian p
projoin = (FreeCocartesian p :-> FreeCocartesian p)
-> FreeCocartesian (FreeCocartesian p) :-> FreeCocartesian p
forall (q :: * -> * -> *) (p :: * -> * -> *).
Cocartesian q =>
(p :-> q) -> FreeCocartesian p :-> q
foldFree FreeCocartesian p a b -> FreeCocartesian p a b
forall a. a -> a
FreeCocartesian p :-> FreeCocartesian p
id

-- * Utility newtype wrappers

-- | 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!