module Plutarch.Extra.Category (
  PSemigroupoid ((#>>>)),
  PCategory (pidentity),
  pconst,
  (#<<<),
) where

import Plutarch.Extra.Profunctor (PProfunctor (PCoSubcategory, PContraSubcategory, prmap))

-- | @since 1.0.0
class (PProfunctor p) => PSemigroupoid (p :: (S -> Type) -> (S -> Type) -> S -> Type) where
  (#>>>) ::
    forall (a :: S -> Type) (b :: S -> Type) (c :: S -> Type) (s :: S).
    ( PContraSubcategory p a
    , PContraSubcategory p b
    , PCoSubcategory p b
    , PCoSubcategory p c
    ) =>
    Term s (p a b) ->
    Term s (p b c) ->
    Term s (p a c)

-- | @since 1.0.0
instance PSemigroupoid (:-->) where
  (#>>>) ::
    forall (a :: S -> Type) (b :: S -> Type) (c :: S -> Type) (s :: S).
    Term s (a :--> b) ->
    Term s (b :--> c) ->
    Term s (a :--> c)
  Term s (a :--> b)
t #>>> :: forall (a :: S -> Type) (b :: S -> Type) (c :: S -> Type) (s :: S).
Term s (a :--> b) -> Term s (b :--> c) -> Term s (a :--> c)
#>>> Term s (b :--> c)
t' = forall (s' :: S).
Term s' ((a :--> b) :--> ((b :--> c) :--> (a :--> c)))
go forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (a :--> b)
t forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (b :--> c)
t'
    where
      go ::
        forall (s' :: S).
        Term s' ((a :--> b) :--> (b :--> c) :--> (a :--> c))
      go :: forall (s' :: S).
Term s' ((a :--> b) :--> ((b :--> c) :--> (a :--> c)))
go = forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic forall a b. (a -> b) -> a -> b
$
        forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$ \Term s (a :--> b)
ab ->
          forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$ \Term s (b :--> c)
bc ->
            forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$ \Term s a
x -> Term s (b :--> c)
bc forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# (Term s (a :--> b)
ab forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s a
x)

-- | @since 1.0.0
class (PSemigroupoid p) => PCategory (p :: (S -> Type) -> (S -> Type) -> S -> Type) where
  pidentity ::
    forall (a :: S -> Type) (s :: S).
    ( PContraSubcategory p a
    , PCoSubcategory p a
    ) =>
    Term s (p a a)

-- | @since 1.0.0
instance PCategory (:-->) where
  pidentity :: forall (a :: S -> Type) (s :: S).
(PContraSubcategory (:-->) a, PCoSubcategory (:-->) a) =>
Term s (a :--> a)
pidentity = forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic forall a b. (a -> b) -> a -> b
$ forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a. a -> a
id

-- | @since 1.0.0
pconst ::
  forall
    (p :: (S -> Type) -> (S -> Type) -> S -> Type)
    (a :: S -> Type)
    (b :: S -> Type)
    (s :: S).
  ( PContraSubcategory p b
  , PCategory p
  , PCoSubcategory p b
  , PCoSubcategory p a
  ) =>
  Term s (a :--> p b a)
pconst :: forall (p :: (S -> Type) -> (S -> Type) -> S -> Type)
       (a :: S -> Type) (b :: S -> Type) (s :: S).
(PContraSubcategory p b, PCategory p, PCoSubcategory p b,
 PCoSubcategory p a) =>
Term s (a :--> p b a)
pconst = forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic forall a b. (a -> b) -> a -> b
$ forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$ \Term s a
x -> forall (p :: (S -> Type) -> (S -> Type) -> S -> Type)
       (a :: S -> Type) (c :: S -> Type) (d :: S -> Type) (s :: S).
(PProfunctor p, PContraSubcategory p a, PCoSubcategory p c,
 PCoSubcategory p d) =>
Term s ((c :--> d) :--> (p a c :--> p a d))
prmap forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# (forall (s' :: S). Term s' (a :--> (b :--> a))
go forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s a
x) forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# forall (p :: (S -> Type) -> (S -> Type) -> S -> Type)
       (a :: S -> Type) (s :: S).
(PCategory p, PContraSubcategory p a, PCoSubcategory p a) =>
Term s (p a a)
pidentity
  where
    go :: forall (s' :: S). Term s' (a :--> b :--> a)
    go :: forall (s' :: S). Term s' (a :--> (b :--> a))
go = forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic forall a b. (a -> b) -> a -> b
$ forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. a -> b -> a
const

-- | @since 1.0.0
(#<<<) ::
  forall
    (p :: (S -> Type) -> (S -> Type) -> S -> Type)
    (a :: S -> Type)
    (b :: S -> Type)
    (c :: S -> Type)
    (s :: S).
  ( PSemigroupoid p
  , PContraSubcategory p a
  , PContraSubcategory p b
  , PCoSubcategory p b
  , PCoSubcategory p c
  ) =>
  Term s (p b c) ->
  Term s (p a b) ->
  Term s (p a c)
Term s (p b c)
t #<<< :: forall (p :: (S -> Type) -> (S -> Type) -> S -> Type)
       (a :: S -> Type) (b :: S -> Type) (c :: S -> Type) (s :: S).
(PSemigroupoid p, PContraSubcategory p a, PContraSubcategory p b,
 PCoSubcategory p b, PCoSubcategory p c) =>
Term s (p b c) -> Term s (p a b) -> Term s (p a c)
#<<< Term s (p a b)
t' = Term s (p a b)
t' forall (p :: (S -> Type) -> (S -> Type) -> S -> Type)
       (a :: S -> Type) (b :: S -> Type) (c :: S -> Type) (s :: S).
(PSemigroupoid p, PContraSubcategory p a, PContraSubcategory p b,
 PCoSubcategory p b, PCoSubcategory p c) =>
Term s (p a b) -> Term s (p b c) -> Term s (p a c)
#>>> Term s (p b c)
t

infixr 1 #<<<