{-# 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.Adjunction (Adjunction (..), counitFromRepCounit, unitFromRepUnit)
import Proarrow.Category.Instance.Nat (Nat (..))
import Proarrow.Category.Instance.Prof (Prof (..))
import Proarrow.Category.Instance.Sub (On, SUBCAT (..), Sub (..))
import Proarrow.Category.Monoidal (Monoidal (..), MonoidalProfunctor (..))
import Proarrow.Category.Monoidal.Applicative (Applicative (..))
import Proarrow.Category.Monoidal.Strictified (Fold)
import Proarrow.Core
  ( CAT
  , CategoryOf (..)
  , Kind
  , OB
  , Profunctor (..)
  , Promonad (..)
  , UN
  , arr
  , lmap
  , rmap
  , src
  , (//)
  , type (+->)
  )
import Proarrow.Functor (Functor (..))
import Proarrow.Monoid (Monoid (..))
import Proarrow.Profunctor.Forget (Forget (..))
import Proarrow.Profunctor.List (LIST (..), List (..))
import Proarrow.Profunctor.Representable (Representable (..), dimapRep, repObj)
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 (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 :: j) (d :: j).
(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 :: j) 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 :: j) (b :: j) r. ((Ob a, Ob b) => r) -> Free ob 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
\\ 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 :: j +-> k) (a :: k) (b :: j) 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 :: j +-> k) (a :: k) (b :: j) 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 :: 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 (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 (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. (CategoryOf k) => 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 LIST where
  type Lift Monoidal LIST a = L '[a]
  type Retract Monoidal LIST (a :: LIST k) = Fold (UN L a)
  liftK :: forall k (a :: k) (b :: k).
CategoryOf k =>
(a ~> b) -> Lift Monoidal LIST a ~> Lift Monoidal LIST b
liftK a ~> b
f = (a ~> b)
-> List (~>) (L '[]) (L '[]) -> List (~>) (L '[a]) (L '[b])
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 a ~> b
f List (~>) (L '[]) (L '[])
forall {j} {k} (p :: j +-> k). List p (L '[]) (L '[])
Nil
  retractK :: forall k (a :: LIST k) (b :: LIST k).
Monoidal k =>
(a ~> b) -> Retract Monoidal LIST a ~> Retract Monoidal LIST b
retractK a ~> b
List (~>) a b
Nil = Unit ~> Unit
Retract Monoidal LIST a ~> Retract Monoidal LIST b
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 Monoidal LIST a ~> Retract Monoidal LIST b
f
  retractK (Cons a ~> b
f fs :: List (~>) (L as1) (L bs1)
fs@Cons{}) = a ~> b
f (a ~> b)
-> (Retract Monoidal LIST (L (a : as1))
    ~> Retract Monoidal LIST (L (b : bs1)))
-> (a ** Retract Monoidal LIST (L (a : as1)))
   ~> (b ** Retract 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 (c :: Type -> Constraint) (f :: Type -> Type) k (a :: f k)
       (b :: f k).
(HasFreeK c f, c k) =>
(a ~> b) -> Retract c f a ~> Retract c f b
retractK @Monoidal L (a : as1) ~> L (b : bs1)
List (~>) (L as1) (L bs1)
fs