{-# 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 (..))
import Proarrow.Core (CategoryOf (..), OB)
import Proarrow.Monoid (Comonoid (..))
import Proarrow.Object.BinaryProduct (HasProducts, PROD (..))

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

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