{-# LANGUAGE AllowAmbiguousTypes #-}
{-# OPTIONS_GHC -Wno-orphans #-}

module Proarrow.Category.Monoidal.CopyDiscard where

import Data.Kind (Type)

import Proarrow.Category (Supplies)
import Proarrow.Category.Instance.Product ((:**:) (..))
import Proarrow.Category.Instance.Sub (SUBCAT, Sub (..), SubMonoidal)
import Proarrow.Category.Monoidal
  ( Monoidal (..)
  , MonoidalProfunctor (..)
  , SymMonoidal (..)
  , leftUnitorWith
  , rightUnitorWith
  )
import Proarrow.Category.Monoidal.Strictified (Strictified (..), listCase)
import Proarrow.Core (CategoryOf (..), OB, Profunctor (..), Promonad (..), obj)
import Proarrow.Limit.BinaryProduct (HasProducts, PROD (..))
import Proarrow.Monoid (Comonoid (..))

class (Monoidal k) => CopyDiscard k where
  copy :: (Ob (a :: k)) => a ~> a ** a
  default copy :: (k `Supplies` Comonoid) => (Ob (a :: k)) => a ~> a ** a
  copy = a ~> (a ** a)
forall {k :: Kind} (c :: k). Comonoid c => c ~> (c ** c)
comult
  discard :: (Ob (a :: k)) => a ~> Unit
  default discard :: (k `Supplies` Comonoid) => (Ob (a :: k)) => a ~> Unit
  discard = a ~> Unit
forall {k :: Kind} (c :: k). Comonoid c => c ~> Unit
counit

copyS :: (CopyDiscard k, Ob (a :: k)) => '[a] ~> '[a, a]
copyS :: forall (k :: Kind) (a :: k).
(CopyDiscard k, Ob a) =>
'[a] ~> '[a, a]
copyS = (Fold '[a] ~> Fold '[a, a]) -> Strictified '[a] '[a, a]
forall {k :: Kind} (as :: [k]) (bs :: [k]).
(Ob as, Ob bs) =>
(Fold as ~> Fold bs) -> Strictified as bs
Str a ~> (a ** a)
Fold '[a] ~> Fold '[a, a]
forall (a :: k). Ob a => a ~> (a ** a)
forall (k :: Kind) (a :: k). (CopyDiscard k, Ob a) => a ~> (a ** a)
copy

discardS :: (CopyDiscard k, Ob (a :: k)) => '[a] ~> '[]
discardS :: forall (k :: Kind) (a :: k). (CopyDiscard k, Ob a) => '[a] ~> '[]
discardS = (Fold '[a] ~> Fold '[]) -> Strictified '[a] '[]
forall {k :: Kind} (as :: [k]) (bs :: [k]).
(Ob as, Ob bs) =>
(Fold as ~> Fold bs) -> Strictified as bs
Str a ~> Unit
Fold '[a] ~> Fold '[]
forall (a :: k). Ob a => a ~> Unit
forall (k :: Kind) (a :: k). (CopyDiscard k, Ob a) => a ~> Unit
discard

instance (HasProducts k) => CopyDiscard (PROD k)
instance CopyDiscard Type
instance CopyDiscard ()
instance (CopyDiscard j, CopyDiscard k) => CopyDiscard (j, k) where
  copy :: forall (a :: (j, k)). Ob a => a ~> (a ** a)
copy = (Fst @ a) ~> ((Fst @ a) ** (Fst @ a))
forall (a :: j). Ob a => a ~> (a ** a)
forall (k :: Kind) (a :: k). (CopyDiscard k, Ob a) => a ~> (a ** a)
copy ((Fst @ a) ~> ((Fst @ a) ** (Fst @ a)))
-> ((Snd @ a) ~> ((Snd @ a) ** (Snd @ a)))
-> (:**:)
     (~>)
     (~>)
     '(Fst @ a, Snd @ a)
     '((Fst @ a) ** (Fst @ a), (Snd @ a) ** (Snd @ a))
forall {j1 :: Kind} {k1 :: Kind} {j2 :: Kind} {k2 :: Kind}
       (c :: j1 +-> k1) (a1 :: k1) (b1 :: j1) (d :: j2 +-> k2) (a2 :: k2)
       (b2 :: j2).
c a1 b1 -> d a2 b2 -> (:**:) c d '(a1, a2) '(b1, b2)
:**: (Snd @ a) ~> ((Snd @ a) ** (Snd @ a))
forall (a :: k). Ob a => a ~> (a ** a)
forall (k :: Kind) (a :: k). (CopyDiscard k, Ob a) => a ~> (a ** a)
copy
  discard :: forall (a :: (j, k)). Ob a => a ~> Unit
discard = (Fst @ a) ~> Unit
forall (a :: j). Ob a => a ~> Unit
forall (k :: Kind) (a :: k). (CopyDiscard k, Ob a) => a ~> Unit
discard ((Fst @ a) ~> Unit)
-> ((Snd @ a) ~> Unit)
-> (:**:) (~>) (~>) '(Fst @ a, Snd @ a) '(Unit, Unit)
forall {j1 :: Kind} {k1 :: Kind} {j2 :: Kind} {k2 :: Kind}
       (c :: j1 +-> k1) (a1 :: k1) (b1 :: j1) (d :: j2 +-> k2) (a2 :: k2)
       (b2 :: j2).
c a1 b1 -> d a2 b2 -> (:**:) c d '(a1, a2) '(b1, b2)
:**: (Snd @ a) ~> Unit
forall (a :: k). Ob a => a ~> Unit
forall (k :: Kind) (a :: k). (CopyDiscard k, Ob a) => a ~> Unit
discard

instance (SubMonoidal ob, CopyDiscard k) => CopyDiscard (SUBCAT (ob :: OB k)) where
  copy :: forall (a :: SUBCAT ob). Ob a => a ~> (a ** a)
copy = (UN SUB a ~> (UN SUB a ** UN SUB a))
-> Sub (~>) (SUB (UN SUB a)) (SUB (UN SUB a ** UN SUB a))
forall {k :: Kind} (ob :: OB k) (a1 :: k) (b1 :: k) (p :: CAT k).
(ob a1, ob b1) =>
p a1 b1 -> Sub p (SUB a1) (SUB b1)
Sub UN SUB a ~> (UN SUB a ** UN SUB a)
forall (a :: k). Ob a => a ~> (a ** a)
forall (k :: Kind) (a :: k). (CopyDiscard k, Ob a) => a ~> (a ** a)
copy
  discard :: forall (a :: SUBCAT ob). Ob a => a ~> Unit
discard = (UN SUB a ~> Unit) -> Sub (~>) (SUB (UN SUB a)) (SUB Unit)
forall {k :: Kind} (ob :: OB k) (a1 :: k) (b1 :: k) (p :: CAT k).
(ob a1, ob b1) =>
p a1 b1 -> Sub p (SUB a1) (SUB b1)
Sub UN SUB a ~> Unit
forall (a :: k). Ob a => a ~> Unit
forall (k :: Kind) (a :: k). (CopyDiscard k, Ob a) => a ~> Unit
discard

instance (SymMonoidal k, CopyDiscard k) => CopyDiscard [k] where
  copy :: forall (a :: [k]). Ob a => a ~> (a ** a)
copy @as0 =
    forall (as :: [k]) (r :: Kind).
IsList as =>
((as ~ '[]) => r)
-> (forall (a :: k). (Ob a, as ~ '[a]) => r)
-> (forall (b :: k) (bs :: [k]) (c :: k) (cs :: [k]).
    (Ob b, Ob bs, Ob cs, as ~ (b : bs), bs ~ (c : cs)) =>
    r)
-> r
forall {k :: Kind} (as :: [k]) (r :: Kind).
IsList as =>
((as ~ '[]) => r)
-> (forall (a :: k). (Ob a, as ~ '[a]) => r)
-> (forall (b :: k) (bs :: [k]) (c :: k) (cs :: [k]).
    (Ob b, Ob bs, Ob cs, as ~ (b : bs), bs ~ (c : cs)) =>
    r)
-> r
listCase @as0
      Strictified a (a ++ a)
Strictified '[] '[]
(a ~ '[]) => Strictified a (a ++ a)
forall (a :: [k]). Ob a => Strictified a a
forall {k :: Kind} (p :: k +-> k) (a :: k).
(Promonad p, Ob a) =>
p a a
id
      (\ @a -> forall (as :: [k]) (bs :: [k]).
(Ob as, Ob bs) =>
(Fold as ~> Fold bs) -> Strictified as bs
forall {k :: Kind} (as :: [k]) (bs :: [k]).
(Ob as, Ob bs) =>
(Fold as ~> Fold bs) -> Strictified as bs
Str @'[a] @'[a, a] a ~> (a ** a)
Fold '[a] ~> Fold '[a, a]
forall (a :: k). Ob a => a ~> (a ** a)
forall (k :: Kind) (a :: k). (CopyDiscard k, Ob a) => a ~> (a ** a)
copy)
      ( \ @a @as ->
          (forall (a :: [k]). (CategoryOf [k], Ob a) => Obj a
forall {k :: Kind} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @'[a] Strictified '[b] '[b]
-> Strictified
     ((b : c : cs) ++ (c : cs)) (c : (cs ++ (b : c : cs)))
-> Strictified
     ('[b] ** ((b : c : cs) ++ (c : cs)))
     ('[b] ** (c : (cs ++ (b : c : cs))))
forall (x1 :: [k]) (x2 :: [k]) (y1 :: [k]) (y2 :: [k]).
Strictified x1 x2
-> Strictified y1 y2 -> Strictified (x1 ** y1) (x2 ** y2)
forall {j :: Kind} {k :: Kind} (p :: j +-> k) (x1 :: k) (x2 :: j)
       (y1 :: k) (y2 :: j).
MonoidalProfunctor p =>
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
** (forall (k :: Kind) (a :: k) (b :: k) (c :: k).
(Monoidal k, Ob a, Ob b, Ob c) =>
((a ** b) ** c) ~> (a ** (b ** c))
associator @_ @as @'[a] @as Strictified
  (c : ((cs ++ '[b]) ++ (c : cs))) (c : (cs ++ (b : c : cs)))
-> Strictified
     ((b : c : cs) ++ (c : cs)) (c : ((cs ++ '[b]) ++ (c : cs)))
-> Strictified
     ((b : c : cs) ++ (c : cs)) (c : (cs ++ (b : c : cs)))
forall (b :: [k]) (c :: [k]) (a :: [k]).
Strictified b c -> Strictified a b -> Strictified a c
forall {k :: Kind} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (forall (k :: Kind) (a :: k) (b :: k).
(SymMonoidal k, Ob a, Ob b) =>
(a ** b) ~> (b ** a)
swap @[k] @'[a] @as Strictified (b : c : cs) (c : (cs ++ '[b]))
-> Strictified (c : cs) (c : cs)
-> Strictified
     ((b : c : cs) ** (c : cs)) ((c : (cs ++ '[b])) ** (c : cs))
forall (x1 :: [k]) (x2 :: [k]) (y1 :: [k]) (y2 :: [k]).
Strictified x1 x2
-> Strictified y1 y2 -> Strictified (x1 ** y1) (x2 ** y2)
forall {j :: Kind} {k :: Kind} (p :: j +-> k) (x1 :: k) (x2 :: j)
       (y1 :: k) (y2 :: j).
MonoidalProfunctor p =>
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
** forall (a :: [k]). (CategoryOf [k], Ob a) => Obj a
forall {k :: Kind} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @as)))
            Strictified
  ('[b] ++ ((b : c : cs) ++ (c : cs))) (b : c : (cs ++ (b : c : cs)))
-> Strictified a ('[b] ++ ((b : c : cs) ++ (c : cs)))
-> Strictified a (b : c : (cs ++ (b : c : cs)))
forall (b :: [k]) (c :: [k]) (a :: [k]).
Strictified b c -> Strictified a b -> Strictified a c
forall {k :: Kind} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (forall (as :: [k]) (bs :: [k]).
(Ob as, Ob bs) =>
(Fold as ~> Fold bs) -> Strictified as bs
forall {k :: Kind} (as :: [k]) (bs :: [k]).
(Ob as, Ob bs) =>
(Fold as ~> Fold bs) -> Strictified as bs
Str @'[a] @'[a, a] b ~> (b ** b)
Fold '[b] ~> Fold '[b, b]
forall (a :: k). Ob a => a ~> (a ** a)
forall (k :: Kind) (a :: k). (CopyDiscard k, Ob a) => a ~> (a ** a)
copy Strictified '[b] '[b, b]
-> Strictified (c : cs) (c : (cs ++ (c : cs)))
-> Strictified
     ('[b] ** (c : cs)) ('[b, b] ** (c : (cs ++ (c : cs))))
forall (x1 :: [k]) (x2 :: [k]) (y1 :: [k]) (y2 :: [k]).
Strictified x1 x2
-> Strictified y1 y2 -> Strictified (x1 ** y1) (x2 ** y2)
forall {j :: Kind} {k :: Kind} (p :: j +-> k) (x1 :: k) (x2 :: j)
       (y1 :: k) (y2 :: j).
MonoidalProfunctor p =>
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
** (c : cs) ~> ((c : cs) ** (c : cs))
Strictified (c : cs) (c : (cs ++ (c : cs)))
forall (a :: [k]). Ob a => a ~> (a ** a)
forall (k :: Kind) (a :: k). (CopyDiscard k, Ob a) => a ~> (a ** a)
copy)
      )
  discard :: forall (a :: [k]). Ob a => a ~> Unit
discard @as =
    forall (as :: [k]) (r :: Kind).
IsList as =>
((as ~ '[]) => r)
-> (forall (a :: k). (Ob a, as ~ '[a]) => r)
-> (forall (b :: k) (bs :: [k]) (c :: k) (cs :: [k]).
    (Ob b, Ob bs, Ob cs, as ~ (b : bs), bs ~ (c : cs)) =>
    r)
-> r
forall {k :: Kind} (as :: [k]) (r :: Kind).
IsList as =>
((as ~ '[]) => r)
-> (forall (a :: k). (Ob a, as ~ '[a]) => r)
-> (forall (b :: k) (bs :: [k]) (c :: k) (cs :: [k]).
    (Ob b, Ob bs, Ob cs, as ~ (b : bs), bs ~ (c : cs)) =>
    r)
-> r
listCase @as
      Strictified a '[]
Strictified '[] '[]
(a ~ '[]) => Strictified a '[]
forall (a :: [k]). Ob a => Strictified a a
forall {k :: Kind} (p :: k +-> k) (a :: k).
(Promonad p, Ob a) =>
p a a
id
      ((Fold a ~> Fold '[]) -> Strictified a '[]
forall {k :: Kind} (as :: [k]) (bs :: [k]).
(Ob as, Ob bs) =>
(Fold as ~> Fold bs) -> Strictified as bs
Str a ~> Unit
Fold a ~> Fold '[]
forall (a :: k). Ob a => a ~> Unit
forall (k :: Kind) (a :: k). (CopyDiscard k, Ob a) => a ~> Unit
discard)
      (\ @a -> forall (as :: [k]) (bs :: [k]).
(Ob as, Ob bs) =>
(Fold as ~> Fold bs) -> Strictified as bs
forall {k :: Kind} (as :: [k]) (bs :: [k]).
(Ob as, Ob bs) =>
(Fold as ~> Fold bs) -> Strictified as bs
Str @'[a] @'[] b ~> Unit
Fold '[b] ~> Fold '[]
forall (a :: k). Ob a => a ~> Unit
forall (k :: Kind) (a :: k). (CopyDiscard k, Ob a) => a ~> Unit
discard Strictified '[b] '[]
-> Strictified (c : cs) '[]
-> Strictified ('[b] ** (c : cs)) ('[] ** '[])
forall (x1 :: [k]) (x2 :: [k]) (y1 :: [k]) (y2 :: [k]).
Strictified x1 x2
-> Strictified y1 y2 -> Strictified (x1 ** y1) (x2 ** y2)
forall {j :: Kind} {k :: Kind} (p :: j +-> k) (x1 :: k) (x2 :: j)
       (y1 :: k) (y2 :: j).
MonoidalProfunctor p =>
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
** (c : cs) ~> Unit
Strictified (c : cs) '[]
forall (a :: [k]). Ob a => a ~> Unit
forall (k :: Kind) (a :: k). (CopyDiscard k, Ob a) => a ~> Unit
discard)

fst :: forall {k} (a :: k) b. (CopyDiscard k, Ob a, Ob b) => (a ** b) ~> a
fst :: forall {k :: Kind} (a :: k) (b :: k).
(CopyDiscard k, Ob a, Ob b) =>
(a ** b) ~> a
fst = (b ~> Unit) -> (a ** b) ~> a
forall {k :: Kind} (a :: k) (b :: k).
(Monoidal k, Ob a) =>
(b ~> Unit) -> (a ** b) ~> a
rightUnitorWith (forall (k :: Kind) (a :: k). (CopyDiscard k, Ob a) => a ~> Unit
discard @k @b)

snd :: forall {k} a (b :: k). (CopyDiscard k, Ob a, Ob b) => (a ** b) ~> b
snd :: forall {k :: Kind} (a :: k) (b :: k).
(CopyDiscard k, Ob a, Ob b) =>
(a ** b) ~> b
snd = (a ~> Unit) -> (a ** b) ~> b
forall {k :: Kind} (a :: k) (b :: k).
(Monoidal k, Ob a) =>
(b ~> Unit) -> (b ** a) ~> a
leftUnitorWith (forall (k :: Kind) (a :: k). (CopyDiscard k, Ob a) => a ~> Unit
discard @k @a)

(&&&) :: forall {k} (a :: k) x y. (CopyDiscard k) => a ~> x -> a ~> y -> a ~> x ** y
a ~> x
f &&& :: forall {k :: Kind} (a :: k) (x :: k) (y :: k).
CopyDiscard k =>
(a ~> x) -> (a ~> y) -> a ~> (x ** y)
&&& a ~> y
g = (a ~> x
f (a ~> x) -> (a ~> y) -> (a ** a) ~> (x ** y)
forall (x1 :: k) (x2 :: k) (y1 :: k) (y2 :: k).
(x1 ~> x2) -> (y1 ~> y2) -> (x1 ** y1) ~> (x2 ** y2)
forall {j :: Kind} {k :: Kind} (p :: j +-> k) (x1 :: k) (x2 :: j)
       (y1 :: k) (y2 :: j).
MonoidalProfunctor p =>
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
** a ~> y
g) ((a ** a) ~> (x ** y)) -> (a ~> (a ** a)) -> a ~> (x ** y)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k :: Kind} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. a ~> (a ** a)
forall (a :: k). Ob a => a ~> (a ** a)
forall (k :: Kind) (a :: k). (CopyDiscard k, Ob a) => a ~> (a ** a)
copy ((Ob a, Ob x) => a ~> (x ** y)) -> (a ~> x) -> a ~> (x ** y)
forall (a :: k) (b :: k) (r :: Kind).
((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j :: Kind} {k :: Kind} (p :: j +-> k) (a :: k) (b :: j)
       (r :: Kind).
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ a ~> x
f