{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE FunctionalDependencies #-}

module Proarrow.Profunctor.Free where

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

import Proarrow.Category.Instance.IntConstruction (INT (..), IntConstruction (..), TracedMonoidal', toInt)
import Proarrow.Category.Instance.Nat (Nat (..), first)
import Proarrow.Category.Instance.Prof (Prof (..))
import Proarrow.Category.Instance.Sub (On, SUBCAT (..), Sub (..))
import Proarrow.Category.Monoidal (Monoidal (..), MonoidalProfunctor (..), swap)
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
  , src
  , (//)
  , type (+->)
  )
import Proarrow.Functor (Functor (..), FunctorForRep (..))
import Proarrow.Monoid (Monoid (..))
import Proarrow.Object.Dual (CompactClosed, Dual, dualObj, dualityCounit, dualityUnit)
import Proarrow.Profunctor.Corepresentable (Corep (..))
import Proarrow.Profunctor.List (LIST (..), List (..))
import Proarrow.Profunctor.Representable (Representable (..), trivialRep)
import Proarrow.Profunctor.Star (Star (..))

type HasFree :: forall {k}. (k -> Constraint) -> Constraint
class (CategoryOf k, Representable (Free ob), forall b. (Ob b) => ob (Free ob % b)) => HasFree (ob :: k -> Constraint) where
  type Free ob :: k +-> k
  lift' :: a ~> b -> Free ob a b
  retract' :: (ob b) => Free ob a b -> a ~> b

lift :: forall ob a. (HasFree ob, Ob a) => a ~> Free ob % a
lift :: forall {j} (ob :: j -> Constraint) (a :: j).
(HasFree ob, Ob a) =>
a ~> (Free ob % a)
lift = forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
Representable p =>
p a b -> a ~> (p % b)
forall (p :: j +-> j) (a :: j) (b :: j).
Representable p =>
p a b -> a ~> (p % b)
index @(Free ob) (forall {k} (ob :: k -> Constraint) (a :: k) (b :: k).
HasFree ob =>
(a ~> b) -> Free ob a b
forall (ob :: j -> Constraint) (a :: j) (b :: j).
HasFree ob =>
(a ~> b) -> Free ob a b
lift' @ob a ~> a
forall (a :: j). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id)

retract :: forall ob a. (HasFree ob, ob a, Ob a) => Free ob % a ~> a
retract :: forall {k} (ob :: k -> Constraint) (a :: k).
(HasFree ob, ob a, Ob a) =>
(Free ob % a) ~> a
retract = forall {k} (ob :: k -> Constraint) (b :: k) (a :: k).
(HasFree ob, ob b) =>
Free ob a b -> a ~> b
forall (ob :: k -> Constraint) (b :: k) (a :: k).
(HasFree ob, ob b) =>
Free ob a b -> a ~> b
retract' @ob Free ob (Free ob % a) a
forall {j} {k} (p :: j +-> k) (a :: j).
(Representable p, Ob a) =>
p (p % a) a
trivialRep

fold :: forall ob a b. (HasFree ob, ob b) => (a ~> b) -> Free ob % a ~> b
fold :: forall {k} (ob :: k -> Constraint) (a :: k) (b :: k).
(HasFree ob, ob b) =>
(a ~> b) -> (Free ob % a) ~> b
fold a ~> b
f = forall {k} (ob :: k -> Constraint) (b :: k) (a :: k).
(HasFree ob, ob b) =>
Free ob a b -> a ~> b
forall (ob :: k -> Constraint) (b :: k) (a :: k).
(HasFree ob, ob b) =>
Free ob a b -> a ~> b
retract' @ob ((a ~> b) -> Free ob (Free ob % a) a -> Free ob (Free ob % a) b
forall {j} {k} (p :: j +-> k) (b :: j) (d :: j) (a :: k).
Profunctor p =>
(b ~> d) -> p a b -> p a d
rmap a ~> b
f Free ob (Free ob % a) a
forall {j} {k} (p :: j +-> k) (a :: j).
(Representable p, Ob a) =>
p (p % a) a
trivialRep) ((Ob a, Ob b) => (Free ob % a) ~> b)
-> (a ~> b) -> (Free ob % a) ~> 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

data family FreeSub :: forall (ob :: OB k) -> k +-> SUBCAT ob
instance (HasFree ob) => FunctorForRep (FreeSub ob) where
  type FreeSub ob @ a = SUB (Free ob % a)
  fmap :: forall (a :: j) (b :: j).
(a ~> b) -> (FreeSub ob @ a) ~> (FreeSub ob @ b)
fmap a ~> b
f = ((Free ob % a) ~> (Free ob % b))
-> Sub (~>) (SUB (Free ob % a)) (SUB (Free ob % 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 {j} {k} (p :: j +-> k) (a :: j) (b :: j).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
forall (p :: j +-> j) (a :: j) (b :: j).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
repMap @(Free ob) a ~> b
f) ((Ob a, Ob b) => Sub (~>) (SUB (Free ob % a)) (SUB (Free ob % b)))
-> (a ~> b) -> Sub (~>) (SUB (Free ob % a)) (SUB (Free ob % b))
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
-- | By creating the right adjoint to the free functor,
-- we obtain the free-forgetful adjunction.
instance (HasFree ob) => Representable (Corep (FreeSub (ob :: OB k))) where
  type Corep (FreeSub ob) % a = UN SUB a
  index :: forall (a :: k) (b :: SUBCAT ob).
Corep (FreeSub ob) a b -> a ~> (Corep (FreeSub ob) % b)
index (Corep (Sub a1 ~> b1
f)) = a1 ~> b1
f (a1 ~> b1) -> (a ~> a1) -> a ~> b1
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
. forall {j} (ob :: j -> Constraint) (a :: j).
(HasFree ob, Ob a) =>
a ~> (Free ob % a)
forall (ob :: k -> Constraint) (a :: k).
(HasFree ob, Ob a) =>
a ~> (Free ob % a)
lift @ob
  tabulate :: forall (b :: SUBCAT ob) (a :: k).
Ob b =>
(a ~> (Corep (FreeSub ob) % b)) -> Corep (FreeSub ob) a b
tabulate a ~> (Corep (FreeSub ob) % b)
f = ((FreeSub ob @ a) ~> b) -> Corep (FreeSub ob) a b
forall {j} {k} (a :: j) (f :: j +-> k) (b :: k).
Ob a =>
((f @ a) ~> b) -> Corep f a b
Corep (((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 :: k -> Constraint) (a :: k).
(HasFree ob, ob a, Ob a) =>
(Free ob % a) ~> a
forall (ob :: k -> Constraint) (a :: k).
(HasFree ob, ob a, Ob a) =>
(Free ob % a) ~> a
retract @ob ((Free ob % UN SUB b) ~> UN SUB b)
-> ((Free ob % a) ~> (Free ob % UN SUB b))
-> (Free ob % a) ~> UN SUB 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
. forall {j} {k} (p :: j +-> k) (a :: j) (b :: j).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
forall (p :: k +-> k) (a :: k) (b :: k).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
repMap @(Free ob) a ~> UN SUB b
a ~> (Corep (FreeSub ob) % b)
f)) ((Ob a, Ob (UN SUB b)) => Corep (FreeSub ob) a b)
-> (a ~> UN SUB b) -> Corep (FreeSub ob) a 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 ~> (Corep (FreeSub ob) % b)
f
  repMap :: forall (a :: SUBCAT ob) (b :: SUBCAT ob).
(a ~> b) -> (Corep (FreeSub ob) % a) ~> (Corep (FreeSub ob) % b)
repMap (Sub a1 ~> b1
f) = a1 ~> b1
(Corep (FreeSub ob) % a) ~> (Corep (FreeSub ob) % b)
f

instance HasFree P.Monoid where
  type Free P.Monoid = Star []
  lift' :: forall a b. (a ~> b) -> Free Monoid a b
lift' a ~> b
f = (a ~> [b]) -> Star [] a b
forall {k1} {k2} (b :: k1) (a :: k2) (f :: k1 -> k2).
Ob b =>
(a ~> f b) -> Star f a b
Star ((b -> [b] -> [b]
forall a. a -> [a] -> [a]
: []) (b -> [b]) -> (a -> b) -> a -> [b]
forall b c a. (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 -> b
f)
  retract' :: forall b a. Monoid b => Free Monoid a b -> a ~> b
retract' (Star a ~> [b]
f) = [b] -> b
forall a. Monoid a => [a] -> a
P.mconcat ([b] -> b) -> (a -> [b]) -> a -> b
forall b c a. (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 -> [b]
f

instance HasFree Semigroup where
  type Free Semigroup = Star NonEmpty
  lift' :: forall a b. (a ~> b) -> Free Semigroup a b
lift' a ~> b
f = (a ~> NonEmpty b) -> Star NonEmpty a b
forall {k1} {k2} (b :: k1) (a :: k2) (f :: k1 -> k2).
Ob b =>
(a ~> f b) -> Star f a b
Star ((b -> [b] -> NonEmpty b
forall a. a -> [a] -> NonEmpty a
:| []) (b -> NonEmpty b) -> (a -> b) -> a -> NonEmpty b
forall b c a. (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 -> b
f)
  retract' :: forall b a. Semigroup b => Free Semigroup a b -> a ~> b
retract' (Star a ~> NonEmpty b
f) = NonEmpty b -> b
forall a. Semigroup a => NonEmpty a -> a
sconcat (NonEmpty b -> b) -> (a -> NonEmpty b) -> a -> b
forall b c a. (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 ~> NonEmpty b
a -> NonEmpty b
f

instance HasFree (P.Monoid `On` Semigroup) where
  type Free (P.Monoid `On` Semigroup) = Sub (Star Maybe) :: CAT (SUBCAT Semigroup)
  lift' :: forall (a :: SUBCAT Semigroup) (b :: SUBCAT Semigroup).
(a ~> b) -> Free (On Monoid Semigroup) a b
lift' (Sub a1 -> b1
f) = Star Maybe a1 b1 -> Sub (Star Maybe) (SUB 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 ~> Maybe b1) -> Star Maybe a1 b1
forall {k1} {k2} (b :: k1) (a :: k2) (f :: k1 -> k2).
Ob b =>
(a ~> f b) -> Star f a b
Star (b1 -> Maybe b1
forall a. a -> Maybe a
Just (b1 -> Maybe b1) -> (a1 -> b1) -> a1 -> Maybe b1
forall b c a. (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
. a1 -> b1
f))
  retract' :: forall (b :: SUBCAT Semigroup) (a :: SUBCAT Semigroup).
On Monoid Semigroup b =>
Free (On Monoid Semigroup) a b -> a ~> b
retract' (Sub (Star a1 ~> Maybe b1
f)) = (a1 -> b1) -> Sub (->) (SUB 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 (b1 -> Maybe b1 -> b1
forall a. a -> Maybe a -> a
fromMaybe b1
forall a. Monoid a => a
P.mempty (Maybe b1 -> b1) -> (a1 -> Maybe b1) -> a1 -> b1
forall b c a. (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
. a1 ~> Maybe b1
a1 -> Maybe 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 {k1} {k} (f :: k1 -> k -> Type) (c :: k) (a :: k1)
       (b :: k1).
(Functor f, 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 {k1} {k} (f :: k1 -> k -> Type) (c :: k) (a :: k1)
       (b :: k1).
(Functor f, 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, 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 :: (k -> Type) -> Constraint) where
  type Free Applicative = Star Ap
  lift' :: forall (a :: k -> Type) (b :: k -> Type).
(a ~> b) -> Free Applicative a b
lift' (Nat a .~> b
f) = (a ~> Ap b) -> Star Ap a b
forall {k1} {k2} (b :: k1) (a :: k2) (f :: k1 -> k2).
Ob b =>
(a ~> f b) -> Star f a b
Star ((a .~> Ap b) -> Nat a (Ap b)
forall {j} {k} (f :: j -> k) (g :: j -> k).
(Functor f, Functor g) =>
(f .~> g) -> Nat f g
Nat (b a -> Ap b a
forall {k} (f :: k -> Type) (a :: k). f a -> Ap f a
Eff (b a -> Ap b a) -> (a a -> b a) -> a a -> Ap b a
forall b c a. (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 a ~> b a
a a -> b a
a .~> b
f))
  retract' :: forall (b :: k -> Type) (a :: k -> Type).
Applicative b =>
Free Applicative a b -> a ~> b
retract' (Star (Nat a .~> Ap b
f)) = (a .~> b) -> Nat a 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
forall {k} (f :: k -> Type) (a :: k).
Applicative f =>
Ap f a -> f a
retractAp (Ap b a -> b a) -> (a a -> Ap b a) -> a a -> b a
forall b c a. (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 a ~> Ap b a
a a -> Ap b a
a .~> Ap b
f)

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

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 b b
p FreePromonad p a b
q) = p b d -> FreePromonad p c b -> FreePromonad p c d
forall {k} (p :: k -> k -> Type) (b :: k) (c :: k) (a :: k).
p b c -> FreePromonad p a b -> FreePromonad p a c
Comp ((b ~> d) -> p b b -> p b 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 p b b
p) ((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 c ~> a
l FreePromonad p a 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 b b
p FreePromonad p a b
q = r
(Ob a, Ob b) => r
(Ob b, Ob b) => r
r ((Ob b, Ob b) => r) -> p b 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 b b
p ((Ob a, Ob b) => r) -> FreePromonad p a 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 a 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
  Unit b ~> c
f . :: forall (b :: k) (c :: k) (a :: k).
FreePromonad p b c -> FreePromonad p a b -> FreePromonad p a c
. FreePromonad p a b
q = (b ~> c) -> FreePromonad p a b -> FreePromonad p a c
forall {j} {k} (p :: j +-> k) (b :: j) (d :: j) (a :: k).
Profunctor p =>
(b ~> d) -> p a b -> p a d
rmap b ~> c
f FreePromonad p a b
q
  Comp p b c
r FreePromonad p b b
p . FreePromonad p a b
q = p b c -> FreePromonad p a b -> FreePromonad p a c
forall {k} (p :: k -> k -> Type) (b :: k) (c :: k) (a :: k).
p b c -> FreePromonad p a b -> FreePromonad p a c
Comp p b c
r (FreePromonad p b b
p FreePromonad p b b -> FreePromonad p a b -> FreePromonad p a b
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 a b
q)
instance Functor FreePromonad where
  map :: forall (a :: k -> k -> Type) (b :: k -> k -> Type).
(a ~> b) -> FreePromonad a ~> FreePromonad b
map a ~> b
n =
    a ~> b
Prof a b
n Prof a b
-> ((Ob a, Ob b) => Prof (FreePromonad a) (FreePromonad b))
-> Prof (FreePromonad a) (FreePromonad b)
forall {k1} {k2} (p :: k1 +-> k2) (a :: k2) (b :: k1) r.
Profunctor p =>
p a b -> ((Ob a, Ob b) => r) -> r
// (FreePromonad a :~> FreePromonad b)
-> Prof (FreePromonad a) (FreePromonad b)
forall {j} {k} (p :: j +-> k) (q :: j +-> k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
Prof \case
      Unit a ~> b
g -> (a ~> b) -> FreePromonad b a b
forall {k} (a :: k) (b :: k) (p :: k -> k -> Type).
(a ~> b) -> FreePromonad p a b
Unit a ~> b
g
      Comp a b b
p FreePromonad a a b
q -> b b b -> FreePromonad b a b -> FreePromonad b a b
forall {k} (p :: k -> k -> Type) (b :: k) (c :: k) (a :: k).
p b c -> FreePromonad p a b -> FreePromonad p a c
Comp (Prof a b -> a :~> b
forall {k1} {k} (p :: k1 +-> k) (q :: k1 +-> k).
Prof p q -> p :~> q
unProf a ~> b
Prof a b
n a b b
p) (Prof (FreePromonad a) (FreePromonad b)
-> FreePromonad a :~> FreePromonad b
forall {k1} {k} (p :: k1 +-> k) (q :: k1 +-> k).
Prof p q -> p :~> q
unProf ((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 -> Type) (b :: k -> k -> Type).
(a ~> b) -> FreePromonad a ~> FreePromonad b
map a ~> b
n) FreePromonad a a b
q)
instance HasFree Promonad where
  type Free Promonad = Star FreePromonad
  lift' :: forall (a :: k +-> k) (b :: k +-> k). (a ~> b) -> Free Promonad a b
lift' (Prof a :~> b
f) = (a ~> FreePromonad b) -> Star FreePromonad a b
forall {k1} {k2} (b :: k1) (a :: k2) (f :: k1 -> k2).
Ob b =>
(a ~> f b) -> Star f a b
Star ((a :~> FreePromonad b) -> Prof a (FreePromonad b)
forall {j} {k} (p :: j +-> k) (q :: j +-> k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
Prof \a a b
a -> a a b -> b a b
a :~> b
f a a b
a b a b -> FreePromonad b a a -> FreePromonad b a b
forall {k} (p :: k -> k -> Type) (b :: k) (c :: k) (a :: k).
p b c -> FreePromonad p a b -> FreePromonad p a c
`Comp` (a ~> a) -> FreePromonad b a a
forall {k} (a :: k) (b :: k) (p :: k -> k -> Type).
(a ~> b) -> FreePromonad p a b
Unit (a a b -> a ~> a
forall {j} {k} (a :: k) (b :: j) (p :: j +-> k).
Profunctor p =>
p a b -> Obj a
src a a b
a))
  retract' :: forall (b :: k +-> k) (a :: k +-> k).
Promonad b =>
Free Promonad a b -> a ~> b
retract' (Star (Prof a :~> FreePromonad b
n)) = (a :~> b) -> Prof a b
forall {j} {k} (p :: j +-> k) (q :: j +-> k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
Prof \a a b
p -> case a a b -> FreePromonad b a b
a :~> FreePromonad b
n a a b
p of
    Unit a ~> b
f -> (a ~> b) -> b a b
forall {k} (p :: k +-> k) (a :: k) (b :: k).
Promonad p =>
(a ~> b) -> p a b
arr a ~> b
f
    Comp b b b
q FreePromonad b a b
r -> b b b
q b b b -> b a b -> b a b
forall (b :: k) (c :: k) (a :: k). b b c -> b a b -> 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
. Prof (FreePromonad b) b -> FreePromonad b :~> b
forall {k1} {k} (p :: k1 +-> k) (q :: k1 +-> k).
Prof p q -> p :~> q
unProf (forall {k} (ob :: k -> Constraint) (a :: k).
(HasFree ob, ob a, Ob a) =>
(Free ob % a) ~> a
forall (ob :: (k +-> k) -> Constraint) (a :: k +-> k).
(HasFree ob, ob a, Ob a) =>
(Free ob % a) ~> a
retract @Promonad) FreePromonad b a b
r

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).
TracedMonoidal' k =>
(a ~> b) -> 'I a Unit ~> 'I b Unit
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]