{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE BlockArguments #-}
{-# LANGUAGE DataKinds #-}
module Data.Profunctor.Cartesian.FreeBicartesian(
  FreeBicartesian(..),
  liftFreeBicartesian,
  foldFreeBicartesian,

  FreeBicartesianD(..),
  liftFreeBicartesianD,
  foldFreeBicartesianD
) where

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

import Data.Profunctor.Cartesian.Free

-- * Free bicartesian, no assumed distributivity

newtype FreeBicartesian p a b = FreeBicartesian {
    forall (p :: * -> * -> *) a b.
FreeBicartesian p a b
-> forall (q :: * -> * -> *).
   (Cartesian q, Cocartesian q) =>
   (p :-> q) -> q a b
runFreeBicartesian :: forall q. (Cartesian q, Cocartesian q) => (p :-> q) -> q a b
  }

instance Functor (FreeBicartesian p a) where
  fmap :: forall a b.
(a -> b) -> FreeBicartesian p a a -> FreeBicartesian p a b
fmap = (a -> b) -> FreeBicartesian p a a -> FreeBicartesian p a b
forall b c a.
(b -> c) -> FreeBicartesian p a b -> FreeBicartesian p a c
forall (p :: * -> * -> *) b c a.
Profunctor p =>
(b -> c) -> p a b -> p a c
rmap

instance Profunctor (FreeBicartesian p) where
  dimap :: forall a b c d.
(a -> b)
-> (c -> d) -> FreeBicartesian p b c -> FreeBicartesian p a d
dimap a -> b
f c -> d
g (FreeBicartesian forall (q :: * -> * -> *).
(Cartesian q, Cocartesian q) =>
(p :-> q) -> q b c
fp) = (forall (q :: * -> * -> *).
 (Cartesian q, Cocartesian q) =>
 (p :-> q) -> q a d)
-> FreeBicartesian p a d
forall (p :: * -> * -> *) a b.
(forall (q :: * -> * -> *).
 (Cartesian q, Cocartesian q) =>
 (p :-> q) -> q a b)
-> FreeBicartesian p a b
FreeBicartesian ((forall (q :: * -> * -> *).
  (Cartesian q, Cocartesian q) =>
  (p :-> q) -> q a d)
 -> FreeBicartesian p a d)
-> (forall (q :: * -> * -> *).
    (Cartesian q, Cocartesian q) =>
    (p :-> q) -> q a d)
-> FreeBicartesian p a d
forall a b. (a -> b) -> a -> b
$ \p :-> q
ret -> (a -> b) -> (c -> d) -> q b c -> q a d
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 -> b
f c -> d
g ((p :-> q) -> q b c
forall (q :: * -> * -> *).
(Cartesian q, Cocartesian q) =>
(p :-> q) -> q b c
fp p a b -> q a b
p :-> q
ret)
  lmap :: forall a b c.
(a -> b) -> FreeBicartesian p b c -> FreeBicartesian p a c
lmap a -> b
f (FreeBicartesian forall (q :: * -> * -> *).
(Cartesian q, Cocartesian q) =>
(p :-> q) -> q b c
fp) = (forall (q :: * -> * -> *).
 (Cartesian q, Cocartesian q) =>
 (p :-> q) -> q a c)
-> FreeBicartesian p a c
forall (p :: * -> * -> *) a b.
(forall (q :: * -> * -> *).
 (Cartesian q, Cocartesian q) =>
 (p :-> q) -> q a b)
-> FreeBicartesian p a b
FreeBicartesian ((forall (q :: * -> * -> *).
  (Cartesian q, Cocartesian q) =>
  (p :-> q) -> q a c)
 -> FreeBicartesian p a c)
-> (forall (q :: * -> * -> *).
    (Cartesian q, Cocartesian q) =>
    (p :-> q) -> q a c)
-> FreeBicartesian p a c
forall a b. (a -> b) -> a -> b
$ \p :-> q
ret -> (a -> b) -> q b c -> q a c
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 -> b
f ((p :-> q) -> q b c
forall (q :: * -> * -> *).
(Cartesian q, Cocartesian q) =>
(p :-> q) -> q b c
fp p a b -> q a b
p :-> q
ret)
  rmap :: forall b c a.
(b -> c) -> FreeBicartesian p a b -> FreeBicartesian p a c
rmap b -> c
g (FreeBicartesian forall (q :: * -> * -> *).
(Cartesian q, Cocartesian q) =>
(p :-> q) -> q a b
fp) = (forall (q :: * -> * -> *).
 (Cartesian q, Cocartesian q) =>
 (p :-> q) -> q a c)
-> FreeBicartesian p a c
forall (p :: * -> * -> *) a b.
(forall (q :: * -> * -> *).
 (Cartesian q, Cocartesian q) =>
 (p :-> q) -> q a b)
-> FreeBicartesian p a b
FreeBicartesian ((forall (q :: * -> * -> *).
  (Cartesian q, Cocartesian q) =>
  (p :-> q) -> q a c)
 -> FreeBicartesian p a c)
-> (forall (q :: * -> * -> *).
    (Cartesian q, Cocartesian q) =>
    (p :-> q) -> q a c)
-> FreeBicartesian p a c
forall a b. (a -> b) -> a -> b
$ \p :-> q
ret -> (b -> c) -> q a b -> q a c
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 -> c
g ((p :-> q) -> q a b
forall (q :: * -> * -> *).
(Cartesian q, Cocartesian q) =>
(p :-> q) -> q a b
fp p a b -> q a b
p :-> q
ret)


instance Cartesian (FreeBicartesian p) where
  proUnit :: forall a. FreeBicartesian p a ()
proUnit = (forall (q :: * -> * -> *).
 (Cartesian q, Cocartesian q) =>
 (p :-> q) -> q a ())
-> FreeBicartesian p a ()
forall (p :: * -> * -> *) a b.
(forall (q :: * -> * -> *).
 (Cartesian q, Cocartesian q) =>
 (p :-> q) -> q a b)
-> FreeBicartesian p a b
FreeBicartesian (q a () -> (p Any Any -> q Any Any) -> q a ()
forall a b. a -> b -> a
const q a ()
forall a. q a ()
forall (p :: * -> * -> *) a. Cartesian p => p a ()
proUnit)
  FreeBicartesian forall (q :: * -> * -> *).
(Cartesian q, Cocartesian q) =>
(p :-> q) -> q a b
fp1 *** :: forall a b a' b'.
FreeBicartesian p a b
-> FreeBicartesian p a' b' -> FreeBicartesian p (a, a') (b, b')
*** FreeBicartesian forall (q :: * -> * -> *).
(Cartesian q, Cocartesian q) =>
(p :-> q) -> q a' b'
fp2
    = (forall (q :: * -> * -> *).
 (Cartesian q, Cocartesian q) =>
 (p :-> q) -> q (a, a') (b, b'))
-> FreeBicartesian p (a, a') (b, b')
forall (p :: * -> * -> *) a b.
(forall (q :: * -> * -> *).
 (Cartesian q, Cocartesian q) =>
 (p :-> q) -> q a b)
-> FreeBicartesian p a b
FreeBicartesian \p :-> q
ret -> (p :-> q) -> q a b
forall (q :: * -> * -> *).
(Cartesian q, Cocartesian q) =>
(p :-> q) -> q a b
fp1 p a b -> q a b
p :-> q
ret q a b -> q a' b' -> q (a, a') (b, b')
forall a b a' b'. q a b -> q a' b' -> q (a, a') (b, b')
forall (p :: * -> * -> *) a b a' b'.
Cartesian p =>
p a b -> p a' b' -> p (a, a') (b, b')
*** (p :-> q) -> q a' b'
forall (q :: * -> * -> *).
(Cartesian q, Cocartesian q) =>
(p :-> q) -> q a' b'
fp2 p a b -> q a b
p :-> q
ret

instance Cocartesian (FreeBicartesian p) where
  proEmpty :: forall b. FreeBicartesian p Void b
proEmpty = (forall (q :: * -> * -> *).
 (Cartesian q, Cocartesian q) =>
 (p :-> q) -> q Void b)
-> FreeBicartesian p Void b
forall (p :: * -> * -> *) a b.
(forall (q :: * -> * -> *).
 (Cartesian q, Cocartesian q) =>
 (p :-> q) -> q a b)
-> FreeBicartesian p a b
FreeBicartesian (q Void b -> (p Any Any -> q Any Any) -> q Void b
forall a b. a -> b -> a
const q Void b
forall b. q Void b
forall (p :: * -> * -> *) b. Cocartesian p => p Void b
proEmpty)
  FreeBicartesian forall (q :: * -> * -> *).
(Cartesian q, Cocartesian q) =>
(p :-> q) -> q a b
fp1 +++ :: forall a b a' b'.
FreeBicartesian p a b
-> FreeBicartesian p a' b'
-> FreeBicartesian p (Either a a') (Either b b')
+++ FreeBicartesian forall (q :: * -> * -> *).
(Cartesian q, Cocartesian q) =>
(p :-> q) -> q a' b'
fp2
    = (forall (q :: * -> * -> *).
 (Cartesian q, Cocartesian q) =>
 (p :-> q) -> q (Either a a') (Either b b'))
-> FreeBicartesian p (Either a a') (Either b b')
forall (p :: * -> * -> *) a b.
(forall (q :: * -> * -> *).
 (Cartesian q, Cocartesian q) =>
 (p :-> q) -> q a b)
-> FreeBicartesian p a b
FreeBicartesian \p :-> q
ret -> (p :-> q) -> q a b
forall (q :: * -> * -> *).
(Cartesian q, Cocartesian q) =>
(p :-> q) -> q a b
fp1 p a b -> q a b
p :-> q
ret q a b -> q a' b' -> q (Either a a') (Either b b')
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) -> q a' b'
forall (q :: * -> * -> *).
(Cartesian q, Cocartesian q) =>
(p :-> q) -> q a' b'
fp2 p a b -> q a b
p :-> q
ret

liftFreeBicartesian :: p :-> FreeBicartesian p
liftFreeBicartesian :: forall (p :: * -> * -> *) a b. p a b -> FreeBicartesian p a b
liftFreeBicartesian p a b
p = (forall (q :: * -> * -> *).
 (Cartesian q, Cocartesian q) =>
 (p :-> q) -> q a b)
-> FreeBicartesian p a b
forall (p :: * -> * -> *) a b.
(forall (q :: * -> * -> *).
 (Cartesian q, Cocartesian q) =>
 (p :-> q) -> q a b)
-> FreeBicartesian p a b
FreeBicartesian \p :-> q
ret -> p a b -> q a b
p :-> q
ret p a b
p

foldFreeBicartesian :: (Cartesian q, Cocartesian q) => (p :-> q) -> FreeBicartesian p :-> q
foldFreeBicartesian :: forall (q :: * -> * -> *) (p :: * -> * -> *).
(Cartesian q, Cocartesian q) =>
(p :-> q) -> FreeBicartesian p :-> q
foldFreeBicartesian p :-> q
pq FreeBicartesian p a b
fp = FreeBicartesian p a b
-> forall (q :: * -> * -> *).
   (Cartesian q, Cocartesian q) =>
   (p :-> q) -> q a b
forall (p :: * -> * -> *) a b.
FreeBicartesian p a b
-> forall (q :: * -> * -> *).
   (Cartesian q, Cocartesian q) =>
   (p :-> q) -> q a b
runFreeBicartesian FreeBicartesian p a b
fp p a b -> q a b
p :-> q
pq

instance ProfunctorFunctor FreeBicartesian where
  promap :: forall (p :: * -> * -> *) (q :: * -> * -> *).
Profunctor p =>
(p :-> q) -> FreeBicartesian p :-> FreeBicartesian q
promap p :-> q
pq (FreeBicartesian forall (q :: * -> * -> *).
(Cartesian q, Cocartesian q) =>
(p :-> q) -> q a b
fp) = (forall (q :: * -> * -> *).
 (Cartesian q, Cocartesian q) =>
 (q :-> q) -> q a b)
-> FreeBicartesian q a b
forall (p :: * -> * -> *) a b.
(forall (q :: * -> * -> *).
 (Cartesian q, Cocartesian q) =>
 (p :-> q) -> q a b)
-> FreeBicartesian p a b
FreeBicartesian \q :-> q
ret -> (p :-> q) -> q a b
forall (q :: * -> * -> *).
(Cartesian q, Cocartesian q) =>
(p :-> q) -> q a b
fp (q a b -> q a b
q :-> q
ret (q a b -> q a b) -> (p a b -> q a b) -> p a b -> q a b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. p a b -> q a b
p :-> q
pq)

instance ProfunctorMonad FreeBicartesian where
  proreturn :: forall (p :: * -> * -> *). Profunctor p => p :-> FreeBicartesian p
proreturn = p a b -> FreeBicartesian p a b
forall (p :: * -> * -> *) a b. p a b -> FreeBicartesian p a b
liftFreeBicartesian
  projoin :: forall (p :: * -> * -> *).
Profunctor p =>
FreeBicartesian (FreeBicartesian p) :-> FreeBicartesian p
projoin = (FreeBicartesian p :-> FreeBicartesian p)
-> FreeBicartesian (FreeBicartesian p) :-> FreeBicartesian p
forall (q :: * -> * -> *) (p :: * -> * -> *).
(Cartesian q, Cocartesian q) =>
(p :-> q) -> FreeBicartesian p :-> q
foldFreeBicartesian FreeBicartesian p a b -> FreeBicartesian p a b
forall a. a -> a
FreeBicartesian p :-> FreeBicartesian p
id

-- * Free distributive bicartesian

newtype FreeBicartesianD p a b = FreeBicartesianD
  { forall (p :: * -> * -> *) a b.
FreeBicartesianD p a b -> FreeCocartesian (FreeCartesian p) a b
runFreeBicartesianD :: FreeCocartesian (FreeCartesian p) a b }

instance Profunctor p => Functor (FreeBicartesianD p a) where
  fmap :: forall a b.
(a -> b) -> FreeBicartesianD p a a -> FreeBicartesianD p a b
fmap = (a -> b) -> FreeBicartesianD p a a -> FreeBicartesianD p a b
forall b c a.
(b -> c) -> FreeBicartesianD p a b -> FreeBicartesianD p a c
forall (p :: * -> * -> *) b c a.
Profunctor p =>
(b -> c) -> p a b -> p a c
rmap

deriving newtype instance Profunctor p => Profunctor (FreeBicartesianD p)
deriving newtype instance Profunctor p => Cartesian (FreeBicartesianD p)
deriving newtype instance Profunctor p => Cocartesian (FreeBicartesianD p)

liftFreeBicartesianD :: Profunctor p => p :-> FreeBicartesianD p
liftFreeBicartesianD :: forall (p :: * -> * -> *). Profunctor p => p :-> FreeBicartesianD p
liftFreeBicartesianD = FreeCocartesian (FreeCartesian p) a b -> FreeBicartesianD p a b
forall (p :: * -> * -> *) a b.
FreeCocartesian (FreeCartesian p) a b -> FreeBicartesianD p a b
FreeBicartesianD (FreeCocartesian (FreeCartesian p) a b -> FreeBicartesianD p a b)
-> (p a b -> FreeCocartesian (FreeCartesian p) a b)
-> p a b
-> FreeBicartesianD p a b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FreeCartesian p a b -> FreeCocartesian (FreeCartesian p) a b
forall (p :: * -> * -> *) a b. p a b -> FreeCocartesian p a b
liftFreeCocartesian (FreeCartesian p a b -> FreeCocartesian (FreeCartesian p) a b)
-> (p a b -> FreeCartesian p a b)
-> p a b
-> FreeCocartesian (FreeCartesian p) a b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. p a b -> FreeCartesian p a b
forall (p :: * -> * -> *) a b. p a b -> FreeCartesian p a b
liftFreeCartesian

foldFreeBicartesianD :: (Cartesian q, Cocartesian q) => (p :-> q) -> FreeBicartesianD p :-> q
foldFreeBicartesianD :: forall (q :: * -> * -> *) (p :: * -> * -> *).
(Cartesian q, Cocartesian q) =>
(p :-> q) -> FreeBicartesianD p :-> q
foldFreeBicartesianD p :-> q
handle = (FreeCartesian p :-> q) -> FreeCocartesian (FreeCartesian p) :-> q
forall (q :: * -> * -> *) (p :: * -> * -> *).
Cocartesian q =>
(p :-> q) -> FreeCocartesian p :-> q
foldFreeCocartesian ((p :-> q) -> FreeCartesian p :-> q
forall (q :: * -> * -> *) (p :: * -> * -> *).
Cartesian q =>
(p :-> q) -> FreeCartesian p :-> q
foldFreeCartesian p a b -> q a b
p :-> q
handle) (FreeCocartesian (FreeCartesian p) a b -> q a b)
-> (FreeBicartesianD p a b
    -> FreeCocartesian (FreeCartesian p) a b)
-> FreeBicartesianD p a b
-> q a b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FreeBicartesianD p a b -> FreeCocartesian (FreeCartesian p) a b
forall (p :: * -> * -> *) a b.
FreeBicartesianD p a b -> FreeCocartesian (FreeCartesian p) a b
runFreeBicartesianD

instance ProfunctorFunctor FreeBicartesianD where
    promap :: forall (p :: * -> * -> *) (q :: * -> * -> *).
Profunctor p =>
(p :-> q) -> FreeBicartesianD p :-> FreeBicartesianD q
promap p :-> q
pq = FreeCocartesian (FreeCartesian q) a b -> FreeBicartesianD q a b
forall (p :: * -> * -> *) a b.
FreeCocartesian (FreeCartesian p) a b -> FreeBicartesianD p a b
FreeBicartesianD (FreeCocartesian (FreeCartesian q) a b -> FreeBicartesianD q a b)
-> (FreeBicartesianD p a b
    -> FreeCocartesian (FreeCartesian q) a b)
-> FreeBicartesianD p a b
-> FreeBicartesianD q a b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (FreeCartesian p :-> FreeCartesian q)
-> FreeMonoidal Either Void (FreeCartesian p)
   :-> FreeMonoidal Either Void (FreeCartesian 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 Either Void p :-> FreeMonoidal Either Void q
promap ((p :-> q) -> FreeCartesian p :-> FreeCartesian 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 (,) () p :-> FreeMonoidal (,) () q
promap p a b -> q a b
p :-> q
pq) (FreeMonoidal Either Void (FreeCartesian p) a b
 -> FreeCocartesian (FreeCartesian q) a b)
-> (FreeBicartesianD p a b
    -> FreeMonoidal Either Void (FreeCartesian p) a b)
-> FreeBicartesianD p a b
-> FreeCocartesian (FreeCartesian q) a b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FreeBicartesianD p a b
-> FreeMonoidal Either Void (FreeCartesian p) a b
forall (p :: * -> * -> *) a b.
FreeBicartesianD p a b -> FreeCocartesian (FreeCartesian p) a b
runFreeBicartesianD

instance ProfunctorMonad FreeBicartesianD where
    proreturn :: forall (p :: * -> * -> *). Profunctor p => p :-> FreeBicartesianD p
proreturn = p a b -> FreeBicartesianD p a b
p :-> FreeBicartesianD p
forall (p :: * -> * -> *). Profunctor p => p :-> FreeBicartesianD p
liftFreeBicartesianD
    projoin :: forall (p :: * -> * -> *).
Profunctor p =>
FreeBicartesianD (FreeBicartesianD p) :-> FreeBicartesianD p
projoin = (FreeBicartesianD p :-> FreeBicartesianD p)
-> FreeBicartesianD (FreeBicartesianD p) :-> FreeBicartesianD p
forall (q :: * -> * -> *) (p :: * -> * -> *).
(Cartesian q, Cocartesian q) =>
(p :-> q) -> FreeBicartesianD p :-> q
foldFreeBicartesianD FreeBicartesianD p a b -> FreeBicartesianD p a b
forall a. a -> a
FreeBicartesianD p :-> FreeBicartesianD p
id