{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# OPTIONS_GHC -Wno-orphans #-}

module Proarrow.Profunctor.Free where

import Data.Foldable1 (Foldable1 (foldMap1))
import Data.Kind (Constraint, Type)
import Data.List.NonEmpty (NonEmpty (..))
import Data.Maybe (Maybe (..))
import Prelude (($))
import Prelude qualified as P

import Proarrow.Category.Instance.IntConstruction (INT (..), IntConstruction (..), toInt)
import Proarrow.Category.Instance.Nat (Nat (..), first)
import Proarrow.Category.Instance.Prof (Prof (..))
import Proarrow.Category.Instance.Sub (Forget, On, SUBCAT (..), Sub (..))
import Proarrow.Category.Monoidal (Monoidal (..), MonoidalProfunctor (..), swap)
import Proarrow.Category.Monoidal.Action (TracedMonoidal)
import Proarrow.Category.Monoidal.Applicative (Applicative (..))
import Proarrow.Category.Monoidal.Strictified (Fold, Strictified (..), (==), (||))
import Proarrow.Core
  ( CAT
  , CategoryOf (..)
  , Kind
  , OB
  , Profunctor (..)
  , Promonad (..)
  , UN
  , arr
  , lmap
  , obj
  , rmap
  , tgt
  , (//)
  , (:~>)
  )
import Proarrow.Functor (Functor (..))
import Proarrow.Monoid (Monoid (..))
import Proarrow.Object.Dual (CompactClosed, Dual, dualObj, dualityCounit, dualityUnit)
import Proarrow.Profunctor.Composition ((:.:) (..))
import Proarrow.Profunctor.Corepresentable (Corepresentable (..))
import Proarrow.Profunctor.List (LIST (..), List (..))
import Proarrow.Profunctor.Representable (Rep (..))
import Proarrow.Profunctor.Star (Star, pattern Star)

type HasFree :: forall {k}. OB k -> Constraint
class (CategoryOf k, forall a. (Ob a) => ob (Free ob a)) => HasFree (ob :: OB k) where
  type Free ob (a :: k) :: k
  lift :: (Ob a) => a ~> Free ob a
  foldMap :: (ob b) => (a ~> b) -> Free ob a ~> b

retract :: forall ob a. (HasFree ob, ob a, Ob a) => Free ob a ~> a
retract :: forall {k} (ob :: OB k) (a :: k).
(HasFree ob, ob a, Ob a) =>
Free ob a ~> a
retract = forall {k} (ob :: OB k) (b :: k) (a :: k).
(HasFree ob, ob b) =>
(a ~> b) -> Free ob a ~> b
forall (ob :: OB k) (b :: k) (a :: k).
(HasFree ob, ob b) =>
(a ~> b) -> Free ob a ~> b
foldMap @ob a ~> a
forall (a :: k). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id

freeMap :: (HasFree ob) => (a ~> b) -> Free ob a ~> Free ob b
freeMap :: forall {k} (ob :: OB k) (a :: k) (b :: k).
HasFree ob =>
(a ~> b) -> Free ob a ~> Free ob b
freeMap @ob a ~> b
f = forall {k} (ob :: OB k) (b :: k) (a :: k).
(HasFree ob, ob b) =>
(a ~> b) -> Free ob a ~> b
forall (ob :: OB k) (b :: k) (a :: k).
(HasFree ob, ob b) =>
(a ~> b) -> Free ob a ~> b
foldMap @ob (forall {k} (ob :: OB k) (a :: k).
(HasFree ob, Ob a) =>
a ~> Free ob a
forall (ob :: OB k) (a :: k). (HasFree ob, Ob a) => a ~> Free ob a
lift @ob (b ~> Free ob b) -> (a ~> b) -> a ~> Free ob b
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. a ~> b
f) ((Ob a, Ob b) => Free ob a ~> Free ob b)
-> (a ~> b) -> Free ob a ~> Free ob b
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ a ~> b
f

freeComp :: (HasFree ob, Ob c) => b ~> Free ob c -> a ~> Free ob b -> a ~> Free ob c
freeComp :: forall {k} (ob :: OB k) (c :: k) (b :: k) (a :: k).
(HasFree ob, Ob c) =>
(b ~> Free ob c) -> (a ~> Free ob b) -> a ~> Free ob c
freeComp @ob b ~> Free ob c
l a ~> Free ob b
r = forall {k} (ob :: OB k) (b :: k) (a :: k).
(HasFree ob, ob b) =>
(a ~> b) -> Free ob a ~> b
forall (ob :: OB k) (b :: k) (a :: k).
(HasFree ob, ob b) =>
(a ~> b) -> Free ob a ~> b
foldMap @ob b ~> Free ob c
l (Free ob b ~> Free ob c) -> (a ~> Free ob b) -> a ~> Free ob c
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. a ~> Free ob b
r

-- | By creating the left adjoint to the forgetful functor,
-- we obtain the free-forgetful adjunction.
instance (HasFree ob) => Corepresentable (Rep (Forget (ob :: OB k))) where
  type Rep (Forget ob) %% a = SUB (Free ob a)
  coindex :: forall (a :: k) (b :: SUBCAT ob).
Rep (Forget ob) a b -> (Rep (Forget ob) %% a) ~> b
coindex (Rep a ~> (Forget ob @ b)
f) = (Free ob a ~> UN SUB b)
-> Sub (~>) (SUB (Free ob a)) (SUB (UN SUB b))
forall {k} (ob :: OB k) (a1 :: k) (b1 :: k) (p :: CAT k).
(ob a1, ob b1) =>
p a1 b1 -> Sub p (SUB a1) (SUB b1)
Sub (forall {k} (ob :: OB k) (b :: k) (a :: k).
(HasFree ob, ob b) =>
(a ~> b) -> Free ob a ~> b
forall (ob :: OB k) (b :: k) (a :: k).
(HasFree ob, ob b) =>
(a ~> b) -> Free ob a ~> b
foldMap @ob a ~> UN SUB b
a ~> (Forget ob @ b)
f) ((Ob a, Ob (UN SUB b)) =>
 Sub (~>) (SUB (Free ob a)) (SUB (UN SUB b)))
-> (a ~> UN SUB b) -> Sub (~>) (SUB (Free ob a)) (SUB (UN SUB b))
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ a ~> UN SUB b
a ~> (Forget ob @ b)
f
  trivialCorep :: forall (a :: k). Ob a => Rep (Forget ob) a (Rep (Forget ob) %% a)
trivialCorep @a = let f :: a ~> Free ob a
f = forall {k} (ob :: OB k) (a :: k).
(HasFree ob, Ob a) =>
a ~> Free ob a
forall (ob :: OB k) (a :: k). (HasFree ob, Ob a) => a ~> Free ob a
lift @ob @a in (a ~> (Forget ob @ SUB (Free ob a)))
-> Rep (Forget ob) a (SUB (Free ob a))
forall {j} {k} (f :: j +-> k) (a :: k) (b :: j).
Ob b =>
(a ~> (f @ b)) -> Rep f a b
Rep a ~> (Forget ob @ SUB (Free ob a))
a ~> Free ob a
f ((Ob a, Ob (Free ob a)) => Rep (Forget ob) a (SUB (Free ob a)))
-> (a ~> Free ob a) -> Rep (Forget ob) a (SUB (Free ob a))
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ a ~> Free ob a
f

instance HasFree P.Monoid where
  type Free P.Monoid a = [a]
  lift :: forall a. Ob a => a ~> Free Monoid a
lift = a ~> Free Monoid a
a -> [a]
forall a. a -> [a]
forall (f :: Type -> Type) a. Applicative f => a -> f a
P.pure
  foldMap :: forall b a. Monoid b => (a ~> b) -> Free Monoid a ~> b
foldMap = (a ~> b) -> Free Monoid a ~> b
(a -> b) -> [a] -> b
forall m a. Monoid m => (a -> m) -> [a] -> m
forall (t :: Type -> Type) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
P.foldMap

instance HasFree P.Semigroup where
  type Free P.Semigroup a = NonEmpty a
  lift :: forall a. Ob a => a ~> Free Semigroup a
lift = a ~> Free Semigroup a
a -> NonEmpty a
forall a. a -> NonEmpty a
forall (f :: Type -> Type) a. Applicative f => a -> f a
P.pure
  foldMap :: forall b a. Semigroup b => (a ~> b) -> Free Semigroup a ~> b
foldMap = (a ~> b) -> Free Semigroup a ~> b
(a -> b) -> NonEmpty a -> b
forall m a. Semigroup m => (a -> m) -> NonEmpty a -> m
forall (t :: Type -> Type) m a.
(Foldable1 t, Semigroup m) =>
(a -> m) -> t a -> m
foldMap1

instance HasFree (P.Monoid `On` P.Semigroup) where
  type Free (P.Monoid `On` P.Semigroup) (SUB a) = SUB (Maybe a)
  lift :: forall (a :: SUBCAT Semigroup).
Ob a =>
a ~> Free (On Monoid Semigroup) a
lift = (UN SUB a -> Maybe (UN SUB a))
-> Sub (->) (SUB (UN SUB a)) (SUB (Maybe (UN SUB a)))
forall {k} (ob :: OB k) (a1 :: k) (b1 :: k) (p :: CAT k).
(ob a1, ob b1) =>
p a1 b1 -> Sub p (SUB a1) (SUB b1)
Sub UN SUB a -> Maybe (UN SUB a)
forall a. a -> Maybe a
Just
  foldMap :: forall (b :: SUBCAT Semigroup) (a :: SUBCAT Semigroup).
On Monoid Semigroup b =>
(a ~> b) -> Free (On Monoid Semigroup) a ~> b
foldMap (Sub a1 -> b1
f) = (Maybe a1 -> b1) -> Sub (->) (SUB (Maybe a1)) (SUB b1)
forall {k} (ob :: OB k) (a1 :: k) (b1 :: k) (p :: CAT k).
(ob a1, ob b1) =>
p a1 b1 -> Sub p (SUB a1) (SUB b1)
Sub ((a1 -> b1) -> Maybe a1 -> b1
forall m a. Monoid m => (a -> m) -> Maybe a -> m
forall (t :: Type -> Type) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
P.foldMap a1 -> b1
f)

type Ap :: (k -> Type) -> k -> Type
data Ap f a where
  Pure :: Unit ~> a -> Ap f a
  Eff :: f a -> Ap f a
  LiftA2 :: (Ob a, Ob b) => (a ** b ~> c) -> Ap f a -> Ap f b -> Ap f c

instance (CategoryOf k, Functor f) => Functor (Ap (f :: k -> Type)) where
  map :: forall (a :: k) (b :: k). (a ~> b) -> Ap f a ~> Ap f b
map a ~> b
f (Pure Unit ~> a
a) = (Unit ~> b) -> Ap f b
forall {k} (a :: k) (f :: k -> Type). (Unit ~> a) -> Ap f a
Pure (a ~> b
f (a ~> b) -> (Unit ~> a) -> Unit ~> b
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. Unit ~> a
a)
  map a ~> b
f (Eff f a
x) = f b -> Ap f b
forall {k} (f :: k -> Type) (a :: k). f a -> Ap f a
Eff ((a ~> b) -> f a ~> f b
forall (a :: k) (b :: k). (a ~> b) -> f a ~> f b
forall {k1} {k2} (f :: k1 -> k2) (a :: k1) (b :: k1).
Functor f =>
(a ~> b) -> f a ~> f b
map a ~> b
f f a
x)
  map a ~> b
f (LiftA2 (a ** b) ~> a
k Ap f a
x Ap f b
y) = ((a ** b) ~> b) -> Ap f a -> Ap f b -> Ap f b
forall {k} (b :: k) (b :: k) (c :: k) (f :: k -> Type).
(Ob b, Ob b) =>
((b ** b) ~> c) -> Ap f b -> Ap f b -> Ap f c
LiftA2 (a ~> b
f (a ~> b) -> ((a ** b) ~> a) -> (a ** b) ~> b
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (a ** b) ~> a
k) Ap f a
x Ap f b
y

instance Functor Ap where
  map :: forall (a :: k -> Type) (b :: k -> Type). (a ~> b) -> Ap a ~> Ap b
map (Nat a .~> b
n) = (Ap a .~> Ap b) -> Nat (Ap a) (Ap b)
forall {j} {k} (f :: j -> k) (g :: j -> k).
(Functor f, Functor g) =>
(f .~> g) -> Nat f g
Nat ((Ap a .~> Ap b) -> Nat (Ap a) (Ap b))
-> (Ap a .~> Ap b) -> Nat (Ap a) (Ap b)
forall a b. (a -> b) -> a -> b
$ \case
    Pure Unit ~> a
a -> (Unit ~> a) -> Ap b a
forall {k} (a :: k) (f :: k -> Type). (Unit ~> a) -> Ap f a
Pure Unit ~> a
a
    Eff a a
fa -> b a -> Ap b a
forall {k} (f :: k -> Type) (a :: k). f a -> Ap f a
Eff (a a ~> b a
a a -> b a
a .~> b
n a a
fa)
    LiftA2 (a ** b) ~> a
k Ap a a
x Ap a b
y -> ((a ** b) ~> a) -> Ap b a -> Ap b b -> Ap b a
forall {k} (b :: k) (b :: k) (c :: k) (f :: k -> Type).
(Ob b, Ob b) =>
((b ** b) ~> c) -> Ap f b -> Ap f b -> Ap f c
LiftA2 (a ** b) ~> a
k ((a ~> b) -> Ap a a ~> Ap b a
forall i j k (f :: i -> j -> k) (c :: j) (a :: i) (b :: i).
(Functor f, (~>) ~ Nat, Ob c) =>
(a ~> b) -> f a c ~> f b c
first ((a .~> b) -> Nat a b
forall {j} {k} (f :: j -> k) (g :: j -> k).
(Functor f, Functor g) =>
(f .~> g) -> Nat f g
Nat a a ~> b a
a .~> b
n) Ap a a
x) ((a ~> b) -> Ap a b ~> Ap b b
forall i j k (f :: i -> j -> k) (c :: j) (a :: i) (b :: i).
(Functor f, (~>) ~ Nat, Ob c) =>
(a ~> b) -> f a c ~> f b c
first ((a .~> b) -> Nat a b
forall {j} {k} (f :: j -> k) (g :: j -> k).
(Functor f, Functor g) =>
(f .~> g) -> Nat f g
Nat a a ~> b a
a .~> b
n) Ap a b
y)

instance (Monoidal k) => Promonad (Star Ap :: CAT (k -> Type)) where
  id :: forall (a :: k -> Type). Ob a => Star Ap a a
id = (a ~> Ap a) -> Star Ap a a
forall {j} {k} (b :: j) (a :: k) (f :: j -> k).
Ob b =>
(a ~> f b) -> Star f a b
Star (forall {k} (ob :: OB k) (a :: k).
(HasFree ob, Ob a) =>
a ~> Free ob a
forall (ob :: OB (k -> Type)) (a :: k -> Type).
(HasFree ob, Ob a) =>
a ~> Free ob a
lift @Applicative)
  Star b ~> Ap c
l . :: forall (b :: k -> Type) (c :: k -> Type) (a :: k -> Type).
Star Ap b c -> Star Ap a b -> Star Ap a c
. Star a ~> Ap b
r = (a ~> Ap c) -> Star Ap a c
forall {j} {k} (b :: j) (a :: k) (f :: j -> k).
Ob b =>
(a ~> f b) -> Star f a b
Star (forall {k} (ob :: OB k) (c :: k) (b :: k) (a :: k).
(HasFree ob, Ob c) =>
(b ~> Free ob c) -> (a ~> Free ob b) -> a ~> Free ob c
forall (ob :: OB (k -> Type)) (c :: k -> Type) (b :: k -> Type)
       (a :: k -> Type).
(HasFree ob, Ob c) =>
(b ~> Free ob c) -> (a ~> Free ob b) -> a ~> Free ob c
freeComp @Applicative b ~> Ap c
b ~> Free Applicative c
l a ~> Ap b
a ~> Free Applicative b
r)

instance (Monoidal k, Functor f) => Applicative (Ap (f :: k -> Type)) where
  pure :: forall (a :: k). (Unit ~> a) -> Unit ~> Ap f a
pure Unit ~> a
a () = (Unit ~> a) -> Ap f a
forall {k} (a :: k) (f :: k -> Type). (Unit ~> a) -> Ap f a
Pure Unit ~> a
a
  liftA2 :: forall (a :: k) (b :: k) (c :: k).
(Ob a, Ob b) =>
((a ** b) ~> c) -> (Ap f a ** Ap f b) ~> Ap f c
liftA2 (a ** b) ~> c
f (Ap f a
fa, Ap f b
fb) = ((a ** b) ~> c) -> Ap f a -> Ap f b -> Ap f c
forall {k} (b :: k) (b :: k) (c :: k) (f :: k -> Type).
(Ob b, Ob b) =>
((b ** b) ~> c) -> Ap f b -> Ap f b -> Ap f c
LiftA2 (a ** b) ~> c
f Ap f a
fa Ap f b
fb

instance (Monoidal k, Monoid m) => Monoid (Ap (f :: k -> Type) m) where
  mempty :: Unit ~> Ap f m
mempty () = (Unit ~> m) -> Ap f m
forall {k} (a :: k) (f :: k -> Type). (Unit ~> a) -> Ap f a
Pure Unit ~> m
forall {k} (m :: k). Monoid m => Unit ~> m
mempty
  mappend :: (Ap f m ** Ap f m) ~> Ap f m
mappend (Ap f m
l, Ap f m
r) = ((m ** m) ~> m) -> Ap f m -> Ap f m -> Ap f m
forall {k} (b :: k) (b :: k) (c :: k) (f :: k -> Type).
(Ob b, Ob b) =>
((b ** b) ~> c) -> Ap f b -> Ap f b -> Ap f c
LiftA2 (m ** m) ~> m
forall {k} (m :: k). Monoid m => (m ** m) ~> m
mappend Ap f m
l Ap f m
r

retractAp :: (Applicative f) => Ap f a -> f a
retractAp :: forall {k} (f :: k -> Type) (a :: k).
Applicative f =>
Ap f a -> f a
retractAp (Pure Unit ~> a
a) = (Unit ~> a) -> Unit ~> f a
forall (a :: k). (Unit ~> a) -> Unit ~> f a
forall {j} {k} (f :: j -> k) (a :: j).
Applicative f =>
(Unit ~> a) -> Unit ~> f a
pure Unit ~> a
a ()
retractAp (Eff f a
fa) = f a
fa
retractAp (LiftA2 (a ** b) ~> a
k Ap f a
x Ap f b
y) = ((a ** b) ~> a) -> (f a ** f b) ~> f a
forall (a :: k) (b :: k) (c :: k).
(Ob a, Ob b) =>
((a ** b) ~> c) -> (f a ** f b) ~> f c
forall {j} {k} (f :: j -> k) (a :: j) (b :: j) (c :: j).
(Applicative f, Ob a, Ob b) =>
((a ** b) ~> c) -> (f a ** f b) ~> f c
liftA2 (a ** b) ~> a
k (Ap f a -> f a
forall {k} (f :: k -> Type) (a :: k).
Applicative f =>
Ap f a -> f a
retractAp Ap f a
x, Ap f b -> f b
forall {k} (f :: k -> Type) (a :: k).
Applicative f =>
Ap f a -> f a
retractAp Ap f b
y)

instance (Monoidal k) => HasFree (Applicative :: OB (k -> Type)) where
  type Free Applicative f = Ap f
  lift :: forall (a :: k -> Type). Ob a => a ~> Free Applicative a
lift = (a .~> Ap a) -> Nat a (Ap a)
forall {j} {k} (f :: j -> k) (g :: j -> k).
(Functor f, Functor g) =>
(f .~> g) -> Nat f g
Nat a a ~> Ap a a
a a -> Ap a a
a .~> Ap a
forall {k} (f :: k -> Type) (a :: k). f a -> Ap f a
Eff
  foldMap :: forall (b :: k -> Type) (a :: k -> Type).
Applicative b =>
(a ~> b) -> Free Applicative a ~> b
foldMap f :: a ~> b
f@Nat{} = (Ap b .~> b) -> Nat (Ap b) b
forall {j} {k} (f :: j -> k) (g :: j -> k).
(Functor f, Functor g) =>
(f .~> g) -> Nat f g
Nat Ap b a ~> b a
Ap b a -> b a
Ap b .~> b
forall {k} (f :: k -> Type) (a :: k).
Applicative f =>
Ap f a -> f a
retractAp Nat (Ap b) b -> Nat (Ap a) (Ap b) -> Nat (Ap a) b
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
forall (b :: k -> Type) (c :: k -> Type) (a :: k -> Type).
Nat b c -> Nat a b -> Nat a c
. (a ~> b) -> Ap a ~> Ap b
forall {k1} {k2} (f :: k1 -> k2) (a :: k1) (b :: k1).
Functor f =>
(a ~> b) -> f a ~> f b
forall (a :: k -> Type) (b :: k -> Type). (a ~> b) -> Ap a ~> Ap b
map a ~> b
f

data FreePromonad p a b where
  Unit :: (a ~> b) -> FreePromonad p a b
  Comp :: p a b -> FreePromonad p b c -> FreePromonad p a c

freePromonadAlg :: p :.: FreePromonad p :~> FreePromonad p
freePromonadAlg :: forall {k} (p :: k +-> k) (a :: k) (b :: k).
(:.:) p (FreePromonad p) a b -> FreePromonad p a b
freePromonadAlg (p a b
p :.: FreePromonad p b b
pp) = p a b -> FreePromonad p b b -> FreePromonad p a b
forall {k} (p :: k -> k -> Type) (a :: k) (b :: k) (c :: k).
p a b -> FreePromonad p b c -> FreePromonad p a c
Comp p a b
p FreePromonad p b b
pp

retractFreePromonad :: (Promonad p) => FreePromonad p :~> p
retractFreePromonad :: forall {k1} (p :: k1 +-> k1). Promonad p => FreePromonad p :~> p
retractFreePromonad (Unit a ~> b
f) = (a ~> b) -> p a b
forall {k} (p :: k +-> k) (a :: k) (b :: k).
Promonad p =>
(a ~> b) -> p a b
arr a ~> b
f
retractFreePromonad (Comp p a b
p FreePromonad p b b
pp) = FreePromonad p b b -> p b b
FreePromonad p :~> p
forall {k1} (p :: k1 +-> k1). Promonad p => FreePromonad p :~> p
retractFreePromonad FreePromonad p b b
pp p b b -> p a b -> p a b
forall (b :: k1) (c :: k1) (a :: k1). p b c -> p a b -> p a c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. p a b
p

instance (Profunctor p) => Profunctor (FreePromonad p) where
  dimap :: forall (c :: j) (a :: j) (b :: j) (d :: j).
(c ~> a) -> (b ~> d) -> FreePromonad p a b -> FreePromonad p c d
dimap c ~> a
l b ~> d
r (Unit a ~> b
f) = (c ~> d) -> FreePromonad p c d
forall {k} (a :: k) (b :: k) (p :: k -> k -> Type).
(a ~> b) -> FreePromonad p a b
Unit (b ~> d
r (b ~> d) -> (c ~> b) -> c ~> d
forall (b :: j) (c :: j) (a :: j). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. a ~> b
f (a ~> b) -> (c ~> a) -> c ~> b
forall (b :: j) (c :: j) (a :: j). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. c ~> a
l)
  dimap c ~> a
l b ~> d
r (Comp p a b
p FreePromonad p b b
q) = p c b -> FreePromonad p b d -> FreePromonad p c d
forall {k} (p :: k -> k -> Type) (a :: k) (b :: k) (c :: k).
p a b -> FreePromonad p b c -> FreePromonad p a c
Comp ((c ~> a) -> p a b -> p c b
forall (c :: j) (a :: j) (b :: j). (c ~> a) -> p a b -> p c b
forall {j} {k} (p :: j +-> k) (c :: k) (a :: k) (b :: j).
Profunctor p =>
(c ~> a) -> p a b -> p c b
lmap c ~> a
l p a b
p) ((b ~> d) -> FreePromonad p b b -> FreePromonad p b d
forall (b :: j) (d :: j) (a :: j).
(b ~> d) -> FreePromonad p a b -> FreePromonad p a d
forall {j} {k} (p :: j +-> k) (b :: j) (d :: j) (a :: k).
Profunctor p =>
(b ~> d) -> p a b -> p a d
rmap b ~> d
r FreePromonad p b b
q)
  (Ob a, Ob b) => r
r \\ :: forall (a :: j) (b :: j) r.
((Ob a, Ob b) => r) -> FreePromonad p a b -> r
\\ (Unit a ~> b
f) = r
(Ob a, Ob b) => r
r ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall (a :: j) (b :: j) r. ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ a ~> b
f
  (Ob a, Ob b) => r
r \\ Comp p a b
p FreePromonad p b b
q = r
(Ob a, Ob b) => r
(Ob a, Ob b) => r
r ((Ob a, Ob b) => r) -> p a b -> r
forall (a :: j) (b :: j) r. ((Ob a, Ob b) => r) -> p a b -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ p a b
p ((Ob b, Ob b) => r) -> FreePromonad p b b -> r
forall (a :: j) (b :: j) r.
((Ob a, Ob b) => r) -> FreePromonad p a b -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ FreePromonad p b b
q

instance (Profunctor p) => Promonad (FreePromonad p) where
  id :: forall (a :: k). Ob a => FreePromonad p a a
id = (a ~> a) -> FreePromonad p a a
forall {k} (a :: k) (b :: k) (p :: k -> k -> Type).
(a ~> b) -> FreePromonad p a b
Unit a ~> a
forall (a :: k). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id
  FreePromonad p b c
p . :: forall (b :: k) (c :: k) (a :: k).
FreePromonad p b c -> FreePromonad p a b -> FreePromonad p a c
. Unit a ~> b
f = (a ~> b) -> FreePromonad p b c -> FreePromonad p a c
forall (c :: k) (a :: k) (b :: k).
(c ~> a) -> FreePromonad p a b -> FreePromonad p c b
forall {j} {k} (p :: j +-> k) (c :: k) (a :: k) (b :: j).
Profunctor p =>
(c ~> a) -> p a b -> p c b
lmap a ~> b
f FreePromonad p b c
p
  FreePromonad p b c
p . Comp p a b
r FreePromonad p b b
q = p a b -> FreePromonad p b c -> FreePromonad p a c
forall {k} (p :: k -> k -> Type) (a :: k) (b :: k) (c :: k).
p a b -> FreePromonad p b c -> FreePromonad p a c
Comp p a b
r (FreePromonad p b c
p FreePromonad p b c -> FreePromonad p b b -> FreePromonad p b c
forall (b :: k) (c :: k) (a :: k).
FreePromonad p b c -> FreePromonad p a b -> FreePromonad p a c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. FreePromonad p b b
q)
instance Functor FreePromonad where
  map :: forall (a :: k -> k -> Type) (b :: k -> k -> Type).
(a ~> b) -> FreePromonad a ~> FreePromonad b
map = forall {k} (ob :: OB k) (a :: k) (b :: k).
HasFree ob =>
(a ~> b) -> Free ob a ~> Free ob b
forall (ob :: OB (k -> k -> Type)) (a :: k -> k -> Type)
       (b :: k -> k -> Type).
HasFree ob =>
(a ~> b) -> Free ob a ~> Free ob b
freeMap @Promonad
instance Promonad (Star FreePromonad) where
  id :: forall (a :: k -> k -> Type). Ob a => Star FreePromonad a a
id = (a ~> FreePromonad a) -> Star FreePromonad a a
forall {j} {k} (b :: j) (a :: k) (f :: j -> k).
Ob b =>
(a ~> f b) -> Star f a b
Star (forall {k} (ob :: OB k) (a :: k).
(HasFree ob, Ob a) =>
a ~> Free ob a
forall (ob :: OB (k -> k -> Type)) (a :: k -> k -> Type).
(HasFree ob, Ob a) =>
a ~> Free ob a
lift @Promonad)
  Star b ~> FreePromonad c
l . :: forall (b :: k -> k -> Type) (c :: k -> k -> Type)
       (a :: k -> k -> Type).
Star FreePromonad b c
-> Star FreePromonad a b -> Star FreePromonad a c
. Star a ~> FreePromonad b
r = (a ~> FreePromonad c) -> Star FreePromonad a c
forall {j} {k} (b :: j) (a :: k) (f :: j -> k).
Ob b =>
(a ~> f b) -> Star f a b
Star (forall {k} (ob :: OB k) (c :: k) (b :: k) (a :: k).
(HasFree ob, Ob c) =>
(b ~> Free ob c) -> (a ~> Free ob b) -> a ~> Free ob c
forall (ob :: OB (k -> k -> Type)) (c :: k -> k -> Type)
       (b :: k -> k -> Type) (a :: k -> k -> Type).
(HasFree ob, Ob c) =>
(b ~> Free ob c) -> (a ~> Free ob b) -> a ~> Free ob c
freeComp @Promonad b ~> FreePromonad c
b ~> Free Promonad c
l a ~> FreePromonad b
a ~> Free Promonad b
r)
instance HasFree Promonad where
  type Free Promonad p = FreePromonad p
  lift :: forall (a :: k +-> k). Ob a => a ~> Free Promonad a
lift = (a :~> FreePromonad a) -> Prof a (FreePromonad a)
forall {j} {k} (p :: j +-> k) (q :: j +-> k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
Prof \a a b
p -> a a b
p a a b -> FreePromonad a b b -> FreePromonad a a b
forall {k} (p :: k -> k -> Type) (a :: k) (b :: k) (c :: k).
p a b -> FreePromonad p b c -> FreePromonad p a c
`Comp` (b ~> b) -> FreePromonad a b b
forall {k} (a :: k) (b :: k) (p :: k -> k -> Type).
(a ~> b) -> FreePromonad p a b
Unit (a a b -> b ~> b
forall {k1} {k2} (a :: k2) (b :: k1) (p :: k1 +-> k2).
Profunctor p =>
p a b -> Obj b
tgt a a b
p)
  foldMap :: forall (b :: k +-> k) (a :: k +-> k).
Promonad b =>
(a ~> b) -> Free Promonad a ~> b
foldMap n :: a ~> b
n@Prof{} = (FreePromonad b :~> b) -> Prof (FreePromonad b) b
forall {j} {k} (p :: j +-> k) (q :: j +-> k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
Prof FreePromonad b a b -> b a b
FreePromonad b :~> b
forall {k1} (p :: k1 +-> k1). Promonad p => FreePromonad p :~> p
retractFreePromonad Prof (FreePromonad b) b
-> Prof (FreePromonad a) (FreePromonad b)
-> Prof (FreePromonad a) b
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
forall (b :: k +-> k) (c :: k +-> k) (a :: k +-> k).
Prof b c -> Prof a b -> Prof a c
. (a ~> b) -> FreePromonad a ~> FreePromonad b
forall {k1} {k2} (f :: k1 -> k2) (a :: k1) (b :: k1).
Functor f =>
(a ~> b) -> f a ~> f b
forall (a :: k +-> k) (b :: k +-> k).
(a ~> b) -> FreePromonad a ~> FreePromonad b
map a ~> b
n

class
  (forall k. (b k) => c (f k)) =>
  HasFreeK (b :: Kind -> Constraint) (c :: Kind -> Constraint) (f :: Kind -> Kind)
    | b c -> f
  where
  type Lift b c f (a :: k) :: f k
  type Retract b c f (a :: f k) :: k
  liftK :: (b k) => (x :: k) ~> y -> Lift b c f x ~> Lift b c f y
  retractK :: (c k) => (x :: f k) ~> y -> Retract b c f x ~> Retract b c f y

instance HasFreeK CategoryOf Monoidal LIST where
  type Lift CategoryOf Monoidal LIST a = L '[a]
  type Retract CategoryOf Monoidal LIST (a :: LIST k) = Fold (UN L a)
  liftK :: forall k (x :: k) (y :: k).
CategoryOf k =>
(x ~> y)
-> Lift CategoryOf Monoidal LIST x
   ~> Lift CategoryOf Monoidal LIST y
liftK x ~> y
f = (x ~> y)
-> List (~>) (L '[]) (L '[]) -> List (~>) (L '[x]) (L '[y])
forall {k} {j} (as1 :: [k]) (bs1 :: [j]) (p :: j +-> k) (a :: k)
       (b :: j).
(IsList as1, IsList bs1) =>
p a b
-> List p (L as1) (L bs1) -> List p (L (a : as1)) (L (b : bs1))
Cons x ~> y
f List (~>) (L '[]) (L '[])
forall {j} {k} (p :: j +-> k). List p (L '[]) (L '[])
Nil
  retractK :: forall k (x :: LIST k) (y :: LIST k).
Monoidal k =>
(x ~> y)
-> Retract CategoryOf Monoidal LIST x
   ~> Retract CategoryOf Monoidal LIST y
retractK x ~> y
List (~>) x y
Nil = Unit ~> Unit
Retract CategoryOf Monoidal LIST x
~> Retract CategoryOf Monoidal LIST y
forall {j} {k} (p :: j +-> k). MonoidalProfunctor p => p Unit Unit
par0
  retractK (Cons a ~> b
f List (~>) (L as1) (L bs1)
Nil) = a ~> b
Retract CategoryOf Monoidal LIST x
~> Retract CategoryOf Monoidal LIST y
f
  retractK (Cons a ~> b
f fs :: List (~>) (L as1) (L bs1)
fs@Cons{}) = a ~> b
f (a ~> b)
-> (Retract CategoryOf Monoidal LIST (L (a : as1))
    ~> Retract CategoryOf Monoidal LIST (L (b : bs1)))
-> (a ** Retract CategoryOf Monoidal LIST (L (a : as1)))
   ~> (b ** Retract CategoryOf Monoidal LIST (L (b : bs1)))
forall (x1 :: k) (x2 :: k) (y1 :: k) (y2 :: k).
(x1 ~> x2) -> (y1 ~> y2) -> (x1 ** y1) ~> (x2 ** y2)
forall {j} {k} (p :: j +-> k) (x1 :: k) (x2 :: j) (y1 :: k)
       (y2 :: j).
MonoidalProfunctor p =>
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
`par` forall (b :: Type -> Constraint) (c :: Type -> Constraint)
       (f :: Type -> Type) k (x :: f k) (y :: f k).
(HasFreeK b c f, c k) =>
(x ~> y) -> Retract b c f x ~> Retract b c f y
retractK @CategoryOf @Monoidal L (a : as1) ~> L (b : bs1)
List (~>) (L as1) (L bs1)
fs

instance HasFreeK TracedMonoidal CompactClosed INT where
  type Lift TracedMonoidal CompactClosed INT (a :: k) = I a Unit
  type Retract TracedMonoidal CompactClosed INT (I a b :: INT k) = a ** Dual b
  liftK :: forall k (x :: k) (y :: k).
TracedMonoidal k =>
(x ~> y)
-> Lift TracedMonoidal CompactClosed INT x
   ~> Lift TracedMonoidal CompactClosed INT y
liftK = (x ~> y) -> 'I x Unit ~> 'I y Unit
(x ~> y)
-> Lift TracedMonoidal CompactClosed INT x
   ~> Lift TracedMonoidal CompactClosed INT y
forall {k} (a :: k) (b :: k) (m :: k).
(TracedMonoidal k, Ob m) =>
(a ~> b) -> 'I a m ~> 'I b m
toInt
  retractK :: forall k (x :: INT k) (y :: INT k).
CompactClosed k =>
(x ~> y)
-> Retract TracedMonoidal CompactClosed INT x
   ~> Retract TracedMonoidal CompactClosed INT y
retractK (Int @ap @am @bp @bm (ap ** bm) ~> (am ** bp)
f) =
    forall (a :: k). (StarAutonomous k, Ob a) => Obj (Dual a)
forall {k} (a :: k). (StarAutonomous k, Ob a) => Obj (Dual a)
dualObj @am Obj (Dual am)
-> ((Ob (Dual am), Ob (Dual am)) =>
    (ap ** Dual am) ~> (bp ** Dual bm))
-> (ap ** Dual am) ~> (bp ** Dual bm)
forall {k1} {k2} (p :: k1 +-> k2) (a :: k2) (b :: k1) r.
Profunctor p =>
p a b -> ((Ob a, Ob b) => r) -> r
//
      forall (a :: k). (StarAutonomous k, Ob a) => Obj (Dual a)
forall {k} (a :: k). (StarAutonomous k, Ob a) => Obj (Dual a)
dualObj @bm Obj (Dual bm)
-> ((Ob (Dual bm), Ob (Dual bm)) =>
    (ap ** Dual am) ~> (bp ** Dual bm))
-> (ap ** Dual am) ~> (bp ** Dual bm)
forall {k1} {k2} (p :: k1 +-> k2) (a :: k2) (b :: k1) r.
Profunctor p =>
p a b -> ((Ob a, Ob b) => r) -> r
//
        Strictified '[ap, Dual am] '[bp, Dual bm]
-> Fold '[ap, Dual am] ~> Fold '[bp, Dual bm]
forall {k} (as :: [k]) (bs :: [k]).
Strictified as bs -> Fold as ~> Fold bs
unStr (Strictified '[ap, Dual am] '[bp, Dual bm]
 -> Fold '[ap, Dual am] ~> Fold '[bp, Dual bm])
-> Strictified '[ap, Dual am] '[bp, Dual bm]
-> Fold '[ap, Dual am] ~> Fold '[bp, Dual bm]
forall a b. (a -> b) -> a -> b
$
          forall (as :: [k]) (bs :: [k]).
(Ob as, Ob bs) =>
(Fold as ~> Fold bs) -> Strictified as bs
forall {k} (as :: [k]) (bs :: [k]).
(Ob as, Ob bs) =>
(Fold as ~> Fold bs) -> Strictified as bs
Str @[ap, Dual am] @[Dual am, ap] (forall k (a :: k) (b :: k).
(SymMonoidal k, Ob a, Ob b) =>
(a ** b) ~> (b ** a)
swap @_ @ap @(Dual am)) ('[ap, Dual am] ~> '[Dual am, ap])
-> ('[] ~> '[bm, Dual bm])
-> ('[ap, Dual am] ++ '[]) ~> ('[Dual am, ap] ++ '[bm, Dual bm])
forall k (as :: [k]) (bs :: [k]) (cs :: [k]) (ds :: [k]).
Monoidal k =>
(as ~> bs) -> (cs ~> ds) -> (as ++ cs) ~> (bs ++ ds)
|| forall (as :: [k]) (bs :: [k]).
(Ob as, Ob bs) =>
(Fold as ~> Fold bs) -> Strictified as bs
forall {k} (as :: [k]) (bs :: [k]).
(Ob as, Ob bs) =>
(Fold as ~> Fold bs) -> Strictified as bs
Str @'[] @[bm, Dual bm] (forall (a :: k). (CompactClosed k, Ob a) => Unit ~> (a ** Dual a)
forall {k} (a :: k).
(CompactClosed k, Ob a) =>
Unit ~> (a ** Dual a)
dualityUnit @bm)
            (('[ap, Dual am] ++ '[]) ~> ('[Dual am, ap] ++ '[bm, Dual bm]))
-> (('[Dual am, ap] ++ '[bm, Dual bm])
    ~> (('[Dual am] ++ '[am, bp]) ++ '[Dual bm]))
-> ('[ap, Dual am] ++ '[])
   ~> (('[Dual am] ++ '[am, bp]) ++ '[Dual bm])
forall k (a :: k) (b :: k) (c :: k).
CategoryOf k =>
(a ~> b) -> (b ~> c) -> a ~> c
== forall (a :: [k]). (CategoryOf [k], Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @'[Dual am] Obj '[Dual am]
-> ('[ap, bm] ~> '[am, bp])
-> ('[Dual am] ++ '[ap, bm]) ~> ('[Dual am] ++ '[am, bp])
forall k (as :: [k]) (bs :: [k]) (cs :: [k]) (ds :: [k]).
Monoidal k =>
(as ~> bs) -> (cs ~> ds) -> (as ++ cs) ~> (bs ++ ds)
|| forall (as :: [k]) (bs :: [k]).
(Ob as, Ob bs) =>
(Fold as ~> Fold bs) -> Strictified as bs
forall {k} (as :: [k]) (bs :: [k]).
(Ob as, Ob bs) =>
(Fold as ~> Fold bs) -> Strictified as bs
Str @[ap, bm] @[am, bp] (ap ** bm) ~> (am ** bp)
Fold '[ap, bm] ~> Fold '[am, bp]
f (('[Dual am] ++ '[ap, bm]) ~> ('[Dual am] ++ '[am, bp]))
-> ('[Dual bm] ~> '[Dual bm])
-> (('[Dual am] ++ '[ap, bm]) ++ '[Dual bm])
   ~> (('[Dual am] ++ '[am, bp]) ++ '[Dual bm])
forall k (as :: [k]) (bs :: [k]) (cs :: [k]) (ds :: [k]).
Monoidal k =>
(as ~> bs) -> (cs ~> ds) -> (as ++ cs) ~> (bs ++ ds)
|| forall (a :: [k]). (CategoryOf [k], Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @'[Dual bm]
            (('[ap, Dual am] ++ '[])
 ~> (('[Dual am] ++ '[am, bp]) ++ '[Dual bm]))
-> ((('[Dual am] ++ '[am, bp]) ++ '[Dual bm])
    ~> (('[] ++ '[bp]) ++ '[Dual bm]))
-> ('[ap, Dual am] ++ '[]) ~> (('[] ++ '[bp]) ++ '[Dual bm])
forall k (a :: k) (b :: k) (c :: k).
CategoryOf k =>
(a ~> b) -> (b ~> c) -> a ~> c
== forall (as :: [k]) (bs :: [k]).
(Ob as, Ob bs) =>
(Fold as ~> Fold bs) -> Strictified as bs
forall {k} (as :: [k]) (bs :: [k]).
(Ob as, Ob bs) =>
(Fold as ~> Fold bs) -> Strictified as bs
Str @[Dual am, am] @'[] (forall (a :: k). (CompactClosed k, Ob a) => (Dual a ** a) ~> Unit
forall {k} (a :: k).
(CompactClosed k, Ob a) =>
(Dual a ** a) ~> Unit
dualityCounit @am) ('[Dual am, am] ~> '[])
-> ('[bp] ~> '[bp]) -> ('[Dual am, am] ++ '[bp]) ~> ('[] ++ '[bp])
forall k (as :: [k]) (bs :: [k]) (cs :: [k]) (ds :: [k]).
Monoidal k =>
(as ~> bs) -> (cs ~> ds) -> (as ++ cs) ~> (bs ++ ds)
|| forall (a :: [k]). (CategoryOf [k], Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @'[bp] (('[Dual am, am] ++ '[bp]) ~> ('[] ++ '[bp]))
-> ('[Dual bm] ~> '[Dual bm])
-> (('[Dual am, am] ++ '[bp]) ++ '[Dual bm])
   ~> (('[] ++ '[bp]) ++ '[Dual bm])
forall k (as :: [k]) (bs :: [k]) (cs :: [k]) (ds :: [k]).
Monoidal k =>
(as ~> bs) -> (cs ~> ds) -> (as ++ cs) ~> (bs ++ ds)
|| forall (a :: [k]). (CategoryOf [k], Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @'[Dual bm]