module Proarrow.Category.Instance.Free where

import Data.Kind (Type)

import Proarrow.Core (CAT, CategoryOf (..), Is, Profunctor (..), Promonad (..), UN, dimapDefault, (:~>))

infixr 4 :|

newtype FREE (g :: k -> k -> Type) = F k
type instance UN F (F k) = k

type Free :: CAT (FREE g)
data Free a b where
  FreeId :: Free (F a) (F a)
  (:|) :: g a b -> Free (F b :: FREE g) (F c) -> Free (F a :: FREE g) (F c)

class Rewrite g where
  rewriteAfterCons :: (Free :: CAT (FREE g)) :~> (Free :: CAT (FREE g))

instance (Rewrite g) => CategoryOf (FREE g) where
  type (~>) = Free
  type Ob a = Is F a

instance (Rewrite g) => Promonad (Free :: CAT (FREE g)) where
  id :: forall (a :: FREE g). Ob a => Free a a
id = Free a a
Free ('F (UN 'F a)) ('F (UN 'F a))
forall {k} {g :: k -> k -> Type} (a :: k). Free ('F a) ('F a)
FreeId
  Free b c
FreeId . :: forall (b :: FREE g) (c :: FREE g) (a :: FREE g).
Free b c -> Free a b -> Free a c
. Free a b
a = Free a b
Free a c
a
  Free b c
a . Free a b
FreeId = Free b c
Free a c
a
  Free b c
a . (g a b
g :| Free ('F b) ('F c)
b) = Free a c -> Free a c
forall {k} (g :: k -> k -> Type). Rewrite g => Free :~> Free
Free :~> Free
rewriteAfterCons (g a b
g g a b -> Free ('F b) ('F (UN 'F c)) -> Free ('F a) ('F (UN 'F c))
forall {k} (g :: k -> k -> Type) (a :: k) (b :: k) (c :: k).
g a b -> Free ('F b) ('F c) -> Free ('F a) ('F c)
:| (Free b c
Free b ('F (UN 'F c))
a Free b ('F (UN 'F c))
-> Free ('F b) b -> Free ('F b) ('F (UN 'F c))
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
forall (b :: FREE g) (c :: FREE g) (a :: FREE g).
Free b c -> Free a b -> Free a c
. Free ('F b) b
Free ('F b) ('F c)
b)) ((Ob b, Ob c) => Free a c) -> Free b c -> Free a c
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
forall (a :: FREE g) (b :: FREE g) r.
((Ob a, Ob b) => r) -> Free a b -> r
\\ Free b c
a

instance (Rewrite g) => Profunctor (Free :: CAT (FREE g)) where
  dimap :: forall (c :: FREE g) (a :: FREE g) (b :: FREE g) (d :: FREE g).
(c ~> a) -> (b ~> d) -> Free a b -> Free c d
dimap = (c ~> a) -> (b ~> d) -> Free a b -> Free c d
Free c a -> Free b d -> Free a b -> Free c d
forall {k} (p :: PRO k k) (c :: k) (a :: k) (b :: k) (d :: k).
Promonad p =>
p c a -> p b d -> p a b -> p c d
dimapDefault
  (Ob a, Ob b) => r
r \\ :: forall (a :: FREE g) (b :: FREE g) r.
((Ob a, Ob b) => r) -> Free a b -> r
\\ Free a b
FreeId = r
(Ob a, Ob b) => r
r
  (Ob a, Ob b) => r
r \\ g a b
_ :| Free ('F b) ('F c)
_ = r
(Ob a, Ob b) => r
r