{-# 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 (($), type (~))
import Prelude qualified as P

import Proarrow.Adjunction (Adjunction (..), counitFromRepCounit, unitFromRepUnit)
import Proarrow.Category.Instance.Prof (Prof (..))
import Proarrow.Category.Instance.Sub (On, SUBCAT (..), Sub (..))
import Proarrow.Core
  ( CAT
  , CategoryOf (..)
  , Kind
  , OB
  , Profunctor (..)
  , Promonad (..)
  , arr
  , lmap
  , rmap
  , src
  , (//)
  , type (+->)
  )
import Proarrow.Functor (Functor (..))
import Proarrow.Monoid (Monoid (..))
import Proarrow.Object.BinaryProduct (Cartesian, PROD (..), Prod (..), fst, snd, (&&&), HasProducts, HasBinaryProducts (..))
import Proarrow.Object.Terminal (terminate, El)
import Proarrow.Profunctor.Forget (Forget)
import Proarrow.Profunctor.Product ((:*:) (..))
import Proarrow.Profunctor.Representable (Representable (..), dimapRep, repObj)
import Proarrow.Profunctor.Star (Star (..))
import Proarrow.Profunctor.Terminal (TerminalProfunctor (..))
import Proarrow.Category.Instance.Nat (Nat(..))
import Proarrow.Category.Monoidal.Applicative (Applicative (..))

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 :: PRO 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 (forall {j} {k} (p :: j +-> k) (b :: j) (a :: k).
(Representable p, Ob b) =>
(a ~> (p % b)) -> p a b
forall (p :: k +-> k) (b :: k) (a :: k).
(Representable p, Ob b) =>
(a ~> (p % b)) -> p a b
tabulate @(Free ob) (forall {j} {k} (p :: j +-> k) (a :: j).
(Representable p, Ob a) =>
Obj (p % a)
forall (p :: k +-> k) (a :: k).
(Representable p, Ob a) =>
Obj (p % a)
repObj @(Free ob) @a))

type FreeSub :: forall (ob :: OB k) -> k +-> SUBCAT ob
data FreeSub ob a b where
  FreeSub :: (ob a) => Free ob a b -> FreeSub ob (SUB a) b

instance (HasFree ob) => Profunctor (FreeSub ob) where
  dimap :: forall (c :: SUBCAT ob) (a :: SUBCAT ob) (b :: k) (d :: k).
(c ~> a) -> (b ~> d) -> FreeSub ob a b -> FreeSub ob c d
dimap = (c ~> a) -> (b ~> d) -> FreeSub ob a b -> FreeSub ob c d
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) (c :: k) (d :: j).
Representable p =>
(c ~> a) -> (b ~> d) -> p a b -> p c d
dimapRep
  (Ob a, Ob b) => r
r \\ :: forall (a :: SUBCAT ob) (b :: k) r.
((Ob a, Ob b) => r) -> FreeSub ob a b -> r
\\ FreeSub Free ob a b
p = r
(Ob a, Ob b) => r
(Ob a, Ob b) => r
r ((Ob a, Ob b) => r) -> Free ob a b -> r
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> Free ob a b -> r
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ Free ob a b
p

instance (HasFree ob) => Representable (FreeSub ob) where
  type FreeSub ob % a = SUB (Free ob % a)
  index :: forall (a :: SUBCAT ob) (b :: j).
FreeSub ob a b -> a ~> (FreeSub ob % b)
index (FreeSub Free ob a b
p) = (a ~> (Free ob % b)) -> Sub (~>) (SUB 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 (Free ob a b -> a ~> (Free ob % b)
forall (a :: j) (b :: j). Free ob a b -> a ~> (Free ob % b)
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
Representable p =>
p a b -> a ~> (p % b)
index Free ob a b
p) ((Ob a, Ob b) => Sub (~>) (SUB a) (SUB (Free ob % b)))
-> Free ob a b -> Sub (~>) (SUB a) (SUB (Free ob % b))
forall (a :: j) (b :: j) r. ((Ob a, Ob b) => r) -> Free ob a b -> r
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ Free ob a b
p
  tabulate :: forall (b :: j) (a :: SUBCAT ob).
Ob b =>
(a ~> (FreeSub ob % b)) -> FreeSub ob a b
tabulate (Sub a1 ~> b1
f) = Free ob a1 b -> FreeSub ob (SUB a1) b
forall {k} (ob :: k -> Constraint) (b :: k) (b :: k).
ob b =>
Free ob b b -> FreeSub ob (SUB b) b
FreeSub ((a1 ~> (Free ob % b)) -> Free ob a1 b
forall (b :: j) (a :: j).
Ob b =>
(a ~> (Free ob % b)) -> Free ob a b
forall {j} {k} (p :: j +-> k) (b :: j) (a :: k).
(Representable p, Ob b) =>
(a ~> (p % b)) -> p a b
tabulate a1 ~> b1
a1 ~> (Free ob % b)
f)
  repMap :: forall (a :: j) (b :: j).
(a ~> b) -> (FreeSub ob % a) ~> (FreeSub ob % b)
repMap 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 :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ a ~> b
f

instance (HasFree ob) => Adjunction (FreeSub ob) (Forget ob) where
  unit :: forall (a :: k). Ob a => (:.:) (Forget ob) (FreeSub ob) a a
unit = (a ~> (Forget ob % (FreeSub ob % a)))
-> (:.:) (Forget ob) (FreeSub ob) a a
forall {i} {j} (l :: i +-> j) (r :: j +-> i) (a :: i).
(Representable l, Representable r, Ob a) =>
(a ~> (r % (l % a))) -> (:.:) r l a a
unitFromRepUnit (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)
  counit :: (FreeSub ob :.: Forget ob) :~> (~>)
counit = (forall (c :: SUBCAT ob).
 Ob c =>
 (FreeSub ob % (Forget ob % c)) ~> c)
-> (FreeSub ob :.: Forget ob) :~> (~>)
forall {j} {k1} (l :: j +-> k1) (r :: k1 +-> j).
(Representable l, Representable r) =>
(forall (c :: k1). Ob c => (l % (r % c)) ~> c)
-> (l :.: r) :~> (~>)
counitFromRepCounit (((Free ob % UN SUB c) ~> UN SUB c)
-> Sub (~>) (SUB (Free ob % UN SUB c)) (SUB (UN SUB c))
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))

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 :: PRO 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 :: PRO 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 :: PRO 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 :: PRO 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 :: PRO 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 :: PRO 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 :: El 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 El a
a) = El b -> Ap f b
forall {k} (a :: k) (f :: k -> Type). El a -> Ap f a
Pure (a ~> b
f (a ~> b) -> El a -> El b
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. El 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 :: PRO 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 El a
a -> El a -> Ap b a
forall {k} (a :: k) (f :: k -> Type). El a -> Ap f a
Pure El 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 (Nat (Ap a) (Ap b) -> Ap a .~> Ap b
forall {k} {k1} (f :: k -> k1) (g :: k -> k1). Nat f g -> f .~> g
unNat ((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) -> 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) (Nat (Ap a) (Ap b) -> Ap a .~> Ap b
forall {k} {k1} (f :: k -> k1) (g :: k -> k1). Nat f g -> f .~> g
unNat ((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) -> 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 (HasProducts k, Functor f) => Applicative (Ap (f :: k -> Type)) where
  pure :: forall (a :: k). El a -> El (Ap f a)
pure El a
a () = El a -> Ap f a
forall {k} (a :: k) (f :: k -> Type). El a -> Ap f a
Pure El 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

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 El a
a) = El a -> El (f a)
forall (a :: k). El a -> El (f a)
forall {j} {k} (f :: j -> k) (a :: j).
Applicative f =>
El a -> El (f a)
pure El 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 (HasProducts 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 :: PRO 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 :: PRO 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 :: k) (a :: k) (b :: k) (d :: k).
(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 :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO 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 :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO 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 :: PRO j k) (b :: k) (d :: k) (a :: j).
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 :: PRO j k) (c :: j) (a :: j) (b :: k).
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 :: k) (b :: k) 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 :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) 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 :: k) (b :: k) r. ((Ob a, Ob b) => r) -> p a b -> r
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) 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 :: k) (b :: k) r.
((Ob a, Ob b) => r) -> FreePromonad p a b -> r
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) 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 :: PRO 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 :: PRO j k) (b :: k) (d :: k) (a :: j).
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 :: PRO 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 :: PRO k1 k2) (a :: k1) (b :: k2) r.
Profunctor p =>
p a b -> ((Ob a, Ob b) => r) -> r
// (FreePromonad a :~> FreePromonad b)
-> Prof (FreePromonad a) (FreePromonad b)
forall {k} {j} (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 {k} {k1} (p :: PRO k k1) (q :: PRO k k1).
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 {k} {k1} (p :: PRO k k1) (q :: PRO k k1).
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 :: PRO k k) (b :: PRO 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 {k} {j} (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 {k1} {k2} (a :: k2) (b :: k1) (p :: PRO k2 k1).
Profunctor p =>
p a b -> Obj a
src a a b
a))
  retract' :: forall (b :: PRO k k) (a :: PRO k k).
Promonad b =>
Free Promonad a b -> a ~> b
retract' (Star (Prof a :~> FreePromonad b
n)) = (a :~> b) -> Prof a b
forall {k} {j} (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 :: PRO 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 :: PRO 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 {k} {k1} (p :: PRO k k1) (q :: PRO k k1).
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 :: PRO k k -> Constraint) (a :: PRO k k).
(HasFree ob, ob a, Ob a) =>
(Free ob % a) ~> a
retract @Promonad) FreePromonad b a b
r

class (Ob (Lift c f a)) => ObLift c f k (a :: k)
instance (Ob (Lift c f a)) => ObLift c f k a
class (Ob (Retract c f a)) => ObRetract c f k (a :: f k)
instance (Ob (Retract c f a)) => ObRetract c f k (a :: f k)
class (forall a. ObLift c f k a, forall a. ObRetract c f k a) => ObLiftRetract c f k
instance (forall a. ObLift c f k a, forall a. ObRetract c f k a) => ObLiftRetract c f k

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

-- instance HasFreeK Monoidal [] where
--   type Lift Monoidal [] a = '[a]
--   type Retract Monoidal [] a = Fold a
--   liftK = singleton
--   retractK (Str f) = f

type FreeMonoid :: k +-> k -> k +-> k
data FreeMonoid p a b where
  Nil :: (Ob a, Ob b) => FreeMonoid p a b
  Cons :: p a b -> FreeMonoid p a b -> FreeMonoid p a b

instance (Profunctor p) => Monoid (PR (FreeMonoid p) :: PROD (k +-> k)) where
  mempty :: Unit ~> 'PR (FreeMonoid p)
mempty = Prof TerminalProfunctor (FreeMonoid p)
-> Prod Prof ('PR TerminalProfunctor) ('PR (FreeMonoid p))
forall {j} {k} (p :: j +-> k) (a1 :: k) (b1 :: j).
p a1 b1 -> Prod p ('PR a1) ('PR b1)
Prod ((TerminalProfunctor :~> FreeMonoid p)
-> Prof TerminalProfunctor (FreeMonoid p)
forall {k} {j} (p :: j +-> k) (q :: j +-> k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
Prof \TerminalProfunctor a b
t -> FreeMonoid p a b
(Ob a, Ob b) => FreeMonoid p a b
forall {k} (a :: k) (b :: k) (p :: k +-> k).
(Ob a, Ob b) =>
FreeMonoid p a b
Nil ((Ob a, Ob b) => FreeMonoid p a b)
-> TerminalProfunctor a b -> FreeMonoid p a b
forall (a :: k) (b :: k) r.
((Ob a, Ob b) => r) -> TerminalProfunctor a b -> r
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ TerminalProfunctor a b
t)
  mappend :: ('PR (FreeMonoid p) ** 'PR (FreeMonoid p)) ~> 'PR (FreeMonoid p)
mappend = Prof (FreeMonoid p :*: FreeMonoid p) (FreeMonoid p)
-> Prod
     Prof ('PR (FreeMonoid p :*: FreeMonoid p)) ('PR (FreeMonoid p))
forall {j} {k} (p :: j +-> k) (a1 :: k) (b1 :: j).
p a1 b1 -> Prod p ('PR a1) ('PR b1)
Prod (Prof (FreeMonoid p :*: FreeMonoid p) (FreeMonoid p)
 -> Prod
      Prof ('PR (FreeMonoid p :*: FreeMonoid p)) ('PR (FreeMonoid p)))
-> Prof (FreeMonoid p :*: FreeMonoid p) (FreeMonoid p)
-> Prod
     Prof ('PR (FreeMonoid p :*: FreeMonoid p)) ('PR (FreeMonoid p))
forall a b. (a -> b) -> a -> b
$ ((FreeMonoid p :*: FreeMonoid p) :~> FreeMonoid p)
-> Prof (FreeMonoid p :*: FreeMonoid p) (FreeMonoid p)
forall {k} {j} (p :: j +-> k) (q :: j +-> k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
Prof \case
    FreeMonoid p a b
Nil :*: FreeMonoid p a b
r -> FreeMonoid p a b
r
    Cons p a b
f FreeMonoid p a b
t :*: FreeMonoid p a b
r -> p a b -> FreeMonoid p a b -> FreeMonoid p a b
forall {k} (p :: k +-> k) (a :: k) (b :: k).
p a b -> FreeMonoid p a b -> FreeMonoid p a b
Cons p a b
f (Prof (FreeMonoid p :*: FreeMonoid p) (FreeMonoid p)
-> (FreeMonoid p :*: FreeMonoid p) :~> FreeMonoid p
forall {k} {k1} (p :: PRO k k1) (q :: PRO k k1).
Prof p q -> p :~> q
unProf (Prod
  Prof ('PR (FreeMonoid p :*: FreeMonoid p)) ('PR (FreeMonoid p))
-> Prof (FreeMonoid p :*: FreeMonoid p) (FreeMonoid p)
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
Prod p ('PR a) ('PR b) -> p a b
unProd ('PR (FreeMonoid p) ** 'PR (FreeMonoid p)) ~> 'PR (FreeMonoid p)
Prod
  Prof ('PR (FreeMonoid p :*: FreeMonoid p)) ('PR (FreeMonoid p))
forall {k} (m :: k). Monoid m => (m ** m) ~> m
mappend) (FreeMonoid p a b
t FreeMonoid p a b
-> FreeMonoid p a b -> (:*:) (FreeMonoid p) (FreeMonoid p) a b
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) (q :: PRO j k).
p a b -> q a b -> (:*:) p q a b
:*: FreeMonoid p a b
r))

data family FreeMonoidF (b :: k) :: k
instance
  ( Cartesian k
  , Representable (FreeMonoid (~>) :: k +-> k)
  , Ob (b :: k)
  , FreeMonoid (~>) % b ~ FreeMonoidF b
  , Ob (FreeMonoid (~>) % b)
  )
  => Monoid (FreeMonoidF b :: k)
  where
  mempty :: Unit ~> FreeMonoidF b
mempty = forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
Representable p =>
p a b -> a ~> (p % b)
forall (p :: PRO k k) (a :: k) (b :: k).
Representable p =>
p a b -> a ~> (p % b)
index @(FreeMonoid (~>)) @_ @b (Prof TerminalProfunctor (FreeMonoid (~>))
-> TerminalProfunctor :~> FreeMonoid (~>)
forall {k} {k1} (p :: PRO k k1) (q :: PRO k k1).
Prof p q -> p :~> q
unProf (Prod Prof ('PR TerminalProfunctor) ('PR (FreeMonoid (~>)))
-> Prof TerminalProfunctor (FreeMonoid (~>))
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
Prod p ('PR a) ('PR b) -> p a b
unProd Unit ~> 'PR (FreeMonoid (~>))
Prod Prof ('PR TerminalProfunctor) ('PR (FreeMonoid (~>)))
forall {k} (m :: k). Monoid m => Unit ~> m
mempty) TerminalProfunctor TerminalObject b
forall j k (a :: j) (b :: k).
(CategoryOf j, CategoryOf k, Ob a, Ob b) =>
TerminalProfunctor a b
TerminalProfunctor)
  mappend :: (FreeMonoidF b ** FreeMonoidF b) ~> FreeMonoidF b
mappend =
    forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
Representable p =>
p a b -> a ~> (p % b)
forall (p :: PRO k k) (a :: k) (b :: k).
Representable p =>
p a b -> a ~> (p % b)
index @(FreeMonoid (~>)) @_ @b
      ( Prof (FreeMonoid (~>) :*: FreeMonoid (~>)) (FreeMonoid (~>))
-> (FreeMonoid (~>) :*: FreeMonoid (~>)) :~> FreeMonoid (~>)
forall {k} {k1} (p :: PRO k k1) (q :: PRO k k1).
Prof p q -> p :~> q
unProf
          (Prod
  Prof
  ('PR (FreeMonoid (~>) :*: FreeMonoid (~>)))
  ('PR (FreeMonoid (~>)))
-> Prof (FreeMonoid (~>) :*: FreeMonoid (~>)) (FreeMonoid (~>))
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
Prod p ('PR a) ('PR b) -> p a b
unProd ('PR (FreeMonoid (~>)) ** 'PR (FreeMonoid (~>)))
~> 'PR (FreeMonoid (~>))
Prod
  Prof
  ('PR (FreeMonoid (~>) :*: FreeMonoid (~>)))
  ('PR (FreeMonoid (~>)))
forall {k} (m :: k). Monoid m => (m ** m) ~> m
mappend)
          ( ((FreeMonoidF b ** FreeMonoidF b) ~> (FreeMonoid (~>) % b))
-> FreeMonoid (~>) (FreeMonoidF b ** FreeMonoidF b) b
forall (b :: k) (a :: k).
Ob b =>
(a ~> (FreeMonoid (~>) % b)) -> FreeMonoid (~>) a b
forall {j} {k} (p :: j +-> k) (b :: j) (a :: k).
(Representable p, Ob b) =>
(a ~> (p % b)) -> p a b
tabulate (forall k (a :: k) (b :: k).
(HasBinaryProducts k, Ob a, Ob b) =>
(a && b) ~> a
fst @_ @(FreeMonoid (~>) % b) @(FreeMonoid (~>) % b))
              FreeMonoid (~>) (FreeMonoidF b ** FreeMonoidF b) b
-> FreeMonoid (~>) (FreeMonoidF b ** FreeMonoidF b) b
-> (:*:)
     (FreeMonoid (~>))
     (FreeMonoid (~>))
     (FreeMonoidF b ** FreeMonoidF b)
     b
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) (q :: PRO j k).
p a b -> q a b -> (:*:) p q a b
:*: ((FreeMonoidF b ** FreeMonoidF b) ~> (FreeMonoid (~>) % b))
-> FreeMonoid (~>) (FreeMonoidF b ** FreeMonoidF b) b
forall (b :: k) (a :: k).
Ob b =>
(a ~> (FreeMonoid (~>) % b)) -> FreeMonoid (~>) a b
forall {j} {k} (p :: j +-> k) (b :: j) (a :: k).
(Representable p, Ob b) =>
(a ~> (p % b)) -> p a b
tabulate (forall k (a :: k) (b :: k).
(HasBinaryProducts k, Ob a, Ob b) =>
(a && b) ~> b
snd @_ @(FreeMonoid (~>) % b) @(FreeMonoid (~>) % b))
          )
      )
instance (Profunctor p) => Profunctor (FreeMonoid p :: k +-> k) where
  dimap :: forall (c :: k) (a :: k) (b :: k) (d :: k).
(c ~> a) -> (b ~> d) -> FreeMonoid p a b -> FreeMonoid p c d
dimap c ~> a
l b ~> d
r FreeMonoid p a b
Nil = FreeMonoid p c d
(Ob c, Ob a) => FreeMonoid p c d
forall {k} (a :: k) (b :: k) (p :: k +-> k).
(Ob a, Ob b) =>
FreeMonoid p a b
Nil ((Ob c, Ob a) => FreeMonoid p c d) -> (c ~> a) -> FreeMonoid p c d
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ c ~> a
l ((Ob b, Ob d) => FreeMonoid p c d) -> (b ~> d) -> FreeMonoid p c d
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ b ~> d
r
  dimap c ~> a
l b ~> d
r (Cons p a b
h FreeMonoid p a b
t) = p c d -> FreeMonoid p c d -> FreeMonoid p c d
forall {k} (p :: k +-> k) (a :: k) (b :: k).
p a b -> FreeMonoid p a b -> FreeMonoid p a b
Cons ((c ~> a) -> (b ~> d) -> p a b -> p c d
forall (c :: k) (a :: k) (b :: k) (d :: k).
(c ~> a) -> (b ~> d) -> p a b -> p c d
forall {j} {k} (p :: PRO j k) (c :: j) (a :: j) (b :: k) (d :: k).
Profunctor p =>
(c ~> a) -> (b ~> d) -> p a b -> p c d
dimap c ~> a
l b ~> d
r p a b
h) ((c ~> a) -> (b ~> d) -> FreeMonoid p a b -> FreeMonoid p c d
forall (c :: k) (a :: k) (b :: k) (d :: k).
(c ~> a) -> (b ~> d) -> FreeMonoid p a b -> FreeMonoid p c d
forall {j} {k} (p :: PRO j k) (c :: j) (a :: j) (b :: k) (d :: k).
Profunctor p =>
(c ~> a) -> (b ~> d) -> p a b -> p c d
dimap c ~> a
l b ~> d
r FreeMonoid p a b
t)
  (Ob a, Ob b) => r
r \\ :: forall (a :: k) (b :: k) r.
((Ob a, Ob b) => r) -> FreeMonoid p a b -> r
\\ FreeMonoid p a b
Nil = r
(Ob a, Ob b) => r
r
  (Ob a, Ob b) => r
r \\ Cons p a b
h FreeMonoid p a b
_ = r
(Ob a, Ob b) => r
r ((Ob a, Ob b) => r) -> p a b -> r
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> p a b -> r
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ p a b
h

class (Monoid (FreeMonoid (~>) % b)) => FreeMonoidIsMonoid b
instance (Monoid (FreeMonoid (~>) % b)) => FreeMonoidIsMonoid b
instance
  (Representable (FreeMonoid (~>) :: k +-> k), forall (b :: k). (Ob b) => FreeMonoidIsMonoid b, Cartesian k)
  => HasFree (Monoid :: k -> Constraint)
  where
  type Free Monoid = FreeMonoid (~>)
  lift' :: forall (a :: k) (b :: k). (a ~> b) -> Free Monoid a b
lift' a ~> b
f = (a ~> b) -> FreeMonoid (~>) a b -> FreeMonoid (~>) a b
forall {k} (p :: k +-> k) (a :: k) (b :: k).
p a b -> FreeMonoid p a b -> FreeMonoid p a b
Cons a ~> b
f FreeMonoid (~>) a b
forall {k} (a :: k) (b :: k) (p :: k +-> k).
(Ob a, Ob b) =>
FreeMonoid p a b
Nil ((Ob a, Ob b) => FreeMonoid (~>) a b)
-> (a ~> b) -> FreeMonoid (~>) a b
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ a ~> b
f
  retract' :: forall (b :: k) (a :: k). Monoid b => Free Monoid a b -> a ~> b
retract' FreeMonoid (~>) a b
Free Monoid a b
Nil = Unit ~> b
TerminalObject ~> b
forall {k} (m :: k). Monoid m => Unit ~> m
mempty (TerminalObject ~> b) -> (a ~> TerminalObject) -> a ~> b
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. a ~> TerminalObject
forall (a :: k). Ob a => a ~> TerminalObject
forall k (a :: k).
(HasTerminalObject k, Ob a) =>
a ~> TerminalObject
terminate
  retract' (Cons a ~> b
h FreeMonoid (~>) a b
t) = (b ** b) ~> b
forall {k} (m :: k). Monoid m => (m ** m) ~> m
mappend ((b ** b) ~> b) -> (a ~> (b ** b)) -> a ~> b
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (a ~> b
h (a ~> b) -> (a ~> b) -> a ~> (b && b)
forall (a :: k) (x :: k) (y :: k).
(a ~> x) -> (a ~> y) -> a ~> (x && y)
forall k (a :: k) (x :: k) (y :: k).
HasBinaryProducts k =>
(a ~> x) -> (a ~> y) -> a ~> (x && y)
&&& 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' @Monoid FreeMonoid (~>) a b
Free Monoid a b
t)