module Proarrow.Monoid where import Data.Kind (Type, Constraint) import Prelude qualified as P import Proarrow.Core (CategoryOf(..), Promonad(..), arr) import Proarrow.Category.Monoidal (Monoidal(..)) import Proarrow.Object.BinaryProduct ((&&&), Cartesian) import Proarrow.Object.Terminal (terminate) type Monoid :: forall {k}. k -> Constraint class (Monoidal k, Ob m) => Monoid (m :: k) where mempty :: Unit ~> m mappend :: m ** m ~> m instance P.Monoid m => Monoid (m :: Type) where mempty :: Unit ~> m mempty () = m forall a. Monoid a => a P.mempty mappend :: (m ** m) ~> m mappend = (m -> m -> m) -> (m, m) -> m forall a b c. (a -> b -> c) -> (a, b) -> c P.uncurry m -> m -> m forall a. Semigroup a => a -> a -> a (P.<>) newtype GenElt x m = GenElt (x ~> m) instance (Monoid m, Cartesian k) => P.Semigroup (GenElt x (m :: k)) where GenElt x ~> m f <> :: GenElt x m -> GenElt x m -> GenElt x m <> GenElt x ~> m g = (x ~> m) -> GenElt x m forall {k} (x :: k) (m :: k). (x ~> m) -> GenElt x m GenElt ((m ** m) ~> m forall {k} (m :: k). Monoid m => (m ** m) ~> m mappend ((m ** m) ~> m) -> (x ~> (m ** m)) -> x ~> m forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k). Promonad p => p b c -> p a b -> p a c . (x ~> m f (x ~> m) -> (x ~> m) -> x ~> (m && m) forall (a :: k) (x :: k) (y :: k). (a ~> x) -> (a ~> y) -> a ~> (x && y) forall k (a :: k) (x :: k) (y :: k). HasBinaryProducts k => (a ~> x) -> (a ~> y) -> a ~> (x && y) &&& x ~> m g)) instance (Monoid m, Cartesian k, Ob x) => P.Monoid (GenElt x (m :: k)) where mempty :: GenElt x m mempty = (x ~> m) -> GenElt x m forall {k} (x :: k) (m :: k). (x ~> m) -> GenElt x m GenElt (Unit ~> m TerminalObject ~> m forall {k} (m :: k). Monoid m => Unit ~> m mempty (TerminalObject ~> m) -> (x ~> TerminalObject) -> x ~> m forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k). Promonad p => p b c -> p a b -> p a c . (x ~> TerminalObject) -> x ~> TerminalObject forall {k} (p :: PRO k k) (a :: k) (b :: k). Promonad p => (a ~> b) -> p a b arr x ~> TerminalObject forall {k} (a :: k). (HasTerminalObject k, Ob a) => a ~> TerminalObject terminate) class (Monoidal k, Ob c) => Comonoid (c :: k) where counit :: c ~> Unit comult :: c ~> c ** c