diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,9 +1,18 @@ # Revision history for monoidal-functors -## 0.1.1 -- 2021-12-13 +## Upcoming +## 0.2.0.0 -- 2023-01-29 + +* Adds Tensored Type +* Rewrites haddocks +* Adds `Control.Category.Cartesian` module +* Adds a number of specialized combinators to `Data.Bifunctor.Monoidal.Specialized` + +## 0.1.1.0 -- 2021-12-13 + * Removes redundant `Iso` types. -* Some intitial attempts at documentation. +* Some initial attempts at documentation. ## 0.1.0.0 -- 2021-04-19 diff --git a/monoidal-functors.cabal b/monoidal-functors.cabal --- a/monoidal-functors.cabal +++ b/monoidal-functors.cabal @@ -1,7 +1,7 @@ cabal-version: 2.4 name: monoidal-functors category: Control, Categories -version: 0.1.1.0 +version: 0.2.0.0 license: MIT license-file: LICENSE author: Solomon Bothwell & Asad Saeeduddin @@ -11,26 +11,30 @@ homepage: http://github.com/solomon-b/monoidal-functors build-type: Simple extra-source-files: CHANGELOG.md -description: - A typeclass hierarchy for monoidal functors. - +description: A typeclass hierarchy for monoidal functors. source-repository head type: git location: https://github.com/solomon-b/monoidal-functors +-------------------------------------------------------------------------------- + library build-depends: - base >= 4.12 && < 5, - bifunctors >= 5.5.11 && < 5.6, - comonad >= 5.0.8 && < 5.1, - tagged >= 0.8.6 && < 0.9, - contravariant >= 1.5.5 && < 1.6, - profunctors >= 5.6.2 && < 5.7, - semigroupoids >= 5.3.6 && < 5.4, - these >= 1.1.1 && < 1.2, + base >= 4.12 && < 5, + bifunctors >= 5.5.11 && < 5.6, + comonad >= 5.0.8 && < 5.1, + distributive >= 0.6.2 && < 0.7, + tagged >= 0.8.6 && < 0.9, + contravariant >= 1.5.5 && < 1.6, + profunctors >= 5.6.2 && < 5.7, + semialign >= 1.2.0 && < 1.3, + semigroupoids >= 5.3.6 && < 5.4, + these >= 1.1.1 && < 1.2, exposed-modules: Control.Category.Tensor + Control.Category.Cartesian + Control.Category.Tensor.Expr Data.Bifunctor.BiInvariant Data.Bifunctor.Module Data.Bifunctor.Monoidal @@ -41,14 +45,17 @@ Data.Trifunctor.Module Data.Trifunctor.Monoidal - ghc-options: -Wall -Wno-trustworthy-safe -Wno-star-is-type - - if impl(ghc >= 9.0) - -- these flags may abort compilation with GHC-8.10 - -- https://gitlab.haskell.org/ghc/ghc/-/merge_requests/3295 - ghc-options: -Winferred-safe-imports -Wmissing-safe-haskell-mode + ghc-options: + -Wall + -Wcpp-undef + -Widentities + -Wincomplete-record-updates + -Wincomplete-uni-patterns + -Wpartial-fields + -Werror=missing-home-modules + -Wno-star-is-type - hs-source-dirs: src + hs-source-dirs: src default-language: Haskell2010 @@ -72,3 +79,4 @@ TypeApplications TypeOperators UndecidableInstances + diff --git a/src/Control/Category/Cartesian.hs b/src/Control/Category/Cartesian.hs new file mode 100644 --- /dev/null +++ b/src/Control/Category/Cartesian.hs @@ -0,0 +1,223 @@ +module Control.Category.Cartesian + ( -- * Semicartesian + Semicartesian (..), + (/\), + + -- * Semicocartesian + Semicocartesian (..), + (\/), + + -- * Cartesian + Cartesian (..), + + -- * Cocartesian + Cocartesian (..), + ) +where + +-------------------------------------------------------------------------------- + +import Control.Category (id, (>>>)) +import Control.Category.Tensor (Iso (..), Symmetric, Tensor (..), (#)) +import Data.Functor.Contravariant (Op (..)) +import Data.Void (Void, absurd) +import Prelude hiding (fst, id, snd) + +-------------------------------------------------------------------------------- + +-- | A 'Category' is 'Semicartesian' if it is equipped with a +-- 'Symmetric' bifunctor @t@ and each object comes equipped with a +-- +-- \(\Delta_x: x \to x \otimes x \), which we call 'split'. +-- +-- === Laws +-- +-- @ +-- 'Control.Category.Tensor.grmap' 'split' '.' 'split' ≡ 'bwd' 'Control.Category.Tensor.assoc' '.' 'Control.Category.Tensor.glmap' 'split' '.' 'split' +-- 'Control.Category.Tensor.glmap' 'split' '.' 'split' ≡ 'fwd' 'Control.Category.Tensor.assoc' '.' 'Control.Category.Tensor.grmap' 'split' '.' 'split' +-- @ +class Symmetric cat t => Semicartesian cat t where + -- | The of @a@ in @cat@. We can think of 'split' + -- as duplicating data. + -- + -- ==== __Examples__ + -- + -- >>> split @(->) @(,) True + -- (True,True) + split :: cat a (a `t` a) + + -- | Given morphisms @cat a x@ and @cat a y@, construct the + -- universal map @cat a (x \`t\` y)@. + -- + -- ==== __Examples__ + -- + -- >>> :t fork @(->) @(,) show not + -- fork @(->) @(,) show not :: Bool -> (String, Bool) + -- + -- >>> fork @(->) @(,) show not True + -- ("True",False) + fork :: cat a x -> cat a y -> cat a (x `t` y) + fork f g = split >>> f # g + + {-# MINIMAL split #-} + +-- | Infix version of 'fork'. +infixr 9 /\ + +(/\) :: Semicartesian cat t => cat a x -> cat a y -> cat a (x `t` y) +(/\) = fork + +instance Semicartesian (->) (,) where + split :: a -> (a, a) + split a = (a, a) + +instance Semicocartesian (->) t => Semicartesian Op t where + split :: Semicocartesian (->) t => Op a (t a a) + split = Op merge + +-------------------------------------------------------------------------------- + +-- | A 'Category' is 'Semicocartesian' if it is equipped with a +-- 'Symmetric' type operator @t@ and each object comes equipped with a +-- morphism \(\Delta^{-1}_x: x \otimes x \to x\), which we call 'merge'. +-- +-- === Laws +-- +-- @ +-- 'merge' '.' 'Control.Category.Tensor.grmap' 'merge' ≡ 'merge' . 'Control.Category.Tensor.glmap' 'merge' '.' 'fwd' 'Control.Category.Tensor.assoc' +-- 'merge' '.' 'Control.Category.Tensor.glmap' 'merge' ≡ 'merge' . 'Control.Category.Tensor.grmap' 'merge' '.' 'bwd' 'Control.Category.Tensor.assoc' +-- @ +class Symmetric cat t => Semicocartesian cat t where + -- | The of @a@ in @cat@. + -- + -- ==== __Examples__ + -- + -- >>> :t merge @(->) @(Either) (Left True) + -- merge @(->) @(Either) (Left True) :: Bool + -- + -- >>> merge @(->) @(Either) (Left True) + -- True + merge :: cat (a `t` a) a + + -- | Given morphisms @cat x a@ and @cat y a@, construct the + -- universal map @cat (x \`t\` y) a@. + -- + -- ==== __Examples__ + fuse :: cat x a -> cat y a -> cat (x `t` y) a + fuse f g = f # g >>> merge + + {-# MINIMAL merge #-} + +-- | Infix version of 'fuse'. +infixr 9 \/ + +(\/) :: Semicocartesian cat t => cat x a -> cat y a -> cat (x `t` y) a +(\/) = fuse + +instance Semicocartesian (->) Either where + merge :: Either a a -> a + merge = either id id + +instance Semicartesian (->) t => Semicocartesian Op t where + merge :: Semicartesian (->) t => Op (t a a) a + merge = Op split + +-------------------------------------------------------------------------------- + +-- | A 'Category' equipped with a 'Tensor' @t@ where the 'Tensor' unit @i@ is the +-- in @cat@ and thus every object @a@ is equipped with a morphism \(e_x: x \to I\), which we call 'kill'. +-- +-- === Laws +-- +-- @ +-- 'fwd' 'unitl' '.' 'Control.Category.Tensor.glmap' 'kill' '.' 'split' ≡ 'id' +-- 'fwd' 'unitr' '.' 'Control.Category.Tensor.grmap' 'kill' '.' 'split' ≡ 'id' +-- @ +class (Semicartesian cat t, Tensor cat t i) => Cartesian cat t i | i -> t, t -> i where + -- | A morphism from the @a@ to the terminal object @i@ in @cat. We + -- can think of 'kill' as deleting data where 'split' duplicates it. + -- + -- ==== __Examples__ + -- + -- >>> kill @(->) @(,) @() True + -- () + kill :: cat a i + + -- | The left projection for @t@. + -- + -- ==== __Examples__ + -- + -- >>> projl @(->) @(,) (True, "hello") + -- True + projl :: cat (x `t` y) x + projl = id # kill >>> fwd unitr + + -- | The right projection for @t@. + -- + -- ==== __Examples__ + -- + -- >>> projr @(->) @(,) (True, "hello") + -- "hello" + projr :: cat (x `t` y) y + projr = kill # id >>> fwd unitl + + -- | Given the universal map @cat a (x `t` y)@, construct morphisms @cat a x@ and @cat a y@. + -- + -- ==== __Examples__ + unfork :: cat a (x `t` y) -> (cat a x, cat a y) + unfork h = (h >>> projl, h >>> projr) + + {-# MINIMAL kill #-} + +instance Cartesian (->) (,) () where + kill :: a -> () + kill = const () + +instance Cocartesian (->) t i => Cartesian Op t i where + kill :: Cocartesian (->) t i => Op a i + kill = Op spawn + +-------------------------------------------------------------------------------- + +-- | A 'Category' equipped with a 'Tensor' @t@ where the 'Tensor' unit @i@ is the +-- in @cat@ and thus every object @a@ is equipped with a morphism \(e^{-1}_x: I \to x\), which we call 'spawn'. +-- +-- === Laws +-- +-- @ +-- 'merge' '.' 'Control.Category.Tensor.glmap' 'spawn' '.' 'bwd' 'unitl' ≡ 'id' +-- 'merge' '.' 'Control.Category.Tensor.grmap' 'spawn' '.' 'bwd' 'unitr' ≡ 'id' +-- @ +class (Semicocartesian cat t, Tensor cat t i) => Cocartesian cat t i | i -> t, t -> i where + -- | A morphism from the initial object @i@ in @cat@ to @a@. + -- + -- ==== __Examples__ + spawn :: cat i a + + -- | The left inclusion for @t@. + -- + -- ==== __Examples__ + incll :: cat x (x `t` y) + incll = bwd unitr >>> id # spawn + + -- | The right inclusion for @t@. + -- + -- ==== __Examples__ + inclr :: cat y (x `t` y) + inclr = bwd unitl >>> spawn # id + + -- | Given the universal map @cat (x `t` y) a@, construct morphisms @cat x a@ and @cat y a@. + -- + -- ==== __Examples__ + unfuse :: cat (x `t` y) a -> (cat x a, cat y a) + unfuse h = (incll >>> h, inclr >>> h) + + {-# MINIMAL spawn #-} + +instance Cartesian (->) t i => Cocartesian Op t i where + spawn :: Cartesian (->) t i => Op i a + spawn = Op kill + +instance Cocartesian (->) Either Void where + spawn :: Void -> a + spawn = absurd diff --git a/src/Control/Category/Tensor.hs b/src/Control/Category/Tensor.hs --- a/src/Control/Category/Tensor.hs +++ b/src/Control/Category/Tensor.hs @@ -1,220 +1,346 @@ {-# LANGUAGE MonoLocalBinds #-} -module Control.Category.Tensor where +module Control.Category.Tensor + ( -- * Iso + Iso (..), -import Prelude hiding (id) -import Control.Applicative -import Control.Category (Category, id) -import Data.Biapplicative -import Data.Functor.Contravariant -import Data.Profunctor -import Data.These -import Data.Void + -- * GBifunctor + GBifunctor (..), + (#), + grmap, + glmap, + -- * Associative + Associative (..), -{- + -- * Tensor + Tensor (..), -| Tensor | Unit | -+--------|------+ -| Either | Void | -| (,) | () | -| These | Void | + -- * Symmetric + Symmetric (..), + ) +where -tensor = monoidal structure = - category - + bifunctor on that category `t` - + unit object in that category `i` - + isomorphisms in that category `t i a <-> a`, `t a i <-> a`, `t a (t b c) <-> t (t a b) c` - + some equalities +-------------------------------------------------------------------------------- -monoidal functor = a functor that goes between the underlying -categories of two different monoidal structure, and has a pair of -operations `t2 (f a) (f b) -> f (t1 a b)` and `i2 -> f i1` +import Control.Applicative (Applicative (..)) +import Control.Category (Category (..)) +import Data.Biapplicative (Biapplicative (..), Bifunctor (..)) +import Data.Functor.Contravariant (Op (..)) +import Data.Profunctor (Profunctor (..), Star (..)) +import Data.These (These (..), these) +import Data.Void (Void, absurd) +import Prelude hiding (id, (.)) --} +-------------------------------------------------------------------------------- -class (Category cat1, Category cat2) => GBifunctor cat1 cat2 r t | t r -> cat1 cat2 where - gbimap :: a `cat1` b -> c `cat2` d -> t a c `r` t b d +-- | An invertible mapping between 'a' and 'b' in category 'cat'. +-- +-- === Laws +-- +-- @ +-- 'fwd' '.' 'bwd' ≡ 'id' +-- 'bwd' '.' 'fwd' ≡ 'id' +-- @ +data Iso cat a b = Iso { fwd :: cat a b, bwd :: cat b a } +instance Category cat => Category (Iso cat) where + id :: Iso cat a a + id = Iso id id + + (.) :: Iso cat b c -> Iso cat a b -> Iso cat a c + bc . ab = Iso (fwd bc . fwd ab) (bwd ab . bwd bc) + +-------------------------------------------------------------------------------- + +-- | A Bifunctor @t@ is a 'Functor' whose domain is the product of two +-- categories. 'GBifunctor' is equivalent to the ordinary +-- 'Data.Bifunctor.Bifunctor' class but we replace the implicit '(->)' 'Category' with +-- three distinct higher kinded variables @cat1@, @cat2@, and @cat3@ allowing the user +-- to pickout a functor from \(cat_1 \times cat_2\) to \(cat_3\). +-- +-- === Laws +-- +-- @ +-- 'gbimap' 'id' 'id' ≡ 'id' +-- 'grmap' 'id' ≡ 'id' +-- 'glmap' 'id' ≡ 'id' +-- +-- 'gbimap' (f '.' g) (h '.' i) ≡ 'gbimap' f h '.' 'gbimap' g i +-- 'grmap' (f '.' g) ≡ 'grmap' f '.' 'grmap' g +-- 'glmap' (f '.' g) ≡ 'glmap' f '.' 'glmap' g +-- @ +class (Category cat1, Category cat2, Category cat3) => GBifunctor cat1 cat2 cat3 t | t cat3 -> cat1 cat2 where + -- | Covariantly map over both variables. + -- + -- @'gbimap' f g ≡ 'glmap' f '.' 'grmap' g@ + -- + -- ==== __Examples__ + -- >>> gbimap @(->) @(->) @(->) @(,) show not (123, False) + -- ("123",True) + -- + -- >>> gbimap @(->) @(->) @(->) @Either show not (Right False) + -- Right True + -- + -- >>> getOp (gbimap @Op @Op @Op @Either (Op (+ 1)) (Op show)) (Right True) + -- Right "True" + gbimap :: cat1 a b -> cat2 c d -> cat3 (a `t` c) (b `t` d) + +-- | Infix operator for 'gbimap'. +infixr 9 # +(#) :: GBifunctor cat1 cat2 cat3 t => cat1 a b -> cat2 c d -> cat3 (a `t` c) (b `t` d) +(#) = gbimap + +-- | Covariantally map over the right variable. +grmap :: GBifunctor cat1 cat2 cat3 t => cat2 c d -> cat3 (a `t` c) (a `t` d) +grmap = (#) id + +-- | Covariantally map over the left variable. +glmap :: GBifunctor cat1 cat2 cat3 t => cat1 a b -> cat3 (a `t` c) (b `t` c) +glmap = flip (#) id + instance GBifunctor (->) (->) (->) t => GBifunctor Op Op Op t where gbimap :: Op a b -> Op c d -> Op (t a c) (t b d) gbimap (Op f) (Op g) = Op $ gbimap f g -instance GBifunctor (->) (->) (->) (,) where - gbimap :: (a -> b) -> (c -> d) -> (a, c) -> (b, d) - gbimap f g = bimap f g - -instance GBifunctor (->) (->) (->) Either where - gbimap :: (a -> b) -> (c -> d) -> Either a c -> Either b d - gbimap f g = bimap f g - -instance GBifunctor (->) (->) (->) These where - gbimap :: (a -> b) -> (c -> d) -> These a c -> These b d - gbimap f g = bimap f g +instance Bifunctor t => GBifunctor (->) (->) (->) t where + gbimap = bimap instance GBifunctor (Star Maybe) (Star Maybe) (Star Maybe) These where gbimap :: Star Maybe a b -> Star Maybe c d -> Star Maybe (These a c) (These b d) gbimap (Star f) (Star g) = Star $ \case - This a -> This <$> f a - That c -> That <$> g c + This a -> This <$> f a + That c -> That <$> g c These a c -> liftA2 These (f a) (g c) -grmap :: GBifunctor cat1 cat2 r t => c `cat2` d -> t a c `r` t a d -grmap = gbimap id - -glmap :: GBifunctor cat1 cat2 r t => a `cat1` b -> t a c `r` t b c -glmap = flip gbimap id +instance GBifunctor cat cat cat t => GBifunctor (Iso cat) (Iso cat) (Iso cat) t where + gbimap :: Iso cat a b -> Iso cat c d -> Iso cat (t a c) (t b d) + gbimap iso1 iso2 = Iso (gbimap (fwd iso1) (fwd iso2)) (gbimap (bwd iso1) (bwd iso2)) -data Iso cat a b = Iso { fwd :: a `cat` b, bwd :: b `cat` a } +-------------------------------------------------------------------------------- -class (Category cat, GBifunctor cat cat cat t) => Associative t cat where +-- | A bifunctor \(\_\otimes\_: \mathcal{C} \times \mathcal{C} \to \mathcal{C}\) is +-- 'Associative' if it is equipped with a +-- of the form +-- \(\alpha_{x,y,z} : (x \otimes (y \otimes z)) \to ((x \otimes y) \otimes z)\), which +-- we call 'assoc'. +-- +-- === Laws +-- +-- @ +-- 'fwd' 'assoc' '.' 'bwd' 'assoc' ≡ 'id' +-- 'bwd' 'assoc' '.' 'fwd' 'assoc' ≡ 'id' +-- @ +class (Category cat, GBifunctor cat cat cat t) => Associative cat t where + -- | The between left and + -- right associated nestings of @t@. + -- + -- ==== __Examples__ + -- + -- >>> :t assoc @(->) @(,) + -- assoc @(->) @(,) :: Iso (->) (a, (b, c)) ((a, b), c) + -- + -- >>> fwd (assoc @(->) @(,)) (1, ("hello", True)) + -- ((1,"hello"),True) assoc :: Iso cat (a `t` (b `t` c)) ((a `t` b) `t` c) -instance Associative t (->) => Associative t Op where - assoc :: Iso Op (t a (t b c)) (t (t a b) c) +instance Associative (->) t => Associative Op t where + assoc :: Iso Op (a `t` (b `t` c)) ((a `t` b) `t` c) assoc = Iso { fwd = Op $ bwd assoc , bwd = Op $ fwd assoc } -instance (Monad m, Associative t (->), GBifunctor (Star m) (Star m) (Star m) t) => Associative t (Star m) where - assoc :: Iso (Star m) (t a (t b c)) (t (t a b) c) - assoc = Iso - { fwd = (`rmap` id) (fwd assoc) - , bwd = (`rmap` id) (bwd assoc) - } - -instance Associative (,) (->) where +instance Associative (->) (,) where assoc :: Iso (->) (a, (b, c)) ((a, b), c) assoc = Iso { fwd = \(a, (b, c)) -> ((a, b), c) , bwd = \((a, b), c) -> (a, (b, c)) } -instance Associative Either (->) where +instance Associative (->) Either where assoc :: Iso (->) (Either a (Either b c)) (Either (Either a b) c) assoc = Iso { fwd = either (Left . Left) (either (Left . Right) Right) , bwd = either (fmap Left) (Right . Right) } -instance Associative These (->) where +instance Associative (->) These where assoc :: Iso (->) (These a (These b c)) (These (These a b) c) assoc = Iso { fwd = these (This . This) (glmap That) (glmap . These) , bwd = these (grmap This) (That . That) (flip $ grmap . flip These) } -class Associative t cat => Tensor t i cat | t -> i where - lunit :: Iso cat (t i a) a - runit :: Iso cat (t a i) a - -instance (Tensor t i (->)) => Tensor t i Op where - lunit :: Iso Op (t i a) a - lunit = Iso - { fwd = Op $ bwd lunit - , bwd = Op $ fwd lunit +instance (Monad m, Associative (->) t, GBifunctor (Star m) (Star m) (Star m) t) => Associative (Star m) t where + assoc :: Iso (Star m) (a `t` (b `t` c)) ((a `t` b) `t` c) + assoc = Iso + { fwd = (`rmap` id) (fwd assoc) + , bwd = (`rmap` id) (bwd assoc) } - runit :: Iso Op (t a i) a - runit = Iso - { fwd = Op $ bwd runit - , bwd = Op $ fwd runit - } +-------------------------------------------------------------------------------- -instance (Monad m, Tensor t i (->), Associative t (Star m)) => Tensor t i (Star m) where - lunit :: Iso (Star m) (t i a) a - lunit = Iso - { fwd = (`rmap` id) (fwd lunit) - , bwd = (`rmap` id) (bwd lunit) +-- | A bifunctor \(\_ \otimes\_ \ : \mathcal{C} \times \mathcal{C} \to \mathcal{C}\) +-- that maps out of the \(\mathcal{C} \times \mathcal{C}\) +-- is a 'Tensor' if it has: +-- +-- 1. a corresponding identity type \(I\) +-- 2. Left and right +-- operations \(\lambda_{x} : 1 \otimes x \to x\) and \(\rho_{x} : x \otimes 1 \to x\), which we call 'unitr' and 'unitl'. +-- +-- === Laws +-- +-- @ +-- 'fwd' 'unitr' (a ⊗ i) ≡ a +-- 'bwd' 'unitr' a ≡ (a ⊗ i) +-- +-- 'fwd' 'unitl' (i ⊗ a) ≡ a +-- 'bwd' 'unitl' a ≡ (i ⊗ a) +-- @ +class Associative cat t => Tensor cat t i | t -> i where + -- | The between @(i \`t\` a)@ and @a@. + -- + -- ==== __Examples__ + -- + -- >>> fwd (unitl @_ @(,)) ((), True) + -- True + -- + -- >>> bwd (unitl @_ @(,)) True + -- ((),True) + -- + -- >>> bwd (unitl @_ @Either) True + -- Right True + -- + -- >>> :t bwd (unitl @_ @Either) True + -- bwd (unitl @_ @Either) True :: Either Void Bool + unitl :: Iso cat (i `t` a) a + -- | The between @(a \`t\` i)@ and @a@. + -- + -- ==== __Examples__ + -- + -- >>> fwd (unitr @_ @(,)) (True, ()) + -- True + -- + -- >>> bwd (unitr @_ @(,)) True + -- (True,()) + -- + -- >>> bwd (unitr @_ @Either) True + -- Left True + -- + -- >>> :t bwd (unitr @_ @Either) True + -- bwd (unitr @_ @Either) True :: Either Bool Void + unitr :: Iso cat (a `t` i) a + +instance (Tensor (->) t i) => Tensor Op t i where + unitl :: Iso Op (i `t` a) a + unitl = Iso + { fwd = Op $ bwd unitl + , bwd = Op $ fwd unitl } - runit = Iso - { fwd = (`rmap` id) (fwd runit) - , bwd = (`rmap` id) (bwd runit) + unitr :: Iso Op (a `t` i) a + unitr = Iso + { fwd = Op $ bwd unitr + , bwd = Op $ fwd unitr } -instance Tensor (,) () (->) where - lunit :: Iso (->) ((), a) a - lunit = Iso +instance Tensor (->) (,) () where + unitl :: Iso (->) ((), a) a + unitl = Iso { fwd = snd , bwd = bipure () } - runit :: Iso (->) (a, ()) a - runit = Iso + unitr :: Iso (->) (a, ()) a + unitr = Iso { fwd = fst , bwd = (`bipure` ()) } -instance Tensor Either Void (->) where - lunit :: Iso (->) (Either Void a) a - lunit = Iso +instance Tensor (->) Either Void where + unitl :: Iso (->) (Either Void a) a + unitl = Iso { fwd = either absurd id , bwd = pure } - runit :: Iso (->) (Either a Void) a - runit = Iso + unitr :: Iso (->) (Either a Void) a + unitr = Iso { fwd = either id absurd , bwd = Left } -instance Tensor These Void (->) where - lunit :: Iso (->) (These Void a) a - lunit = Iso +instance Tensor (->) These Void where + unitl :: Iso (->) (These Void a) a + unitl = Iso { fwd = these absurd id (\ _ x -> x) , bwd = That } - runit :: Iso (->) (These a Void) a - runit = Iso + unitr :: Iso (->) (These a Void) a + unitr = Iso { fwd = these id absurd const , bwd = This } -class Associative t cat => Symmetric t cat where - swap :: t a b `cat` t b a +instance (Monad m, Tensor (->) t i, Associative (Star m) t) => Tensor (Star m) t i where + unitl :: Iso (Star m) (i `t` a) a + unitl = Iso + { fwd = (`rmap` id) (fwd unitl) + , bwd = (`rmap` id) (bwd unitl) + } -instance (Symmetric t (->)) => Symmetric t Op where - swap :: Op (t a b) (t b a) - swap = Op swap + unitr :: Iso (Star m) (a `t` i) a + unitr = Iso + { fwd = (`rmap` id) (fwd unitr) + , bwd = (`rmap` id) (bwd unitr) + } -instance (Monad m, Symmetric t (->), Associative t (Star m)) => Symmetric t (Star m) where - swap :: Star m (t a b) (t b a) - swap = Star $ pure . swap +-------------------------------------------------------------------------------- -instance Symmetric (,) (->) where +-- | A bifunctor \(\_ \otimes\_ \ : \mathcal{C} \times \mathcal{C} \to \mathcal{C}\) +-- is 'Symmetric' if it has a product operation \(B_{x,y} : x \otimes y \to y \otimes x\) +-- such that \(B_{x,y} \circ B_{x,y} \equiv 1_{x \otimes y}\), which we call 'swap'. +-- +-- === Laws +-- +-- @ +-- 'swap' '.' 'swap' ≡ 'id' +-- @ +class Associative cat t => Symmetric cat t where + -- | @swap@ is a symmetry isomorphism for @t@ + -- + -- ==== __Examples__ + -- + -- >>> :t swap @(->) @(,) + -- swap @(->) @(,) :: (a, b) -> (b, a) + -- + -- >>> swap @(->) @(,) (True, "hello") + -- ("hello",True) + -- + -- >>> :t swap @(->) @Either (Left True) + -- swap @(->) @Either (Left True) :: Either b Bool + -- + -- >>> swap @(->) @Either (Left True) + -- Right True + swap :: cat (a `t` b) (b `t` a) + +instance Symmetric (->) t => Symmetric Op t where + swap :: Op (a `t` b) (b `t` a) + swap = Op swap + +instance Symmetric (->) (,) where swap :: (a, b) -> (b, a) swap (a, b) = (b, a) -instance Symmetric Either (->) where +instance Symmetric (->) Either where swap :: Either a b -> Either b a swap = either Right Left -instance Symmetric These (->) where +instance Symmetric (->) These where swap :: These a b -> These b a swap = these That This (flip These) -class (Symmetric t cat, Tensor t i cat) => Cartesian t i cat | i -> t, t -> i where - diagonal :: a `cat` t a a - terminal :: a `cat` i - -instance Cartesian (,) () (->) where - diagonal :: a -> (a , a) - diagonal = dup - - terminal :: a -> () - terminal = const () - -instance Cartesian Either Void Op where - diagonal :: Op a (Either a a) - diagonal = Op merge - - terminal :: Op a Void - terminal = Op absurd - -dup :: a -> (a, a) -dup a = (a, a) - -merge :: Either a a -> a -merge = either id id +instance (Monad m, Symmetric (->) t, Associative (Star m) t) => Symmetric (Star m) t where + swap :: Star m (a `t` b) (b `t` a) + swap = Star $ pure . swap diff --git a/src/Control/Category/Tensor/Expr.hs b/src/Control/Category/Tensor/Expr.hs new file mode 100644 --- /dev/null +++ b/src/Control/Category/Tensor/Expr.hs @@ -0,0 +1,74 @@ +{-# LANGUAGE AllowAmbiguousTypes #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE StandaloneKindSignatures #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeFamilies #-} +module Control.Category.Tensor.Expr + ( -- * Type Families + MConcat, + Tensored (..), + type (++), + + -- * AppendTensored + AppendTensored (..), + ) +where + +import Control.Category.Tensor +import Data.Function +import Data.Kind +import Prelude (Eq, Ord, Show) + +-------------------------------------------------------------------------------- + +-- | +-- +-- __Examples:__ +-- +-- >>> :{ +-- let foo :: Tensored (,) () '[Bool, Int] +-- foo = Tensored (True, (8, ())) +-- :} +-- +-- >>> :{ +-- let bar :: Tensored Either Void '[Bool, Int] +-- bar = Tensored $ Right $ Left 8 +-- :} +-- +-- >>> :{ +-- let baz :: Tensored These Void '[Bool, Int] +-- baz = Tensored $ These True $ This 8 +-- :} +type MConcat :: (Type -> Type -> Type) -> Type -> [Type] -> Type +type family MConcat mappend mempty xs where + MConcat mappend mempty '[] = mempty + MConcat mappend mempty (x ': xs) = mappend x (MConcat mappend mempty xs) + +newtype Tensored t i xs = Tensored { getTensored :: MConcat t i xs } + +deriving newtype instance Show (MConcat t i xs) => Show (Tensored t i xs) +deriving newtype instance Eq (MConcat t i xs) => Eq (Tensored t i xs) +deriving newtype instance Ord (MConcat t i xs) => Ord (Tensored t i xs) + +-------------------------------------------------------------------------------- + +type (++) :: [k] -> [k] -> [k] +type family xs ++ ys + where + '[] ++ xs = xs + (x ': xs) ++ ys = x ': (xs ++ ys) + +class AppendTensored xs where + appendTensored :: Tensor (->) t i => Tensored t i xs `t` Tensored t i ys -> Tensored t i (xs ++ ys) + +instance AppendTensored '[] + where + appendTensored = fwd unitl . glmap getTensored + +instance AppendTensored xs => AppendTensored (x ': xs) + where + appendTensored = Tensored . grmap (getTensored . appendTensored @xs . glmap Tensored) . bwd assoc . glmap getTensored + diff --git a/src/Data/Bifunctor/BiInvariant.hs b/src/Data/Bifunctor/BiInvariant.hs --- a/src/Data/Bifunctor/BiInvariant.hs +++ b/src/Data/Bifunctor/BiInvariant.hs @@ -1,74 +1,114 @@ -module Data.Bifunctor.BiInvariant where +module Data.Bifunctor.BiInvariant + ( -- * BiInvariant + BiInvariant (..), + biinvIso, + type Coercible1, + type Coercible2, + ) +where -import Prelude -import Control.Arrow -import Control.Category.Tensor -import Control.Comonad -import Data.Bifunctor -import Data.Bifunctor.Biap -import Data.Bifunctor.Biff -import Data.Bifunctor.Clown -import Data.Bifunctor.Flip -import Data.Bifunctor.Tannen -import Data.Bifunctor.Joker -import Data.Bifunctor.Sum -import Data.Bifunctor.Product -import Data.Bifunctor.Wrapped -import Data.Coerce -import Data.Functor.Const -import Data.Functor.Contravariant -import Data.Kind -import Data.Profunctor -import Data.Profunctor.Cayley -import Data.Profunctor.Composition -import Data.Profunctor.Choice -import Data.Profunctor.Closed -import Data.Profunctor.Mapping -import Data.Profunctor.Ran -import Data.Profunctor.Strong -import Data.Profunctor.Traversing -import Data.Profunctor.Yoneda +-------------------------------------------------------------------------------- + +import Control.Arrow (Arrow, Kleisli (Kleisli)) +import Control.Category.Tensor (Iso (Iso)) +import Control.Comonad (Cokleisli (Cokleisli)) +import Data.Bifunctor (Bifunctor (bimap)) +import Data.Bifunctor.Biap (Biap (Biap)) +import Data.Bifunctor.Biff (Biff (Biff)) +import Data.Bifunctor.Clown (Clown (Clown)) +import Data.Bifunctor.Flip (Flip (Flip)) +import Data.Bifunctor.Joker (Joker (Joker)) +import Data.Bifunctor.Product (Product) +import Data.Bifunctor.Sum (Sum) +import Data.Bifunctor.Tannen (Tannen (Tannen)) +import Data.Bifunctor.Wrapped (WrappedBifunctor (WrapBifunctor)) +import Data.Coerce (Coercible) +import Data.Functor.Const (Const (Const)) +import Data.Functor.Contravariant (Contravariant (contramap)) +import Data.Kind (Constraint) +import Data.Profunctor (Costar (Costar), Forget (Forget), Profunctor (dimap), Star (Star), WrappedArrow (WrapArrow)) +import Data.Profunctor.Cayley (Cayley (Cayley)) +import Data.Profunctor.Choice (CopastroSum (CopastroSum), CotambaraSum, PastroSum, TambaraSum (TambaraSum)) +import Data.Profunctor.Closed (Closure (Closure), Environment) +import Data.Profunctor.Composition (Procompose, Rift (Rift)) +import Data.Profunctor.Mapping (CofreeMapping (CofreeMapping), FreeMapping) +import Data.Profunctor.Ran (Codensity (Codensity), Ran (Ran)) +import Data.Profunctor.Strong (Copastro (Copastro), Cotambara, Pastro, Tambara (Tambara)) +import Data.Profunctor.Traversing (CofreeTraversing (CofreeTraversing), FreeTraversing) +import Data.Profunctor.Yoneda (Coyoneda, Yoneda (Yoneda)) import Data.Semigroup (Arg) -import Data.Tagged -import Data.These +import Data.Tagged (Tagged (Tagged)) +import Data.These (These) import GHC.Generics (K1) +import Prelude +-------------------------------------------------------------------------------- +-- | A bifunctor is 'BiInvariant' if it is parametric in both its type +-- parameters. +-- +-- === Laws +-- +-- @ +-- 'biinvmap' 'id' 'id' 'id' 'id' ≡ 'id' +-- 'biinvmap' @g2@ @g2'@ @f2@ @f2'@ 'Control.Category..' 'Data.Functor.Invariant.invmap' @g1@ @g1'@ @f1@ @f1'@ ≡ 'Data.Functor.Invariant.invmap' (@g2@ 'Control.Category..' @g1@) (@g1'@ 'Control.Category..' @g2'@) (@f2@ 'Control.Category..' @f1@) (@f1'@ 'Control.Category..' @f2'@) +-- @ class BiInvariant p where + -- | Used to apply a pair of isomorphic functions to @p a b@. + -- 'Biinvmap' picks out the appropriate half of the iso depending if + -- @p@ is covariant or contravariant on each parameter. + -- + -- ==== __Examples__ + -- + -- >>> :t biinvmap @(,) (read @Int) show (read @Bool) show + -- biinvmap @(,) (read @Int) show (read @Bool) show :: (Int, Bool) -> (String, String) + -- + -- >>> biinvmap @(,) (read @Int) show (read @Bool) show (10, True) + -- ("10","True") + -- + -- >>> :t biinvmap @(->) (read @Int) show (read @Bool) show + -- biinvmap @(->) (read @Int) show (read @Bool) show :: (Int -> Bool) -> String -> String + -- + -- >>> biinvmap @(->) (read @Int) show (read @Bool) show (\i -> i > 10) "12" + -- "True" biinvmap :: (a' -> a) -> (a -> a') -> (b' -> b) -> (b -> b') -> p a b -> p a' b' --- BiInvariant witnesses an Isomorphism +-- | BiInvariant witnesses an Isomorphism biinvIso :: BiInvariant p => Iso (->) a a' -> Iso (->) b b' -> Iso (->) (p a b) (p a' b') biinvIso (Iso f f') (Iso g g') = Iso (biinvmap f' f g' g) (biinvmap f f' g g') +-- | Boilerplate newtype to derive 'BiInvariant' for any 'Profunctor'. newtype FromProfunctor p a b = FromProfunctor { runPro :: p a b} instance Profunctor p => BiInvariant (FromProfunctor p) where biinvmap :: (a' -> a) -> (a -> a') -> (b' -> b) -> (b -> b') -> FromProfunctor p a b -> FromProfunctor p a' b' biinvmap f _ _ g = FromProfunctor . dimap f g . runPro +-- | Boilerplate newtype to derive 'BiInvariant' for any 'Bifunctor'. newtype FromBifunctor p a b = FromBifunctor { runBi :: p a b } instance Bifunctor p => BiInvariant (FromBifunctor p) where biinvmap :: (a' -> a) -> (a -> a') -> (b' -> b) -> (b -> b') -> FromBifunctor p a b -> FromBifunctor p a' b' biinvmap _ f _ g = FromBifunctor . bimap f g . runBi +-- | Boilerplate newtype to derive 'BiInvariant' for any 'Contravariant'. newtype FromContra f a = FromContra { runContra :: f a } instance Contravariant f => Contravariant (FromContra f) where + contramap :: Contravariant f => (a' -> a) -> FromContra f a -> FromContra f a' contramap f = FromContra . contramap f . runContra -newtype FromFunctor f a = FromFunctor { runFunctor :: f a } +newtype FromFunctor f a = FromFunctor (f a) deriving Functor type Coercible1 f = ((forall a b. Coercible a b => Coercible (f a) (f b)) :: Constraint) type Coercible2 f = (forall a b c d. (Coercible a b, Coercible c d) => Coercible (f a c) (f b d) :: Constraint) -deriving via (FromProfunctor (->)) instance BiInvariant (->) +deriving via (FromProfunctor (->)) instance BiInvariant (->) deriving via (FromProfunctor (Biff p f g)) instance (Profunctor p, Functor f, Functor g) => BiInvariant (Biff (FromProfunctor p) f g) deriving via (FromProfunctor (Cayley f q)) instance (Functor f, Profunctor q) => BiInvariant (Cayley f q) deriving via (FromProfunctor (Closure p)) instance Profunctor p => BiInvariant (Closure p) -deriving via (FromProfunctor (Clown f :: * -> * -> *)) instance Contravariant f => BiInvariant (Clown (FromContra f) :: * -> * -> *) +deriving via (FromProfunctor (Clown f :: * -> * -> *)) instance Contravariant f => BiInvariant (Clown (FromContra f) :: * -> * -> *) deriving via (FromProfunctor (Codensity p)) instance Profunctor p => BiInvariant (Codensity p) deriving via (FromProfunctor (CofreeMapping p)) instance Profunctor p => BiInvariant (CofreeMapping p) deriving via (FromProfunctor (CofreeTraversing p)) instance Profunctor p => BiInvariant (CofreeTraversing p) @@ -93,7 +133,7 @@ deriving via (FromProfunctor (Rift p q)) instance (Profunctor p, Profunctor q) => BiInvariant (Rift p q) deriving via (FromProfunctor (Star f)) instance Functor f => BiInvariant (Star (FromFunctor f)) deriving via (FromProfunctor (Sum p q)) instance (Profunctor p, Profunctor q) => BiInvariant (Sum (FromProfunctor p) (FromProfunctor q)) -deriving via (FromProfunctor (Tagged :: * -> * -> *)) instance BiInvariant (Tagged :: * -> * -> *) +deriving via (FromProfunctor (Tagged :: * -> * -> *)) instance BiInvariant (Tagged :: * -> * -> *) deriving via (FromProfunctor (Tambara p)) instance Profunctor p => BiInvariant (Tambara p) deriving via (FromProfunctor (TambaraSum p)) instance Profunctor p => BiInvariant (TambaraSum p) deriving via (FromProfunctor (Tannen f q)) instance (Functor f, Profunctor q) => BiInvariant (Tannen f q) @@ -106,17 +146,17 @@ deriving via (FromBifunctor ((,,,,,) x1 x2 x3 x4)) instance BiInvariant ((,,,,,) x1 x2 x3 x4) deriving via (FromBifunctor ((,,,,,,) x1 x2 x3 x4 x5)) instance BiInvariant ((,,,,,,) x1 x2 x3 x4 x5) deriving via (FromBifunctor (,)) instance BiInvariant (,) -deriving via (FromBifunctor (Arg)) instance BiInvariant (Arg) +deriving via (FromBifunctor Arg) instance BiInvariant Arg deriving via (FromBifunctor (Biap bi)) instance Bifunctor bi => BiInvariant (Biap bi) deriving via (FromBifunctor (Biff p f g)) instance (Bifunctor p, Functor f, Functor g) => BiInvariant (Biff (FromBifunctor p) f g) -deriving via (FromBifunctor (Clown f :: * -> * -> *)) instance Functor f => BiInvariant (Clown (FromFunctor f) :: * -> * -> *) -deriving via (FromBifunctor (Const :: * -> * -> *)) instance BiInvariant (Const :: * -> * -> *) -deriving via (FromBifunctor (Either)) instance BiInvariant (Either) +deriving via (FromBifunctor (Clown f :: * -> * -> *)) instance Functor f => BiInvariant (Clown (FromFunctor f) :: * -> * -> *) +deriving via (FromBifunctor (Const :: * -> * -> *)) instance BiInvariant (Const :: * -> * -> *) +deriving via (FromBifunctor Either) instance BiInvariant Either deriving via (FromBifunctor (Flip p)) instance Bifunctor p => BiInvariant (Flip p) -deriving via (FromBifunctor (Joker f :: * -> * -> *)) instance Functor f => BiInvariant (Joker (FromFunctor f) :: * -> * -> *) -deriving via (FromBifunctor (K1 i :: * -> * -> *)) instance BiInvariant (K1 i :: * -> * -> *) +deriving via (FromBifunctor (Joker f :: * -> * -> *)) instance Functor f => BiInvariant (Joker (FromFunctor f) :: * -> * -> *) +deriving via (FromBifunctor (K1 i :: * -> * -> *)) instance BiInvariant (K1 i :: * -> * -> *) deriving via (FromBifunctor (Product p q)) instance (Bifunctor p, Bifunctor q) => BiInvariant (Product (FromBifunctor p) (FromBifunctor q)) deriving via (FromBifunctor (Sum p q)) instance (Bifunctor p, Bifunctor q) => BiInvariant (Sum (FromBifunctor p) (FromBifunctor q)) deriving via (FromBifunctor (Tannen f q)) instance (Functor f, Coercible1 f, Bifunctor q) => BiInvariant (Tannen (FromFunctor f) (FromBifunctor q)) -deriving via (FromBifunctor (These)) instance BiInvariant (These) +deriving via (FromBifunctor These) instance BiInvariant These deriving via (FromBifunctor (WrappedBifunctor p)) instance Bifunctor p => BiInvariant (WrappedBifunctor p) diff --git a/src/Data/Bifunctor/Module.hs b/src/Data/Bifunctor/Module.hs --- a/src/Data/Bifunctor/Module.hs +++ b/src/Data/Bifunctor/Module.hs @@ -1,11 +1,724 @@ -module Data.Bifunctor.Module where +module Data.Bifunctor.Module + ( -- * LeftModule + LeftModule (..), -class LeftModule cat t1 t2 f where - lstrength :: cat (f a b) (f (t1 a x) (t2 b x)) + -- * RightModule + RightModule (..), --- Strong is LeftModule (->) (,) (,) + -- * Bimodule + Bimodule, + -- * LeftCoModule + LeftCoModule (..), + + -- * RightCoModule + RightCoModule (..), + + -- * CoBimodule + CoBimodule, + ) +where + +-------------------------------------------------------------------------------- + +import Control.Applicative (Applicative) +import Control.Arrow (Arrow, ArrowChoice, ArrowLoop, Kleisli (..)) +import Control.Category.Tensor (GBifunctor (..)) +import Control.Comonad (Cokleisli, Comonad) +import Control.Monad (Functor, Monad) +import Control.Monad.Fix (MonadFix) +import Data.Bifunctor (Bifunctor) +import Data.Bifunctor.Clown (Clown) +import Data.Bifunctor.Joker (Joker) +import Data.Bifunctor.Product (Product) +import Data.Bifunctor.Sum (Sum) +import Data.Bifunctor.Tannen (Tannen) +import Data.Either (Either (..)) +import Data.Functor.Const (Const (..)) +import Data.Functor.Contravariant (Contravariant, Op (..)) +import Data.Kind (Type) +import Data.Monoid (Monoid) +import Data.Profunctor +import Data.Profunctor.Cayley (Cayley) +import Data.Profunctor.Choice (CopastroSum, CotambaraSum, PastroSum, TambaraSum) +import Data.Profunctor.Closed (Closure) +import Data.Profunctor.Composition (Procompose) +import Data.Profunctor.Mapping (CofreeMapping, FreeMapping) +import Data.Profunctor.Rep (Corepresentable) +import Data.Profunctor.Strong (Copastro, Pastro, Tambara) +import Data.Profunctor.Traversing (CofreeTraversing, FreeTraversing) +import Data.Profunctor.Yoneda (Coyoneda, Yoneda) +import Data.Semigroup (Arg) +import Data.Tagged (Tagged) +import Data.These (These (This, That)) +import Data.Traversable (Traversable) +import Data.Tuple (fst, snd) +import GHC.Generics (K1 (..)) + +-------------------------------------------------------------------------------- + +-- | Boilerplate newtype to derive modules for any 'Profunctor'. +newtype FromProfunctor p a b = FromProfunctor (p a b) + deriving newtype (Functor, Profunctor, Strong, Choice, Costrong, Cochoice) + +-- | Boilerplate newtype to derive modules for any 'Bifunctor'. +newtype FromBifunctor p a b = FromBifunctor (p a b) + deriving newtype (Functor, Bifunctor) + +-------------------------------------------------------------------------------- + +-- | A 'Profunctor' \(P : \mathcal{C}^{op} \times \mathcal{D} \to Set\) +-- is a Tambara 'LeftModule' if it is equipped with a morphism \(s_{a,b,m} : P(a, b) \to P(a \odot m, b \odot m)\), +-- which we call 'lstrength'. +-- +-- === Laws +-- +-- @ +-- 'Types.lmap' 'Control.Category.Cartesian.projl' ≡ 'Types.rmap' 'Control.Category.Cartesian.projl' 'Control.Category..' 'lstrength' +-- 'Data.Profunctor.Types.lmap' ('rstrength' @f@) 'Control.Category..' 'lstrength' ≡ 'Data.Profunctor.Types.rmap' ('rstrength' @f@) 'Control.Category..' 'lstrength' +-- 'lstrength' 'Control.Category..' 'lstrength' ≡ 'Types.dimap' ('Control.Category.Tensor.bwd' 'Control.Category.Tensor.assoc') ('Control.Category.Tensor.fwd' 'Control.Category.Tensor.assoc') 'Control.Category..' 'lstrength' +-- @ +class LeftModule cat t1 t2 p where + -- | ==== __Examples__ + -- + -- 'Data.Profiunctor.Strong.first'': + -- + -- >>> :t lstrength @(->) @(,) @(,) + -- lstrength @(->) @(,) @(,) :: LeftModule (->) (,) (,) p => p a b -> p (a, x) (b, x) + -- + -- 'Data.Profiunctor.Choice.left'': + -- + -- >>> :t lstrength @(->) @Either @Either + -- lstrength @(->) @Either @Either :: LeftModule (->) Either Either p => p a b -> p (Either a x) (Either b x) + lstrength :: cat (p a b) (p (t1 a x) (t2 b x)) + +instance Strong p => LeftModule (->) (,) (,) (FromProfunctor p) where + lstrength :: FromProfunctor p a b -> FromProfunctor p (a, x) (b, x) + lstrength = first' + +instance Choice p => LeftModule (->) Either Either (FromProfunctor p) where + lstrength :: FromProfunctor p a b -> FromProfunctor p (Either a x) (Either b x) + lstrength = left' + +instance Bifunctor p => LeftModule (->) Either Either (FromBifunctor p) where + lstrength :: FromBifunctor p a b -> FromBifunctor p (Either a x) (Either b x) + lstrength = gbimap Left Left + +instance Bifunctor p => LeftModule (->) These These (FromBifunctor p) where + lstrength :: FromBifunctor p a b -> FromBifunctor p (These a x) (These b x) + lstrength = gbimap This This + +instance Bifunctor p => LeftModule Op (,) (,) (FromBifunctor p) where + lstrength :: Op (FromBifunctor p a b) (FromBifunctor p (a, x) (b, x)) + lstrength = Op (gbimap fst fst) + +deriving via (FromProfunctor (Kleisli m)) instance Monad m => LeftModule (->) (,) (,) (Kleisli m) +deriving via (FromProfunctor (Pastro p)) instance LeftModule (->) (,) (,) (Pastro p) +deriving via (FromProfunctor (Tambara p)) instance Profunctor p => LeftModule (->) (,) (,) (Tambara p) +deriving via (FromProfunctor (Closure p)) instance Strong p => LeftModule (->) (,) (,) (Closure p) +deriving via (FromProfunctor (FreeTraversing p)) instance LeftModule (->) (,) (,) (FreeTraversing p) +deriving via (FromProfunctor (CofreeTraversing p)) instance Profunctor p => LeftModule (->) (,) (,) (CofreeTraversing p) +deriving via (FromProfunctor (FreeMapping p)) instance LeftModule (->) (,) (,) (FreeMapping p) +deriving via (FromProfunctor (CofreeMapping p)) instance Profunctor p => LeftModule (->) (,) (,) (CofreeMapping p) +deriving via (FromProfunctor (Coyoneda p)) instance Strong p => LeftModule (->) (,) (,) (Coyoneda p) +deriving via (FromProfunctor (Yoneda p)) instance Strong p => LeftModule (->) (,) (,) (Yoneda p) +deriving via (FromProfunctor (->)) instance LeftModule (->) (,) (,) (->) +deriving via (FromProfunctor (Forget r)) instance LeftModule (->) (,) (,) (Forget r) +deriving via (FromProfunctor (Star m)) instance Functor m => LeftModule (->) (,) (,) (Star m) +deriving via (FromProfunctor (Clown f)) instance Contravariant f => LeftModule (->) (,) (,) (Clown f) +deriving via (FromProfunctor (WrappedArrow p)) instance Arrow p => LeftModule (->) (,) (,) (WrappedArrow p) +deriving via (FromProfunctor (Sum p q)) instance (Strong p, Strong q) => LeftModule (->) (,) (,) (Sum p q) +deriving via (FromProfunctor (Product p q)) instance (Strong p, Strong q) => LeftModule (->) (,) (,) (Product p q) +deriving via (FromProfunctor (Tannen f q)) instance (Functor f, Strong q) => LeftModule (->) (,) (,) (Tannen f q) +deriving via (FromProfunctor (Procompose p q)) instance (Strong p, Strong q) => LeftModule (->) (,) (,) (Procompose p q) +deriving via (FromProfunctor (Cayley f q)) instance (Functor f, Strong q) => LeftModule (->) (,) (,) (Cayley f q) + +deriving via (FromProfunctor (Kleisli m)) instance Monad m => LeftModule (->) Either Either (Kleisli m) +deriving via (FromProfunctor Tagged) instance LeftModule (->) Either Either Tagged +deriving via (FromProfunctor (Tambara p)) instance (Choice p) => LeftModule (->) Either Either (Tambara p) +deriving via (FromProfunctor (PastroSum p)) instance LeftModule (->) Either Either (PastroSum p) +deriving via (FromProfunctor (TambaraSum p)) instance Profunctor p => LeftModule (->) Either Either (TambaraSum p) +deriving via (FromProfunctor (FreeTraversing p)) instance LeftModule (->) Either Either ( FreeTraversing p) +deriving via (FromProfunctor (CofreeTraversing p)) instance Profunctor p => LeftModule (->) Either Either (CofreeTraversing p) +deriving via (FromProfunctor (FreeMapping p )) instance LeftModule (->) Either Either (FreeMapping p) +deriving via (FromProfunctor (CofreeMapping p)) instance Profunctor p => LeftModule (->) Either Either (CofreeMapping p) +deriving via (FromProfunctor (Coyoneda p)) instance Choice p => LeftModule (->) Either Either (Coyoneda p) +deriving via (FromProfunctor (Yoneda p)) instance Choice p => LeftModule (->) Either Either (Yoneda p) +deriving via (FromProfunctor (->)) instance LeftModule (->) Either Either (->) +deriving via (FromProfunctor (Cokleisli w)) instance Comonad w => LeftModule (->) Either Either (Cokleisli w) +deriving via (FromProfunctor (Forget r)) instance Monoid r => LeftModule (->) Either Either (Forget r) +deriving via (FromProfunctor (Star f)) instance Applicative f => LeftModule (->) Either Either (Star f) +deriving via (FromProfunctor (Joker f)) instance Functor f => LeftModule (->) Either Either (Joker f) +deriving via (FromProfunctor (WrappedArrow p)) instance ArrowChoice p => LeftModule (->) Either Either (WrappedArrow p) +deriving via (FromProfunctor (Sum p q)) instance (Choice p, Choice q) => LeftModule (->) Either Either (Sum p q) +deriving via (FromProfunctor (Product p q)) instance (Choice p, Choice q) => LeftModule (->) Either Either (Product p q) +deriving via (FromProfunctor (Tannen f p)) instance (Functor f, Choice p) => LeftModule (->) Either Either (Tannen f p) +deriving via (FromProfunctor (Procompose p q)) instance (Choice p, Choice q) => LeftModule (->) Either Either (Procompose p q) +deriving via (FromProfunctor (Cayley f q)) instance (Functor f, Choice q) => LeftModule (->) Either Either (Cayley f q) + +deriving via (FromBifunctor Arg) instance LeftModule (->) Either Either Arg +deriving via (FromBifunctor Const) instance LeftModule (->) Either Either Const +deriving via (FromBifunctor Either) instance LeftModule (->) Either Either Either +deriving via (FromBifunctor These) instance LeftModule (->) Either Either These +deriving via (FromBifunctor (K1 i)) instance LeftModule (->) Either Either (K1 i :: Type -> Type -> Type) +deriving via (FromBifunctor (,)) instance LeftModule (->) Either Either (,) +deriving via (FromBifunctor ((,,) x1)) instance LeftModule (->) Either Either ((,,) x1) +deriving via (FromBifunctor ((,,,) x1 x2)) instance LeftModule (->) Either Either ((,,,) x1 x2) +deriving via (FromBifunctor ((,,,,) x1 x2 x3)) instance LeftModule (->) Either Either ((,,,,) x1 x2 x3) +deriving via (FromBifunctor ((,,,,,) x1 x2 x3 x4)) instance LeftModule (->) Either Either ((,,,,,) x1 x2 x3 x4) +deriving via (FromBifunctor ((,,,,,,) x1 x2 x3 x4 x5)) instance LeftModule (->) Either Either ((,,,,,,) x1 x2 x3 x4 x5) + +deriving via (FromBifunctor Arg) instance LeftModule (->) These These Arg +deriving via (FromBifunctor Const) instance LeftModule (->) These These Const +deriving via (FromBifunctor Either) instance LeftModule (->) These These Either +deriving via (FromBifunctor These) instance LeftModule (->) These These These +deriving via (FromBifunctor (K1 i)) instance LeftModule (->) These These (K1 i :: Type -> Type -> Type) +deriving via (FromBifunctor (,)) instance LeftModule (->) These These (,) +deriving via (FromBifunctor ((,,) x1)) instance LeftModule (->) These These ((,,) x1) +deriving via (FromBifunctor ((,,,) x1 x2)) instance LeftModule (->) These These ((,,,) x1 x2) +deriving via (FromBifunctor ((,,,,) x1 x2 x3)) instance LeftModule (->) These These ((,,,,) x1 x2 x3) +deriving via (FromBifunctor ((,,,,,) x1 x2 x3 x4)) instance LeftModule (->) These These ((,,,,,) x1 x2 x3 x4) +deriving via (FromBifunctor ((,,,,,,) x1 x2 x3 x4 x5)) instance LeftModule (->) These These ((,,,,,,) x1 x2 x3 x4 x5) + +deriving via (FromBifunctor Arg) instance LeftModule Op (,) (,) Arg +deriving via (FromBifunctor Const) instance LeftModule Op (,) (,) Const +deriving via (FromBifunctor Either) instance LeftModule Op (,) (,) Either +deriving via (FromBifunctor These) instance LeftModule Op (,) (,) These +deriving via (FromBifunctor (K1 i)) instance LeftModule Op (,) (,) (K1 i :: Type -> Type -> Type) +deriving via (FromBifunctor (,)) instance LeftModule Op (,) (,) (,) +deriving via (FromBifunctor ((,,) x1)) instance LeftModule Op (,) (,) ((,,) x1) +deriving via (FromBifunctor ((,,,) x1 x2)) instance LeftModule Op (,) (,) ((,,,) x1 x2) +deriving via (FromBifunctor ((,,,,) x1 x2 x3)) instance LeftModule Op (,) (,) ((,,,,) x1 x2 x3) +deriving via (FromBifunctor ((,,,,,) x1 x2 x3 x4)) instance LeftModule Op (,) (,) ((,,,,,) x1 x2 x3 x4) +deriving via (FromBifunctor ((,,,,,,) x1 x2 x3 x4 x5)) instance LeftModule Op (,) (,) ((,,,,,,) x1 x2 x3 x4 x5) + +-------------------------------------------------------------------------------- + +-- | A 'Profunctor' \(P : \mathcal{C}^{op} \times \mathcal{D} \to Set\) +-- is a Tambara 'RightModule' if it is equipped with a morphism \(s_{a,b,m} : P(a, b) \to P(m \odot a, m \odot b)\), +-- which we call 'rstrength'. +-- +-- === Laws +-- +-- @ +-- 'Data.Profunctor.Types.lmap' 'Control.Category.Cartesian.projr' ≡ 'Data.Profunctor.Types.rmap' 'Control.Category.Cartesian.projr' 'Control.Category..' 'rstrength' +-- 'Data.Profunctor.Types.lmap' ('lstrength' @f@) 'Control.Category..' 'rstrength' ≡ 'Data.Profunctor.Types.rmap' ('lstrength' @f@) 'Control.Category..' 'rstrength' +-- 'rstrength' 'Control.Category..' 'rstrength' ≡ 'Data.Profunctor.Types.dimap' ('Control.Category.Tensor.fwd' 'Control.Category.Tensor.assoc') ('Control.Category.Tensor.bwd' 'Control.Category.Tensor.assoc') 'Control.Category..' 'rstrength' +-- @ class RightModule cat t1 t2 f where - rstrength :: cat (f a b) (f (t1 x a) (t2 x b)) + -- | ==== __Examples__ + -- + -- 'Data.Profunctor.Strong.second'': + -- + -- >>> :t rstrength @(->) @(,) @(,) + -- rstrength @(->) @(,) @(,) :: RightModule (->) (,) (,) f => f a b -> f (x, a) (x, b) + -- + -- 'Data.Profunctor.Choice.right'': + -- + -- >>> :t rstrength @(->) @Either @Either + -- rstrength @(->) @Either @Either :: RightModule (->) Either Either f => f a b -> f (Either x a) (Either x b) + rstrength :: cat (f a b) (f (x `t1` a) (x `t2` b)) +instance Strong p => RightModule (->) (,) (,) (FromProfunctor p) where + rstrength :: FromProfunctor p a b -> FromProfunctor p (c, a) (c, b) + rstrength = second' + +instance Choice p => RightModule (->) Either Either (FromProfunctor p) where + rstrength :: FromProfunctor p a b -> FromProfunctor p (Either c a) (Either c b) + rstrength = right' + +instance Bifunctor p => RightModule (->) Either Either (FromBifunctor p) where + rstrength :: FromBifunctor p a b -> FromBifunctor p (Either x a) (Either x b) + rstrength = gbimap Right Right + +instance Bifunctor p => RightModule (->) These These (FromBifunctor p) where + rstrength :: FromBifunctor p a b -> FromBifunctor p (These x a) (These x b) + rstrength = gbimap That That + +instance Bifunctor p => RightModule Op (,) (,) (FromBifunctor p) where + rstrength :: Op (FromBifunctor p a b) (FromBifunctor p (x, a) (x, b)) + rstrength = Op (gbimap snd snd) + +deriving via (FromProfunctor (Kleisli m)) instance Monad m => RightModule (->) (,) (,) (Kleisli m) +deriving via (FromProfunctor (Pastro p)) instance RightModule (->) (,) (,) (Pastro p) +deriving via (FromProfunctor (Tambara p)) instance Profunctor p => RightModule (->) (,) (,) (Tambara p) +deriving via (FromProfunctor (Closure p)) instance Strong p => RightModule (->) (,) (,) (Closure p) +deriving via (FromProfunctor (FreeTraversing p)) instance RightModule (->) (,) (,) (FreeTraversing p) +deriving via (FromProfunctor (CofreeTraversing p)) instance Profunctor p => RightModule (->) (,) (,) (CofreeTraversing p) +deriving via (FromProfunctor (FreeMapping p)) instance RightModule (->) (,) (,) (FreeMapping p) +deriving via (FromProfunctor (CofreeMapping p)) instance Profunctor p => RightModule (->) (,) (,) (CofreeMapping p) +deriving via (FromProfunctor (Coyoneda p)) instance Strong p => RightModule (->) (,) (,) (Coyoneda p) +deriving via (FromProfunctor (Yoneda p)) instance Strong p => RightModule (->) (,) (,) (Yoneda p) +deriving via (FromProfunctor (->)) instance RightModule (->) (,) (,) (->) +deriving via (FromProfunctor (Forget r)) instance RightModule (->) (,) (,) (Forget r) +deriving via (FromProfunctor (Star m)) instance Functor m => RightModule (->) (,) (,) (Star m) +deriving via (FromProfunctor (Clown f)) instance Contravariant f => RightModule (->) (,) (,) (Clown f) +deriving via (FromProfunctor (WrappedArrow p)) instance Arrow p => RightModule (->) (,) (,) (WrappedArrow p) +deriving via (FromProfunctor (Sum p q)) instance (Strong p, Strong q) => RightModule (->) (,) (,) (Sum p q) +deriving via (FromProfunctor (Product p q)) instance (Strong p, Strong q) => RightModule (->) (,) (,) (Product p q) +deriving via (FromProfunctor (Tannen f q)) instance (Functor f, Strong q) => RightModule (->) (,) (,) (Tannen f q) +deriving via (FromProfunctor (Procompose p q)) instance (Strong p, Strong q) => RightModule (->) (,) (,) (Procompose p q) +deriving via (FromProfunctor (Cayley f q)) instance (Functor f, Strong q) => RightModule (->) (,) (,) (Cayley f q) + +deriving via (FromProfunctor (Kleisli m)) instance Monad m => RightModule (->) Either Either (Kleisli m) +deriving via (FromProfunctor Tagged) instance RightModule (->) Either Either Tagged +deriving via (FromProfunctor (Tambara p)) instance (Choice p) => RightModule (->) Either Either (Tambara p) +deriving via (FromProfunctor (PastroSum p)) instance RightModule (->) Either Either (PastroSum p) +deriving via (FromProfunctor (TambaraSum p)) instance Profunctor p => RightModule (->) Either Either (TambaraSum p) +deriving via (FromProfunctor (FreeTraversing p)) instance RightModule (->) Either Either ( FreeTraversing p) +deriving via (FromProfunctor (CofreeTraversing p)) instance Profunctor p => RightModule (->) Either Either (CofreeTraversing p) +deriving via (FromProfunctor (FreeMapping p )) instance RightModule (->) Either Either (FreeMapping p) +deriving via (FromProfunctor (CofreeMapping p)) instance Profunctor p => RightModule (->) Either Either (CofreeMapping p) +deriving via (FromProfunctor (Coyoneda p)) instance Choice p => RightModule (->) Either Either (Coyoneda p) +deriving via (FromProfunctor (Yoneda p)) instance Choice p => RightModule (->) Either Either (Yoneda p) +deriving via (FromProfunctor (->)) instance RightModule (->) Either Either (->) +deriving via (FromProfunctor (Cokleisli w)) instance Comonad w => RightModule (->) Either Either (Cokleisli w) +deriving via (FromProfunctor (Forget r)) instance Monoid r => RightModule (->) Either Either (Forget r) +deriving via (FromProfunctor (Star f)) instance Applicative f => RightModule (->) Either Either (Star f) +deriving via (FromProfunctor (Joker f)) instance Functor f => RightModule (->) Either Either (Joker f) +deriving via (FromProfunctor (WrappedArrow p)) instance ArrowChoice p => RightModule (->) Either Either (WrappedArrow p) +deriving via (FromProfunctor (Sum p q)) instance (Choice p, Choice q) => RightModule (->) Either Either (Sum p q) +deriving via (FromProfunctor (Product p q)) instance (Choice p, Choice q) => RightModule (->) Either Either (Product p q) +deriving via (FromProfunctor (Tannen f p)) instance (Functor f, Choice p) => RightModule (->) Either Either (Tannen f p) +deriving via (FromProfunctor (Procompose p q)) instance (Choice p, Choice q) => RightModule (->) Either Either (Procompose p q) +deriving via (FromProfunctor (Cayley f q)) instance (Functor f, Choice q) => RightModule (->) Either Either (Cayley f q) + +deriving via (FromBifunctor Arg) instance RightModule (->) Either Either Arg +deriving via (FromBifunctor Const) instance RightModule (->) Either Either Const +deriving via (FromBifunctor Either) instance RightModule (->) Either Either Either +deriving via (FromBifunctor These) instance RightModule (->) Either Either These +deriving via (FromBifunctor (K1 i)) instance RightModule (->) Either Either (K1 i :: Type -> Type -> Type) +deriving via (FromBifunctor (,)) instance RightModule (->) Either Either (,) +deriving via (FromBifunctor ((,,) x1)) instance RightModule (->) Either Either ((,,) x1) +deriving via (FromBifunctor ((,,,) x1 x2)) instance RightModule (->) Either Either ((,,,) x1 x2) +deriving via (FromBifunctor ((,,,,) x1 x2 x3)) instance RightModule (->) Either Either ((,,,,) x1 x2 x3) +deriving via (FromBifunctor ((,,,,,) x1 x2 x3 x4)) instance RightModule (->) Either Either ((,,,,,) x1 x2 x3 x4) +deriving via (FromBifunctor ((,,,,,,) x1 x2 x3 x4 x5)) instance RightModule (->) Either Either ((,,,,,,) x1 x2 x3 x4 x5) + +deriving via (FromBifunctor Arg) instance RightModule (->) These These Arg +deriving via (FromBifunctor Const) instance RightModule (->) These These Const +deriving via (FromBifunctor Either) instance RightModule (->) These These Either +deriving via (FromBifunctor These) instance RightModule (->) These These These +deriving via (FromBifunctor (K1 i)) instance RightModule (->) These These (K1 i :: Type -> Type -> Type) +deriving via (FromBifunctor (,)) instance RightModule (->) These These (,) +deriving via (FromBifunctor ((,,) x1)) instance RightModule (->) These These ((,,) x1) +deriving via (FromBifunctor ((,,,) x1 x2)) instance RightModule (->) These These ((,,,) x1 x2) +deriving via (FromBifunctor ((,,,,) x1 x2 x3)) instance RightModule (->) These These ((,,,,) x1 x2 x3) +deriving via (FromBifunctor ((,,,,,) x1 x2 x3 x4)) instance RightModule (->) These These ((,,,,,) x1 x2 x3 x4) +deriving via (FromBifunctor ((,,,,,,) x1 x2 x3 x4 x5)) instance RightModule (->) These These ((,,,,,,) x1 x2 x3 x4 x5) + +deriving via (FromBifunctor Arg) instance RightModule Op (,) (,) Arg +deriving via (FromBifunctor Const) instance RightModule Op (,) (,) Const +deriving via (FromBifunctor Either) instance RightModule Op (,) (,) Either +deriving via (FromBifunctor These) instance RightModule Op (,) (,) These +deriving via (FromBifunctor (K1 i)) instance RightModule Op (,) (,) (K1 i :: Type -> Type -> Type) +deriving via (FromBifunctor (,)) instance RightModule Op (,) (,) (,) +deriving via (FromBifunctor ((,,) x1)) instance RightModule Op (,) (,) ((,,) x1) +deriving via (FromBifunctor ((,,,) x1 x2)) instance RightModule Op (,) (,) ((,,,) x1 x2) +deriving via (FromBifunctor ((,,,,) x1 x2 x3)) instance RightModule Op (,) (,) ((,,,,) x1 x2 x3) +deriving via (FromBifunctor ((,,,,,) x1 x2 x3 x4)) instance RightModule Op (,) (,) ((,,,,,) x1 x2 x3 x4) +deriving via (FromBifunctor ((,,,,,,) x1 x2 x3 x4 x5)) instance RightModule Op (,) (,) ((,,,,,,) x1 x2 x3 x4 x5) + +-------------------------------------------------------------------------------- + +-- | A 'Profunctor' equipped with both a Tambara 'LeftModule' and +-- Tambara 'RightModule' is a 'Bimodule'. +-- +-- === Laws +-- +-- @ +-- 'rstrength' ≡ 'Data.Profunctor.Types.dimap' 'Control.Category.Tensor.swap' 'Control.Category.Tensor.swap' 'Control.Category..' 'lstrength' +-- 'lstrength' ≡ 'Data.Profunctor.Types.dimap' 'Control.Category.Tensor.swap' 'Control.Category.Tensor.swap' 'Control.Category..' 'rstrength' +-- @ class (LeftModule cat t1 t2 f, RightModule cat t1 t2 f) => Bimodule cat t1 t2 f + +instance Strong p => Bimodule (->) (,) (,) (FromProfunctor p) +instance Choice p => Bimodule (->) Either Either (FromProfunctor p) +instance Bifunctor p => Bimodule (->) Either Either (FromBifunctor p) +instance Bifunctor p => Bimodule (->) These These (FromBifunctor p) +instance Bifunctor p => Bimodule Op (,) (,) (FromBifunctor p) + +deriving via (FromProfunctor (Kleisli m)) instance Monad m => Bimodule (->) (,) (,) (Kleisli m) +deriving via (FromProfunctor (Pastro p)) instance Bimodule (->) (,) (,) (Pastro p) +deriving via (FromProfunctor (Tambara p)) instance Profunctor p => Bimodule (->) (,) (,) (Tambara p) +deriving via (FromProfunctor (Closure p)) instance Strong p => Bimodule (->) (,) (,) (Closure p) +deriving via (FromProfunctor (FreeTraversing p)) instance Bimodule (->) (,) (,) (FreeTraversing p) +deriving via (FromProfunctor (CofreeTraversing p)) instance Profunctor p => Bimodule (->) (,) (,) (CofreeTraversing p) +deriving via (FromProfunctor (FreeMapping p)) instance Bimodule (->) (,) (,) (FreeMapping p) +deriving via (FromProfunctor (CofreeMapping p)) instance Profunctor p => Bimodule (->) (,) (,) (CofreeMapping p) +deriving via (FromProfunctor (Coyoneda p)) instance Strong p => Bimodule (->) (,) (,) (Coyoneda p) +deriving via (FromProfunctor (Yoneda p)) instance Strong p => Bimodule (->) (,) (,) (Yoneda p) +deriving via (FromProfunctor (->)) instance Bimodule (->) (,) (,) (->) +deriving via (FromProfunctor (Forget r)) instance Bimodule (->) (,) (,) (Forget r) +deriving via (FromProfunctor (Star m)) instance Functor m => Bimodule (->) (,) (,) (Star m) +deriving via (FromProfunctor (Clown f)) instance Contravariant f => Bimodule (->) (,) (,) (Clown f) +deriving via (FromProfunctor (WrappedArrow p)) instance Arrow p => Bimodule (->) (,) (,) (WrappedArrow p) +deriving via (FromProfunctor (Sum p q)) instance (Strong p, Strong q) => Bimodule (->) (,) (,) (Sum p q) +deriving via (FromProfunctor (Product p q)) instance (Strong p, Strong q) => Bimodule (->) (,) (,) (Product p q) +deriving via (FromProfunctor (Tannen f q)) instance (Functor f, Strong q) => Bimodule (->) (,) (,) (Tannen f q) +deriving via (FromProfunctor (Procompose p q)) instance (Strong p, Strong q) => Bimodule (->) (,) (,) (Procompose p q) +deriving via (FromProfunctor (Cayley f q)) instance (Functor f, Strong q) => Bimodule (->) (,) (,) (Cayley f q) + +deriving via (FromProfunctor (Kleisli m)) instance Monad m => Bimodule (->) Either Either (Kleisli m) +deriving via (FromProfunctor Tagged) instance Bimodule (->) Either Either Tagged +deriving via (FromProfunctor (Tambara p)) instance (Choice p) => Bimodule (->) Either Either (Tambara p) +deriving via (FromProfunctor (PastroSum p)) instance Bimodule (->) Either Either (PastroSum p) +deriving via (FromProfunctor (TambaraSum p)) instance Profunctor p => Bimodule (->) Either Either (TambaraSum p) +deriving via (FromProfunctor (FreeTraversing p)) instance Bimodule (->) Either Either ( FreeTraversing p) +deriving via (FromProfunctor (CofreeTraversing p)) instance Profunctor p => Bimodule (->) Either Either (CofreeTraversing p) +deriving via (FromProfunctor (FreeMapping p )) instance Bimodule (->) Either Either (FreeMapping p) +deriving via (FromProfunctor (CofreeMapping p)) instance Profunctor p => Bimodule (->) Either Either (CofreeMapping p) +deriving via (FromProfunctor (Coyoneda p)) instance Choice p => Bimodule (->) Either Either (Coyoneda p) +deriving via (FromProfunctor (Yoneda p)) instance Choice p => Bimodule (->) Either Either (Yoneda p) +deriving via (FromProfunctor (->)) instance Bimodule (->) Either Either (->) +deriving via (FromProfunctor (Cokleisli w)) instance Comonad w => Bimodule (->) Either Either (Cokleisli w) +deriving via (FromProfunctor (Forget r)) instance Monoid r => Bimodule (->) Either Either (Forget r) +deriving via (FromProfunctor (Star f)) instance Applicative f => Bimodule (->) Either Either (Star f) +deriving via (FromProfunctor (Joker f)) instance Functor f => Bimodule (->) Either Either (Joker f) +deriving via (FromProfunctor (WrappedArrow p)) instance ArrowChoice p => Bimodule (->) Either Either (WrappedArrow p) +deriving via (FromProfunctor (Sum p q)) instance (Choice p, Choice q) => Bimodule (->) Either Either (Sum p q) +deriving via (FromProfunctor (Product p q)) instance (Choice p, Choice q) => Bimodule (->) Either Either (Product p q) +deriving via (FromProfunctor (Tannen f p)) instance (Functor f, Choice p) => Bimodule (->) Either Either (Tannen f p) +deriving via (FromProfunctor (Procompose p q)) instance (Choice p, Choice q) => Bimodule (->) Either Either (Procompose p q) +deriving via (FromProfunctor (Cayley f q)) instance (Functor f, Choice q) => Bimodule (->) Either Either (Cayley f q) + +deriving via (FromBifunctor Arg) instance Bimodule (->) Either Either Arg +deriving via (FromBifunctor Const) instance Bimodule (->) Either Either Const +deriving via (FromBifunctor Either) instance Bimodule (->) Either Either Either +deriving via (FromBifunctor These) instance Bimodule (->) Either Either These +deriving via (FromBifunctor (K1 i)) instance Bimodule (->) Either Either (K1 i :: Type -> Type -> Type) +deriving via (FromBifunctor (,)) instance Bimodule (->) Either Either (,) +deriving via (FromBifunctor ((,,) x1)) instance Bimodule (->) Either Either ((,,) x1) +deriving via (FromBifunctor ((,,,) x1 x2)) instance Bimodule (->) Either Either ((,,,) x1 x2) +deriving via (FromBifunctor ((,,,,) x1 x2 x3)) instance Bimodule (->) Either Either ((,,,,) x1 x2 x3) +deriving via (FromBifunctor ((,,,,,) x1 x2 x3 x4)) instance Bimodule (->) Either Either ((,,,,,) x1 x2 x3 x4) +deriving via (FromBifunctor ((,,,,,,) x1 x2 x3 x4 x5)) instance Bimodule (->) Either Either ((,,,,,,) x1 x2 x3 x4 x5) + +deriving via (FromBifunctor Arg) instance Bimodule (->) These These Arg +deriving via (FromBifunctor Const) instance Bimodule (->) These These Const +deriving via (FromBifunctor Either) instance Bimodule (->) These These Either +deriving via (FromBifunctor These) instance Bimodule (->) These These These +deriving via (FromBifunctor (K1 i)) instance Bimodule (->) These These (K1 i :: Type -> Type -> Type) +deriving via (FromBifunctor (,)) instance Bimodule (->) These These (,) +deriving via (FromBifunctor ((,,) x1)) instance Bimodule (->) These These ((,,) x1) +deriving via (FromBifunctor ((,,,) x1 x2)) instance Bimodule (->) These These ((,,,) x1 x2) +deriving via (FromBifunctor ((,,,,) x1 x2 x3)) instance Bimodule (->) These These ((,,,,) x1 x2 x3) +deriving via (FromBifunctor ((,,,,,) x1 x2 x3 x4)) instance Bimodule (->) These These ((,,,,,) x1 x2 x3 x4) +deriving via (FromBifunctor ((,,,,,,) x1 x2 x3 x4 x5)) instance Bimodule (->) These These ((,,,,,,) x1 x2 x3 x4 x5) + +deriving via (FromBifunctor Arg) instance Bimodule Op (,) (,) Arg +deriving via (FromBifunctor Const) instance Bimodule Op (,) (,) Const +deriving via (FromBifunctor Either) instance Bimodule Op (,) (,) Either +deriving via (FromBifunctor These) instance Bimodule Op (,) (,) These +deriving via (FromBifunctor (K1 i)) instance Bimodule Op (,) (,) (K1 i :: Type -> Type -> Type) +deriving via (FromBifunctor (,)) instance Bimodule Op (,) (,) (,) +deriving via (FromBifunctor ((,,) x1)) instance Bimodule Op (,) (,) ((,,) x1) +deriving via (FromBifunctor ((,,,) x1 x2)) instance Bimodule Op (,) (,) ((,,,) x1 x2) +deriving via (FromBifunctor ((,,,,) x1 x2 x3)) instance Bimodule Op (,) (,) ((,,,,) x1 x2 x3) +deriving via (FromBifunctor ((,,,,,) x1 x2 x3 x4)) instance Bimodule Op (,) (,) ((,,,,,) x1 x2 x3 x4) +deriving via (FromBifunctor ((,,,,,,) x1 x2 x3 x4 x5)) instance Bimodule Op (,) (,) ((,,,,,,) x1 x2 x3 x4 x5) + +-------------------------------------------------------------------------------- + +-- | A 'Profunctor' \(P : \mathcal{C}^{op} \times \mathcal{D} \to Set\) +-- is a Tambara 'LeftCoModule' if it is equipped with a morphism \(s^{-1}_{a,b,m} : P(a \odot m, a \odot m) \to P(a, b) \), +-- which we call 'lcostrength'. +-- +-- === Laws +-- +-- @ +-- 'Data.Profunctor.Types.Data.Profunctor.Types.lmap' 'Control.Category.Cartesian.incll' ≡ 'lcostrength' 'Control.Category..' 'Data.Profunctor.Types.rmap' 'Control.Category.Cartesian.incll' +-- 'lcostrength' 'Control.Category..' 'Data.Profunctor.Types.lmap' ('rstrength' f) ≡ 'lcostrength' 'Control.Category..' 'Data.Profunctor.Types.rmap' ('rstrength' f) +-- 'lcostrength' 'Control.Category..' 'lcostrength' ≡ 'lcostrength' 'Control.Category..' 'Data.Profunctor.Types.dimap' ('Control.Category.Tensor.fwd' 'Control.Category.Tensor.assoc') ('Control.Category.Tensor.bwd' 'Control.Category.Tensor.assoc') +-- @ +class LeftCoModule cat t1 t2 f where + -- | ==== __Examples__ + -- + -- 'Data.Profunctor.Strong.unfirst': + -- + -- >>> :t lcostrength @(->) @(,) @(,) + -- lcostrength @(->) @(,) @(,) :: LeftCoModule (->) (,) (,) f => f (a, x) (b, x) -> f a b + -- + -- 'Data.Profunctor.Choice.unleft': + -- + -- >>> :t lcostrength @(->) @Either @Either + -- lcostrength @(->) @Either @Either :: LeftCoModule (->) Either Either f => f (Either a x) (Either b x) -> f a b + lcostrength :: cat (f (t1 a x) (t2 b x)) (f a b) + +instance Costrong p => LeftCoModule (->) (,) (,) (FromProfunctor p) where + lcostrength :: FromProfunctor p (a, x) (b, x) -> FromProfunctor p a b + lcostrength = unfirst + +instance Cochoice p => LeftCoModule (->) Either Either (FromProfunctor p) where + lcostrength :: Cochoice p => FromProfunctor p (Either a x) (Either b x) -> FromProfunctor p a b + lcostrength = unleft + +instance Bifunctor p => LeftCoModule (->) (,) (,) (FromBifunctor p) where + lcostrength :: Bifunctor p => FromBifunctor p (a, x) (b, x) -> FromBifunctor p a b + lcostrength = gbimap fst fst + +instance Bifunctor p => LeftCoModule Op Either Either (FromBifunctor p) where + lcostrength :: Bifunctor p => Op (FromBifunctor p (Either a x) (Either b x)) (FromBifunctor p a b) + lcostrength = Op (gbimap Left Left) + +instance Bifunctor p => LeftCoModule Op These These (FromBifunctor p) where + lcostrength :: Bifunctor p => Op (FromBifunctor p (These a x) (These b x)) (FromBifunctor p a b) + lcostrength = Op (gbimap This This) + +deriving via (FromProfunctor (Kleisli m)) instance MonadFix m => LeftCoModule (->) (,) (,) (Kleisli m) +deriving via (FromProfunctor Tagged) instance LeftCoModule (->) (,) (,) Tagged +deriving via (FromProfunctor (Coyoneda p)) instance Costrong p => LeftCoModule (->) (,) (,) (Coyoneda p) +deriving via (FromProfunctor (Copastro p)) instance Cochoice p => LeftCoModule (->) (,) (,) (Copastro p) +deriving via (FromProfunctor (Yoneda p)) instance Costrong p => LeftCoModule (->) (,) (,) (Yoneda p) +deriving via (FromProfunctor (->)) instance LeftCoModule (->) (,) (,) (->) +deriving via (FromProfunctor (Cokleisli f)) instance Functor f => LeftCoModule (->) (,) (,) (Cokleisli f) +deriving via (FromProfunctor (Costar f)) instance Functor f => LeftCoModule (->) (,) (,) (Costar f) +deriving via (FromProfunctor (WrappedArrow p)) instance ArrowLoop p => LeftCoModule (->) (,) (,) (WrappedArrow p) +deriving via (FromProfunctor (Sum p q)) instance (Costrong p, Costrong q) => LeftCoModule (->) (,) (,) (Sum p q) +deriving via (FromProfunctor (Product p q)) instance (Costrong p, Costrong q) => LeftCoModule (->) (,) (,) (Product p q) +deriving via (FromProfunctor (Tannen f p)) instance (Functor f, Costrong p) => LeftCoModule (->) (,) (,) (Tannen f p) +deriving via (FromProfunctor (Procompose p q)) instance (Corepresentable p, Corepresentable q) => LeftCoModule (->) (,) (,) (Procompose p q) +deriving via (FromProfunctor (Cayley f p)) instance (Functor f, Costrong p) => LeftCoModule (->) (,) (,) (Cayley f p) + +deriving via (FromProfunctor (CopastroSum p)) instance LeftCoModule (->) Either Either (CopastroSum p) +deriving via (FromProfunctor (CotambaraSum p)) instance LeftCoModule (->) Either Either (CotambaraSum p) +deriving via (FromProfunctor (Coyoneda p)) instance Cochoice p => LeftCoModule (->) Either Either (Coyoneda p) +deriving via (FromProfunctor (Yoneda p)) instance Cochoice p => LeftCoModule (->) Either Either (Yoneda p) +deriving via (FromProfunctor (->)) instance LeftCoModule (->) Either Either (->) +deriving via (FromProfunctor (Forget r)) instance LeftCoModule (->) Either Either (Forget r) +deriving via (FromProfunctor (Costar f)) instance Applicative f => LeftCoModule (->) Either Either (Costar f) +deriving via (FromProfunctor (Star f)) instance Traversable f => LeftCoModule (->) Either Either (Star f) +deriving via (FromProfunctor (Sum p q)) instance (Cochoice p, Cochoice q) => LeftCoModule (->) Either Either (Sum p q) +deriving via (FromProfunctor (Product p q)) instance (Cochoice p, Cochoice q) => LeftCoModule (->) Either Either (Product p q) +deriving via (FromProfunctor (Tannen f p)) instance (Functor f, Cochoice p) => LeftCoModule (->) Either Either (Tannen f p) +deriving via (FromProfunctor (Cayley f p)) instance (Functor f, Cochoice p) => LeftCoModule (->) Either Either (Cayley f p) + +deriving via (FromBifunctor Arg) instance LeftCoModule (->) (,) (,) Arg +deriving via (FromBifunctor Const) instance LeftCoModule (->) (,) (,) Const +deriving via (FromBifunctor Either) instance LeftCoModule (->) (,) (,) Either +deriving via (FromBifunctor These) instance LeftCoModule (->) (,) (,) These +deriving via (FromBifunctor (K1 i)) instance LeftCoModule (->) (,) (,) (K1 i :: Type -> Type -> Type) +deriving via (FromBifunctor (,)) instance LeftCoModule (->) (,) (,) (,) +deriving via (FromBifunctor ((,,) x1)) instance LeftCoModule (->) (,) (,) ((,,) x1) +deriving via (FromBifunctor ((,,,) x1 x2)) instance LeftCoModule (->) (,) (,) ((,,,) x1 x2) +deriving via (FromBifunctor ((,,,,) x1 x2 x3)) instance LeftCoModule (->) (,) (,) ((,,,,) x1 x2 x3) +deriving via (FromBifunctor ((,,,,,) x1 x2 x3 x4)) instance LeftCoModule (->) (,) (,) ((,,,,,) x1 x2 x3 x4) +deriving via (FromBifunctor ((,,,,,,) x1 x2 x3 x4 x5)) instance LeftCoModule (->) (,) (,) ((,,,,,,) x1 x2 x3 x4 x5) + +deriving via (FromBifunctor Arg) instance LeftCoModule Op Either Either Arg +deriving via (FromBifunctor Const) instance LeftCoModule Op Either Either Const +deriving via (FromBifunctor Either) instance LeftCoModule Op Either Either Either +deriving via (FromBifunctor These) instance LeftCoModule Op Either Either These +deriving via (FromBifunctor (K1 i)) instance LeftCoModule Op Either Either (K1 i :: Type -> Type -> Type) +deriving via (FromBifunctor (,)) instance LeftCoModule Op Either Either (,) +deriving via (FromBifunctor ((,,) x1)) instance LeftCoModule Op Either Either ((,,) x1) +deriving via (FromBifunctor ((,,,) x1 x2)) instance LeftCoModule Op Either Either ((,,,) x1 x2) +deriving via (FromBifunctor ((,,,,) x1 x2 x3)) instance LeftCoModule Op Either Either ((,,,,) x1 x2 x3) +deriving via (FromBifunctor ((,,,,,) x1 x2 x3 x4)) instance LeftCoModule Op Either Either ((,,,,,) x1 x2 x3 x4) +deriving via (FromBifunctor ((,,,,,,) x1 x2 x3 x4 x5)) instance LeftCoModule Op Either Either ((,,,,,,) x1 x2 x3 x4 x5) + +deriving via (FromBifunctor Arg) instance LeftCoModule Op These These Arg +deriving via (FromBifunctor Const) instance LeftCoModule Op These These Const +deriving via (FromBifunctor Either) instance LeftCoModule Op These These Either +deriving via (FromBifunctor These) instance LeftCoModule Op These These These +deriving via (FromBifunctor (K1 i)) instance LeftCoModule Op These These (K1 i :: Type -> Type -> Type) +deriving via (FromBifunctor (,)) instance LeftCoModule Op These These (,) +deriving via (FromBifunctor ((,,) x1)) instance LeftCoModule Op These These ((,,) x1) +deriving via (FromBifunctor ((,,,) x1 x2)) instance LeftCoModule Op These These ((,,,) x1 x2) +deriving via (FromBifunctor ((,,,,) x1 x2 x3)) instance LeftCoModule Op These These ((,,,,) x1 x2 x3) +deriving via (FromBifunctor ((,,,,,) x1 x2 x3 x4)) instance LeftCoModule Op These These ((,,,,,) x1 x2 x3 x4) +deriving via (FromBifunctor ((,,,,,,) x1 x2 x3 x4 x5)) instance LeftCoModule Op These These ((,,,,,,) x1 x2 x3 x4 x5) + +-------------------------------------------------------------------------------- + +-- | A 'Profunctor' \(P : \mathcal{C}^{op} \times \mathcal{D} \to Set\) +-- is a Tambara 'RightCoModule' if it is equipped with a morphism \(s^{-1}_{a,b,m} : P(m \odot a, m \odot a) \to P(a, b) \), +-- which we call 'rcostrength'. +-- +-- === Laws +-- +-- @ +-- 'Data.Profunctor.Types.Data.Profunctor.Types.lmap' 'Control.Category.Cartesian.inclr' ≡ 'rcostrength' 'Control.Category..' 'Data.Profunctor.Types.rmap' 'Control.Category.Cartesian.inclr' +-- 'rcostrength' 'Control.Category..' 'Data.Profunctor.Types.lmap' ('lstrength' f) ≡ 'rcostrength' 'Control.Category..' 'Data.Profunctor.Types.rmap' ('lstrength' f) +-- 'rcostrength' 'Control.Category..' 'rcostrength' ≡ 'rcostrength' 'Control.Category..' 'Data.Profunctor.Types.dimap' ('Control.Category.Tensor.bwd' 'Control.Category.Tensor.assoc') ('Control.Category.Tensor.fwd' 'Control.Category.Tensor.assoc') +-- @ +class RightCoModule cat t1 t2 f where + -- | ==== __Examples__ + -- + -- 'Data.Profunctor.Strong.unsecond': + -- + -- >>> :t rcostrength @(->) @(,) @(,) + -- rcostrength @(->) @(,) @(,) :: RightCoModule (->) (,) (,) f => f (x, a) (x, b) -> f a b + -- + -- 'Data.Profunctor.Choice.unright': + -- + -- >>> :t rcostrength @(->) @Either @Either + -- rcostrength @(->) @Either @Either :: RightCoModule (->) Either Either f => f (Either x a) (Either x b) -> f a b + rcostrength :: cat (f (x `t1` a) (x `t2` b)) (f a b) + +instance Costrong p => RightCoModule (->) (,) (,) (FromProfunctor p) where + rcostrength :: FromProfunctor p (x, a) (x, b) -> FromProfunctor p a b + rcostrength = unsecond + +instance Cochoice p => RightCoModule (->) Either Either (FromProfunctor p) where + rcostrength :: FromProfunctor p (Either x a) (Either x b) -> FromProfunctor p a b + rcostrength = unright + +instance Bifunctor p => RightCoModule (->) (,) (,) (FromBifunctor p) where + rcostrength :: FromBifunctor p (x, a) (x, b) -> FromBifunctor p a b + rcostrength = gbimap snd snd + +instance Bifunctor p => RightCoModule Op Either Either (FromBifunctor p) where + rcostrength :: Op (FromBifunctor p (Either x a) (Either x b)) (FromBifunctor p a b) + rcostrength = Op (gbimap Right Right) + +instance Bifunctor p => RightCoModule Op These These (FromBifunctor p) where + rcostrength :: Op (FromBifunctor p (These x a) (These x b)) (FromBifunctor p a b) + rcostrength = Op (gbimap That That) + +deriving via (FromProfunctor (Kleisli m)) instance MonadFix m => RightCoModule (->) (,) (,) (Kleisli m) +deriving via (FromProfunctor Tagged) instance RightCoModule (->) (,) (,) Tagged +deriving via (FromProfunctor (Coyoneda p)) instance Costrong p => RightCoModule (->) (,) (,) (Coyoneda p) +deriving via (FromProfunctor (Copastro p)) instance Cochoice p => RightCoModule (->) (,) (,) (Copastro p) +deriving via (FromProfunctor (Yoneda p)) instance Costrong p => RightCoModule (->) (,) (,) (Yoneda p) +deriving via (FromProfunctor (->)) instance RightCoModule (->) (,) (,) (->) +deriving via (FromProfunctor (Cokleisli f)) instance Functor f => RightCoModule (->) (,) (,) (Cokleisli f) +deriving via (FromProfunctor (Costar f)) instance Functor f => RightCoModule (->) (,) (,) (Costar f) +deriving via (FromProfunctor (WrappedArrow p)) instance ArrowLoop p => RightCoModule (->) (,) (,) (WrappedArrow p) +deriving via (FromProfunctor (Sum p q)) instance (Costrong p, Costrong q) => RightCoModule (->) (,) (,) (Sum p q) +deriving via (FromProfunctor (Product p q)) instance (Costrong p, Costrong q) => RightCoModule (->) (,) (,) (Product p q) +deriving via (FromProfunctor (Tannen f p)) instance (Functor f, Costrong p) => RightCoModule (->) (,) (,) (Tannen f p) +deriving via (FromProfunctor (Procompose p q)) instance (Corepresentable p, Corepresentable q) => RightCoModule (->) (,) (,) (Procompose p q) +deriving via (FromProfunctor (Cayley f p)) instance (Functor f, Costrong p) => RightCoModule (->) (,) (,) (Cayley f p) + +deriving via (FromProfunctor (CopastroSum p)) instance RightCoModule (->) Either Either (CopastroSum p) +deriving via (FromProfunctor (CotambaraSum p)) instance RightCoModule (->) Either Either (CotambaraSum p) +deriving via (FromProfunctor (Coyoneda p)) instance Cochoice p => RightCoModule (->) Either Either (Coyoneda p) +deriving via (FromProfunctor (Yoneda p)) instance Cochoice p => RightCoModule (->) Either Either (Yoneda p) +deriving via (FromProfunctor (->)) instance RightCoModule (->) Either Either (->) +deriving via (FromProfunctor (Forget r)) instance RightCoModule (->) Either Either (Forget r) +deriving via (FromProfunctor (Costar f)) instance Applicative f => RightCoModule (->) Either Either (Costar f) +deriving via (FromProfunctor (Star f)) instance Traversable f => RightCoModule (->) Either Either (Star f) +deriving via (FromProfunctor (Sum p q)) instance (Cochoice p, Cochoice q) => RightCoModule (->) Either Either (Sum p q) +deriving via (FromProfunctor (Product p q)) instance (Cochoice p, Cochoice q) => RightCoModule (->) Either Either (Product p q) +deriving via (FromProfunctor (Tannen f p)) instance (Functor f, Cochoice p) => RightCoModule (->) Either Either (Tannen f p) +deriving via (FromProfunctor (Cayley f p)) instance (Functor f, Cochoice p) => RightCoModule (->) Either Either (Cayley f p) + +deriving via (FromBifunctor Arg) instance RightCoModule (->) (,) (,) Arg +deriving via (FromBifunctor Const) instance RightCoModule (->) (,) (,) Const +deriving via (FromBifunctor Either) instance RightCoModule (->) (,) (,) Either +deriving via (FromBifunctor These) instance RightCoModule (->) (,) (,) These +deriving via (FromBifunctor (K1 i)) instance RightCoModule (->) (,) (,) (K1 i :: Type -> Type -> Type) +deriving via (FromBifunctor (,)) instance RightCoModule (->) (,) (,) (,) +deriving via (FromBifunctor ((,,) x1)) instance RightCoModule (->) (,) (,) ((,,) x1) +deriving via (FromBifunctor ((,,,) x1 x2)) instance RightCoModule (->) (,) (,) ((,,,) x1 x2) +deriving via (FromBifunctor ((,,,,) x1 x2 x3)) instance RightCoModule (->) (,) (,) ((,,,,) x1 x2 x3) +deriving via (FromBifunctor ((,,,,,) x1 x2 x3 x4)) instance RightCoModule (->) (,) (,) ((,,,,,) x1 x2 x3 x4) +deriving via (FromBifunctor ((,,,,,,) x1 x2 x3 x4 x5)) instance RightCoModule (->) (,) (,) ((,,,,,,) x1 x2 x3 x4 x5) + +deriving via (FromBifunctor Arg) instance RightCoModule Op Either Either Arg +deriving via (FromBifunctor Const) instance RightCoModule Op Either Either Const +deriving via (FromBifunctor Either) instance RightCoModule Op Either Either Either +deriving via (FromBifunctor These) instance RightCoModule Op Either Either These +deriving via (FromBifunctor (K1 i)) instance RightCoModule Op Either Either (K1 i :: Type -> Type -> Type) +deriving via (FromBifunctor (,)) instance RightCoModule Op Either Either (,) +deriving via (FromBifunctor ((,,) x1)) instance RightCoModule Op Either Either ((,,) x1) +deriving via (FromBifunctor ((,,,) x1 x2)) instance RightCoModule Op Either Either ((,,,) x1 x2) +deriving via (FromBifunctor ((,,,,) x1 x2 x3)) instance RightCoModule Op Either Either ((,,,,) x1 x2 x3) +deriving via (FromBifunctor ((,,,,,) x1 x2 x3 x4)) instance RightCoModule Op Either Either ((,,,,,) x1 x2 x3 x4) +deriving via (FromBifunctor ((,,,,,,) x1 x2 x3 x4 x5)) instance RightCoModule Op Either Either ((,,,,,,) x1 x2 x3 x4 x5) + +deriving via (FromBifunctor Arg) instance RightCoModule Op These These Arg +deriving via (FromBifunctor Const) instance RightCoModule Op These These Const +deriving via (FromBifunctor Either) instance RightCoModule Op These These Either +deriving via (FromBifunctor These) instance RightCoModule Op These These These +deriving via (FromBifunctor (K1 i)) instance RightCoModule Op These These (K1 i :: Type -> Type -> Type) +deriving via (FromBifunctor (,)) instance RightCoModule Op These These (,) +deriving via (FromBifunctor ((,,) x1)) instance RightCoModule Op These These ((,,) x1) +deriving via (FromBifunctor ((,,,) x1 x2)) instance RightCoModule Op These These ((,,,) x1 x2) +deriving via (FromBifunctor ((,,,,) x1 x2 x3)) instance RightCoModule Op These These ((,,,,) x1 x2 x3) +deriving via (FromBifunctor ((,,,,,) x1 x2 x3 x4)) instance RightCoModule Op These These ((,,,,,) x1 x2 x3 x4) +deriving via (FromBifunctor ((,,,,,,) x1 x2 x3 x4 x5)) instance RightCoModule Op These These ((,,,,,,) x1 x2 x3 x4 x5) + +-------------------------------------------------------------------------------- + +-- | A 'Profunctor' equipped with both a Tambara 'LeftCoModule' and +-- Tambara 'RightCoModule' is a 'CoBimodule'. +-- +-- === Laws +-- +-- @ +-- 'rcostrength' ≡ 'lcostrength' 'Control.Category..' 'Data.Profunctor.Types.dimap' 'Control.Category.Tensor.swap' 'Control.Category.Tensor.swap' +-- 'lcostrength' ≡ 'rcostrength' 'Control.Category..' 'Data.Profunctor.Types.dimap' 'Control.Category.Tensor.swap' 'Control.Category.Tensor.swap' +-- @ +class (LeftCoModule cat t1 t2 f, RightCoModule cat t1 t2 f) => CoBimodule cat t1 t2 f + +instance Costrong p => CoBimodule (->) (,) (,) (FromProfunctor p) +instance Cochoice p => CoBimodule (->) Either Either (FromProfunctor p) +instance Bifunctor p => CoBimodule (->) (,) (,) (FromBifunctor p) +instance Bifunctor p => CoBimodule Op Either Either (FromBifunctor p) +instance Bifunctor p => CoBimodule Op These These (FromBifunctor p) + +deriving via (FromProfunctor (Kleisli m)) instance MonadFix m => CoBimodule (->) (,) (,) (Kleisli m) +deriving via (FromProfunctor Tagged) instance CoBimodule (->) (,) (,) Tagged +deriving via (FromProfunctor (Coyoneda p)) instance Costrong p => CoBimodule (->) (,) (,) (Coyoneda p) +deriving via (FromProfunctor (Copastro p)) instance Cochoice p => CoBimodule (->) (,) (,) (Copastro p) +deriving via (FromProfunctor (Yoneda p)) instance Costrong p => CoBimodule (->) (,) (,) (Yoneda p) +deriving via (FromProfunctor (->)) instance CoBimodule (->) (,) (,) (->) +deriving via (FromProfunctor (Cokleisli f)) instance Functor f => CoBimodule (->) (,) (,) (Cokleisli f) +deriving via (FromProfunctor (Costar f)) instance Functor f => CoBimodule (->) (,) (,) (Costar f) +deriving via (FromProfunctor (WrappedArrow p)) instance ArrowLoop p => CoBimodule (->) (,) (,) (WrappedArrow p) +deriving via (FromProfunctor (Sum p q)) instance (Costrong p, Costrong q) => CoBimodule (->) (,) (,) (Sum p q) +deriving via (FromProfunctor (Product p q)) instance (Costrong p, Costrong q) => CoBimodule (->) (,) (,) (Product p q) +deriving via (FromProfunctor (Tannen f p)) instance (Functor f, Costrong p) => CoBimodule (->) (,) (,) (Tannen f p) +deriving via (FromProfunctor (Procompose p q)) instance (Corepresentable p, Corepresentable q) => CoBimodule (->) (,) (,) (Procompose p q) +deriving via (FromProfunctor (Cayley f p)) instance (Functor f, Costrong p) => CoBimodule (->) (,) (,) (Cayley f p) + +deriving via (FromProfunctor (CopastroSum p)) instance CoBimodule (->) Either Either (CopastroSum p) +deriving via (FromProfunctor (CotambaraSum p)) instance CoBimodule (->) Either Either (CotambaraSum p) +deriving via (FromProfunctor (Coyoneda p)) instance Cochoice p => CoBimodule (->) Either Either (Coyoneda p) +deriving via (FromProfunctor (Yoneda p)) instance Cochoice p => CoBimodule (->) Either Either (Yoneda p) +deriving via (FromProfunctor (->)) instance CoBimodule (->) Either Either (->) +deriving via (FromProfunctor (Forget r)) instance CoBimodule (->) Either Either (Forget r) +deriving via (FromProfunctor (Costar f)) instance Applicative f => CoBimodule (->) Either Either (Costar f) +deriving via (FromProfunctor (Star f)) instance Traversable f => CoBimodule (->) Either Either (Star f) +deriving via (FromProfunctor (Sum p q)) instance (Cochoice p, Cochoice q) => CoBimodule (->) Either Either (Sum p q) +deriving via (FromProfunctor (Product p q)) instance (Cochoice p, Cochoice q) => CoBimodule (->) Either Either (Product p q) +deriving via (FromProfunctor (Tannen f p)) instance (Functor f, Cochoice p) => CoBimodule (->) Either Either (Tannen f p) +deriving via (FromProfunctor (Cayley f p)) instance (Functor f, Cochoice p) => CoBimodule (->) Either Either (Cayley f p) + +deriving via (FromBifunctor Arg) instance CoBimodule (->) (,) (,) Arg +deriving via (FromBifunctor Const) instance CoBimodule (->) (,) (,) Const +deriving via (FromBifunctor Either) instance CoBimodule (->) (,) (,) Either +deriving via (FromBifunctor These) instance CoBimodule (->) (,) (,) These +deriving via (FromBifunctor (K1 i)) instance CoBimodule (->) (,) (,) (K1 i :: Type -> Type -> Type) +deriving via (FromBifunctor (,)) instance CoBimodule (->) (,) (,) (,) +deriving via (FromBifunctor ((,,) x1)) instance CoBimodule (->) (,) (,) ((,,) x1) +deriving via (FromBifunctor ((,,,) x1 x2)) instance CoBimodule (->) (,) (,) ((,,,) x1 x2) +deriving via (FromBifunctor ((,,,,) x1 x2 x3)) instance CoBimodule (->) (,) (,) ((,,,,) x1 x2 x3) +deriving via (FromBifunctor ((,,,,,) x1 x2 x3 x4)) instance CoBimodule (->) (,) (,) ((,,,,,) x1 x2 x3 x4) +deriving via (FromBifunctor ((,,,,,,) x1 x2 x3 x4 x5)) instance CoBimodule (->) (,) (,) ((,,,,,,) x1 x2 x3 x4 x5) + +deriving via (FromBifunctor Arg) instance CoBimodule Op Either Either Arg +deriving via (FromBifunctor Const) instance CoBimodule Op Either Either Const +deriving via (FromBifunctor Either) instance CoBimodule Op Either Either Either +deriving via (FromBifunctor These) instance CoBimodule Op Either Either These +deriving via (FromBifunctor (K1 i)) instance CoBimodule Op Either Either (K1 i :: Type -> Type -> Type) +deriving via (FromBifunctor (,)) instance CoBimodule Op Either Either (,) +deriving via (FromBifunctor ((,,) x1)) instance CoBimodule Op Either Either ((,,) x1) +deriving via (FromBifunctor ((,,,) x1 x2)) instance CoBimodule Op Either Either ((,,,) x1 x2) +deriving via (FromBifunctor ((,,,,) x1 x2 x3)) instance CoBimodule Op Either Either ((,,,,) x1 x2 x3) +deriving via (FromBifunctor ((,,,,,) x1 x2 x3 x4)) instance CoBimodule Op Either Either ((,,,,,) x1 x2 x3 x4) +deriving via (FromBifunctor ((,,,,,,) x1 x2 x3 x4 x5)) instance CoBimodule Op Either Either ((,,,,,,) x1 x2 x3 x4 x5) + +deriving via (FromBifunctor Arg) instance CoBimodule Op These These Arg +deriving via (FromBifunctor Const) instance CoBimodule Op These These Const +deriving via (FromBifunctor Either) instance CoBimodule Op These These Either +deriving via (FromBifunctor These) instance CoBimodule Op These These These +deriving via (FromBifunctor (K1 i)) instance CoBimodule Op These These (K1 i :: Type -> Type -> Type) +deriving via (FromBifunctor (,)) instance CoBimodule Op These These (,) +deriving via (FromBifunctor ((,,) x1)) instance CoBimodule Op These These ((,,) x1) +deriving via (FromBifunctor ((,,,) x1 x2)) instance CoBimodule Op These These ((,,,) x1 x2) +deriving via (FromBifunctor ((,,,,) x1 x2 x3)) instance CoBimodule Op These These ((,,,,) x1 x2 x3) +deriving via (FromBifunctor ((,,,,,) x1 x2 x3 x4)) instance CoBimodule Op These These ((,,,,,) x1 x2 x3 x4) +deriving via (FromBifunctor ((,,,,,,) x1 x2 x3 x4 x5)) instance CoBimodule Op These These ((,,,,,,) x1 x2 x3 x4 x5) diff --git a/src/Data/Bifunctor/Monoidal.hs b/src/Data/Bifunctor/Monoidal.hs --- a/src/Data/Bifunctor/Monoidal.hs +++ b/src/Data/Bifunctor/Monoidal.hs @@ -1,18 +1,71 @@ -module Data.Bifunctor.Monoidal where +module Data.Bifunctor.Monoidal + ( -- * Semigroupal + Semigroupal (..), -import Prelude hiding ((.), id) -import Control.Applicative -import Control.Category -import Control.Category.Tensor -import Data.Biapplicative -import Data.Bifunctor.Clown -import Data.Bifunctor.Joker -import Data.Profunctor -import Data.Semigroupoid -import Data.These -import Data.Void + -- * Unital + Unital (..), -class (Associative t1 cat, Associative t2 cat, Associative to cat) => Semigroupal cat t1 t2 to f where + -- * Monoidal + Monoidal, + ) +where + +-------------------------------------------------------------------------------- + +import Control.Applicative (Alternative (..), Applicative (..), pure, (<$>)) +import Control.Category (Category (..)) +import Control.Category.Cartesian (Cocartesian (..), Semicartesian (..)) +import Control.Category.Tensor (Associative, Iso (..), Tensor (..)) +import Control.Monad (Functor(..), Monad) +import Data.Biapplicative (Biapplicative (..), Bifunctor (..)) +import Data.Bifunctor.Clown (Clown) +import Data.Bifunctor.Joker (Joker (..)) +import Data.Either (Either, either) +import Data.Function (const, ($)) +import Data.Profunctor (Forget (..), Profunctor (..), Star (..), Strong (..)) +import Data.Semigroupoid (Semigroupoid (..)) +import Data.These (These (..)) +import Data.Tuple (fst, snd, uncurry) +import Data.Void (Void, absurd) +import Prelude (Either (..)) + +-------------------------------------------------------------------------------- + +-- | Given monoidal categories \((\mathcal{C}, \otimes, I_{\mathcal{C}})\) and \((\mathcal{D}, \bullet, I_{\mathcal{D}})\). +-- A bifunctor \(F : \mathcal{C_1} \times \mathcal{C_2} \to \mathcal{D}\) is 'Semigroupal' if it supports a +-- natural transformation \(\phi_{AB,CD} : F\ A\ B \bullet F\ C\ D \to F\ (A \otimes C)\ (B \otimes D)\), which we call 'combine'. +-- +-- === Laws +-- +-- __Associativity:__ +-- +-- \[ +-- \require{AMScd} +-- \begin{CD} +-- (F A B \bullet F C D) \bullet F X Y @>>{\alpha_{\mathcal{D}}}> F A B \bullet (F C D \bullet F X Y) \\ +-- @VV{\phi_{AB,CD} \bullet 1}V @VV{1 \bullet \phi_{CD,FY}}V \\ +-- F (A \otimes C) (B \otimes D) \bullet F X Y @. F A B \bullet (F (C \otimes X) (D \otimes Y) \\ +-- @VV{\phi_{(A \otimes C)(B \otimes D),XY}}V @VV{\phi_{AB,(C \otimes X)(D \otimes Y)}}V \\ +-- F ((A \otimes C) \otimes X) ((B \otimes D) \otimes Y) @>>{F \alpha_{\mathcal{C_1}}} \alpha_{\mathcal{C_2}}> F (A \otimes (C \otimes X)) (B \otimes (D \otimes Y)) \\ +-- \end{CD} +-- \] +-- +-- @ +-- 'combine' 'Control.Category..' 'Control.Category.Tensor.grmap' 'combine' 'Control.Category..' 'bwd' 'Control.Category.Tensor.assoc' ≡ 'fmap' ('bwd' 'Control.Category.Tensor.assoc') 'Control.Category..' 'combine' 'Control.Category..' 'Control.Category.Tensor.glmap' 'combine' +-- @ +class (Associative cat t1, Associative cat t2, Associative cat to) => Semigroupal cat t1 t2 to f where + -- | A natural transformation \(\phi_{AB,CD} : F\ A\ B \bullet F\ C\ D \to F\ (A \otimes C)\ (B \otimes D)\). + -- + -- ==== __Examples__ + -- + -- >>> :t combine @(->) @(,) @(,) @(,) @(,) + -- combine @(->) @(,) @(,) @(,) @(,) :: ((x, y), (x', y')) -> ((x, x'), (y, y')) + -- + -- >>> combine @(->) @(,) @(,) @(,) @(,) ((True, "Hello"), ((), "World")) + -- ((True,()),("Hello","World")) + -- + -- >>> combine @(->) @(,) @(,) @(,) @(->) (show, (>10)) (True, 11) + -- ("True",True) combine :: cat (to (f x y) (f x' y')) (f (t1 x x') (t2 y y')) instance Profunctor p => Semigroupal (->) (,) Either Either p where @@ -40,22 +93,22 @@ instance Semigroupal (->) Either (,) (,) Either where combine :: (Either x y, Either x' y') -> Either (Either x x') (y, y') combine = \case - (Left x, Left _) -> Left $ Left x - (Left x, Right _) -> Left $ Left x - (Right _, Left x') -> Left $ Right x' + (Left x, Left _) -> Left $ Left x + (Left x, Right _) -> Left $ Left x + (Right _, Left x') -> Left $ Right x' (Right y, Right y') -> Right (y, y') instance Semigroupal (->) These (,) (,) Either where combine :: (Either x y, Either x' y') -> Either (These x x') (y, y') combine = \case - (Left x, Left x') -> Left $ These x x' - (Left x, Right _) -> Left $ This x - (Right _, Left x') -> Left $ That x' + (Left x, Left x') -> Left $ These x x' + (Left x, Right _) -> Left $ This x + (Right _, Left x') -> Left $ That x' (Right y, Right y') -> Right (y, y') instance Semigroupal (->) (,) (,) (,) (->) where combine :: (x -> y, x' -> y') -> (x, x') -> (y, y') - combine fs = uncurry bimap fs + combine = uncurry bimap instance Semigroupal (->) Either Either (,) (->) where combine :: (x -> y, x' -> y') -> Either x x' -> Either y y' @@ -92,7 +145,7 @@ instance Alternative f => Semigroupal (->) Either Either Either (Star f) where combine :: Either (Star f x y) (Star f x' y') -> Star f (Either x x') (Either y y') combine = \case - Left (Star fxy) -> Star $ either (fmap Left . fxy) (const empty) + Left (Star fxy) -> Star $ either (fmap Left . fxy) (const empty) Right (Star fxy') -> Star $ either (const empty) (fmap Right . fxy') instance Alternative f => Semigroupal (->) (,) Either (,) (Star f) where @@ -110,14 +163,32 @@ instance Alternative f => Semigroupal (->) Either Either Either (Forget (f r)) where combine :: Either (Forget (f r) x y) (Forget (f r) x' y') -> Forget (f r) (Either x x') (Either y y') combine = \case - Left (Forget f) -> Forget $ either f (const empty) + Left (Forget f) -> Forget $ either f (const empty) Right (Forget g) -> Forget $ either (const empty) g instance Alternative f => Semigroupal (->) (,) Either (,) (Forget (f r)) where combine :: (Forget (f r) x y, Forget (f r) x' y') -> Forget (f r) (x, x') (Either y y') combine (Forget f, Forget g) = Forget $ \(x, x') -> f x <|> g x' +-------------------------------------------------------------------------------- + +-- | Given monoidal categories \((\mathcal{C}, \otimes, I_{\mathcal{C}})\) and \((\mathcal{D}, \bullet, I_{\mathcal{D}})\). +-- A bifunctor \(F : \mathcal{C_1} \times \mathcal{C_2} \to \mathcal{D}\) is 'Unital' if it supports a morphism +-- \(\phi : I_{\mathcal{D}} \to F\ I_{\mathcal{C_1}}\ I_{\mathcal{C_2}}\), which we call 'introduce'. class Unital cat i1 i2 io f where + -- | @introduce@ maps from the identity in \(\mathcal{C_1} \times \mathcal{C_2}\) to the + -- identity in \(\mathcal{D}\). + -- + -- ==== __Examples__ + -- + -- >>> introduce @(->) @() @() @() @(,) () + -- ((),()) + -- + -- >>> :t introduce @(->) @Void @() @() @Either + -- introduce @(->) @Void @() @() @Either :: () -> Either Void () + -- + -- >>> introduce @(->) @Void @() @() @Either () + -- Right () introduce :: cat io (f i1 i2) instance (Profunctor p, Category p) => Unital (->) () () () (StrongCategory p) where @@ -126,15 +197,15 @@ instance Unital (->) () () () (,) where introduce :: () -> ((), ()) - introduce = dup + introduce = split instance Unital (->) Void Void Void (,) where introduce :: Void -> (Void, Void) - introduce = absurd + introduce = spawn instance Unital (->) Void Void Void Either where introduce :: Void -> Either Void Void - introduce = bwd runit + introduce = bwd unitr instance Unital (->) Void () () Either where introduce :: () -> Either Void () @@ -180,9 +251,48 @@ introduce :: () -> Star f () Void introduce () = Star $ const empty -class (Tensor t1 i1 cat - , Tensor t2 i2 cat - , Tensor to io cat +-------------------------------------------------------------------------------- +-- Monoidal + +-- | Given monoidal categories \((\mathcal{C}, \otimes, I_{\mathcal{C}})\) and \((\mathcal{D}, \bullet, I_{\mathcal{D}})\). +-- A bifunctor \(F : \mathcal{C_1} \times \mathcal{C_2} \to \mathcal{D}\) is 'Monoidal' if it maps between \(\mathcal{C_1} \times \mathcal{C_2}\) +-- and \(\mathcal{D}\) while preserving their monoidal structure. Eg., a homomorphism of monoidal categories. +-- +-- See for more details. +-- +-- === Laws +-- +-- __Right Unitality:__ +-- +-- \[ +-- \require{AMScd} +-- \begin{CD} +-- F A B \bullet I_{\mathcal{D}} @>{1 \bullet \phi}>> F A B \bullet F I_{\mathcal{C_{1}}} I_{\mathcal{C_{2}}}\\ +-- @VV{\rho_{\mathcal{D}}}V @VV{\phi AB,I_{\mathcal{C_{1}}}I_{\mathcal{C_{2}}}}V \\ +-- F A B @<<{F \rho_{\mathcal{C_{1}}} \rho_{\mathcal{C_{2}}}}< F (A \otimes I_{\mathcal{C_{1}}}) (B \otimes I_{\mathcal{C_{2}}}) +-- \end{CD} +-- \] +-- +-- @ +-- 'combine' 'Control.Category..' 'Control.Category.Tensor.grmap' 'introduce' ≡ 'bwd' 'unitr' 'Control.Category..' 'fwd' 'unitr' +-- @ +-- +-- __ Left Unitality__: +-- +-- \[ +-- \begin{CD} +-- I_{\mathcal{D}} \bullet F A B @>{\phi \bullet 1}>> F I_{\mathcal{C_{1}}} I_{\mathcal{C_{2}}} \bullet F A B\\ +-- @VV{\lambda_{\mathcal{D}}}V @VV{I_{\mathcal{C_{1}}}I_{\mathcal{C_{2}}},\phi AB}V \\ +-- F A B @<<{F \lambda_{\mathcal{C_{1}}} \lambda_{\mathcal{C_{2}}}}< F (I_{\mathcal{C_{1}}} \otimes A) (I_{\mathcal{C_{2}}} \otimes B) +-- \end{CD} +-- \] +-- +-- @ +-- 'combine' 'Control.Category..' 'Control.Category.Tensor.glmap' 'introduce' ≡ 'fmap' ('bwd' 'unitl') 'Control.Category..' 'fwd' 'unitl' +-- @ +class ( Tensor cat t1 i1 + , Tensor cat t2 i2 + , Tensor cat to io , Semigroupal cat t1 t2 to f , Unital cat i1 i2 io f ) => Monoidal cat t1 i1 t2 i2 to io f diff --git a/src/Data/Bifunctor/Monoidal/Specialized.hs b/src/Data/Bifunctor/Monoidal/Specialized.hs --- a/src/Data/Bifunctor/Monoidal/Specialized.hs +++ b/src/Data/Bifunctor/Monoidal/Specialized.hs @@ -3,54 +3,78 @@ import Prelude hiding ((&&), (||)) -import Control.Category.Tensor +import Control.Category.Cartesian +import Control.Category.Tensor () import Data.Bifunctor.Monoidal import Data.Functor.Contravariant import Data.Profunctor import Data.Void +-- | Split the input between the two argument arrows and multiply their outputs. mux :: Semigroupal (->) (,) (,) (,) p => p a b -> p c d -> p (a, c) (b, d) mux = curry combine -infixr 5 && - -(&&) :: Semigroupal (->) (,) (,) (,) p => p a b -> p c d -> p (a, c) (b, d) -(&&) = mux +infixr 3 *** -zip :: (Profunctor p, Semigroupal (->) (,) (,) (,) p) => p x a -> p x b -> p x (a, b) -zip pxa pxb = lmap dup $ pxa && pxb +-- | Infix operator for 'mux'. +(***) :: Semigroupal (->) (,) (,) (,) p => p a b -> p c d -> p (a, c) (b, d) +(***) = mux +-- | Split the input between the two argument arrows and sum their outputs. demux :: Semigroupal (->) Either Either (,) p => p a b -> p c d -> p (Either a c) (Either b d) demux = curry combine -infixr 4 || +infixr 2 +++ -(||) :: Semigroupal (->) Either Either (,) p => p a b -> p c d -> p (Either a c) (Either b d) -(||) = demux +-- | Infix operator for 'demux'. +(+++) :: Semigroupal (->) Either Either (,) p => p a b -> p c d -> p (Either a c) (Either b d) +(+++) = demux +-- | Send the whole input to the two argument arrows and multiply their outputs. +fanout :: (Profunctor p, Semigroupal (->) (,) (,) (,) p) => p x a -> p x b -> p x (a, b) +fanout pxa pxb = lmap split' $ pxa *** pxb +infixr 3 &&& + +-- | Infix operator for 'fanout'. +(&&&) :: (Profunctor p, Semigroupal (->) (,) (,) (,) p) => p x a -> p x b -> p x (a, b) +(&&&) = fanout + +-- | Split the input between the two argument arrows and merge their outputs. fanin :: (Profunctor p, Semigroupal (->) Either Either (,) p) => p a x -> p b x -> p (Either a b) x -fanin pax pbx = rmap merge $ pax || pbx +fanin pax pbx = rmap merge' $ pax +++ pbx +infixr 2 ||| + +-- | Infix operator for 'fanin'. +(|||) :: (Profunctor p, Semigroupal (->) Either Either (,) p) => p a x -> p b x -> p (Either a b) x +(|||) = fanin + +-- | Split the input between the two argument arrows and and sum their outputs. switch :: Semigroupal (->) (,) Either (,) p => p a b -> p c d -> p (a, c) (Either b d) switch = curry combine infixr 5 &| +-- | Infix operator for 'switch'. (&|) :: Semigroupal (->) (,) Either (,) p => p a b -> p c d -> p (a, c) (Either b d) (&|) = switch +-- | Send the whole input to the two argument arrows and sum their outputs. union :: Profunctor p => Semigroupal (->) (,) Either (,) p => p x a -> p x b -> p x (Either a b) -union pxa pxb = lmap dup $ pxa &| pxb +union pxa pxb = lmap split' $ pxa &| pxb +-- | Split the input between the two argument arrows then merge their outputs. divide :: (Profunctor p, Semigroupal (->) (,) Either (,) p) => p a x -> p b x -> p (a, b) x -divide pxa pxb = rmap merge $ pxa &| pxb +divide pxa pxb = rmap merge' $ pxa &| pxb +-- | Split the input between the two argument arrows then multiply their outputs. splice :: Semigroupal (->) Either (,) (,) p => p a b -> p c d -> p (Either a c) (b, d) splice = curry combine infix 5 |& +-- | Infix operator for 'splice'. (|&) :: Semigroupal (->) Either (,) (,) p => p a b -> p c d -> p (Either a c) (b, d) (|&) = splice @@ -58,13 +82,13 @@ diverge = combine contramapMaybe :: Profunctor p => Semigroupal (->) Either Either Either p => (a -> Maybe b) -> p b x -> p a x -contramapMaybe f = dimap (maybe (Right ()) Left . f) merge . ultraleft +contramapMaybe f = dimap (maybe (Right ()) Left . f) merge' . ultraleft zig :: (Profunctor p, Semigroupal (->) (,) t Either p) => Either (p x a) (p x b) -> p x (t a b) -zig = lmap dup . combine +zig = lmap split' . combine zag :: (Profunctor p, Semigroupal (->) t Either Either p) => Either (p a x) (p b x) -> p (t a b) x -zag = rmap merge . combine +zag = rmap merge' . combine ultrafirst :: (Profunctor p, Semigroupal (->) (,) (,) Either p) => p a b -> p (a, x) (b, y) ultrafirst = zag . Left . zig . Left @@ -82,22 +106,22 @@ comux = getOp combine undivide :: forall p x a b. Profunctor p => Semigroupal Op (,) (,) (,) p => p (a, b) x -> (p a x, p b x) -undivide = comux . rmap dup +undivide = comux . rmap split' codemux :: forall p a b c d. Semigroupal Op Either Either (,) p => p (Either a c) (Either b d) -> (p a b, p c d) codemux = getOp combine partition :: forall p x a b. Profunctor p => Semigroupal Op Either Either (,) p => p x (Either a b) -> (p x a, p x b) -partition = codemux . lmap merge +partition = codemux . lmap merge' coswitch :: forall p a b c d. Semigroupal Op Either (,) (,) p => p (Either a c) (b, d) -> (p a b, p c d) coswitch = getOp combine unfanin :: forall p x a b. Profunctor p => Semigroupal Op Either (,) (,) p => p (Either a b) x -> (p a x, p b x) -unfanin = coswitch . rmap dup +unfanin = coswitch . rmap split' unzip :: forall p x a b. Profunctor p => Semigroupal Op Either (,) (,) p => p x (a, b) -> (p x a, p x b) -unzip = coswitch . lmap merge +unzip = coswitch . lmap merge' cosplice :: forall p a b c d. Semigroupal Op (,) Either (,) p => p (a, c) (Either b d) -> (p a b, p c d) cosplice = getOp combine @@ -106,7 +130,7 @@ terminal = lmap (const ()) $ introduce () ppure :: forall p a. Profunctor p => Unital (->) () () () p => Strong p => p a a -ppure = dimap ((),) snd $ first' (introduce () :: p () ()) +ppure = dimap ((),) projr $ first' (introduce () :: p () ()) initial :: forall p a. Profunctor p => Unital (->) Void Void () p => p Void a initial = rmap absurd $ introduce () @@ -116,3 +140,9 @@ mono :: forall p. Unital (->) Void () () p => p Void () mono = introduce () + +split' :: a -> (a, a) +split' = split @(->) @(,) + +merge' :: Either a a -> a +merge' = merge @(->) @Either diff --git a/src/Data/Functor/Invariant.hs b/src/Data/Functor/Invariant.hs --- a/src/Data/Functor/Invariant.hs +++ b/src/Data/Functor/Invariant.hs @@ -1,22 +1,57 @@ -module Data.Functor.Invariant where +{-# LANGUAGE DefaultSignatures #-} +module Data.Functor.Invariant + ( -- * Invariant + Invariant (..), + invIso, + ) +where -import Prelude +-------------------------------------------------------------------------------- + import Control.Applicative (ZipList) -import Control.Category.Tensor -import Data.Functor.Contravariant -import Data.Functor.Compose -import Data.Functor.Identity -import Data.Functor.Sum -import Data.Functor.Product +import Control.Category.Tensor (Iso (Iso)) +import Data.Functor.Compose (Compose (..)) +import Data.Functor.Contravariant (Contravariant (..)) +import Data.Functor.Identity (Identity (Identity)) +import Data.Functor.Product (Product) +import Data.Functor.Sum (Sum) import Data.List.NonEmpty (NonEmpty) +import Prelude +-------------------------------------------------------------------------------- + +-- | A functor is 'Invariant' if it is parametric in its type +-- parameter @a@. +-- +-- === Laws +-- +-- @ +-- 'invmap' 'id' 'id' ≡ 'id' +-- 'invmap' @f2@ @f2'@ 'Control.Category..' 'invmap' @f1@ @f1'@ ≡ 'invmap' (@f2@ 'Control.Category..' @f1@) (@f1'@ 'Control.Category..' @f2'@) +-- @ class Invariant f where + -- | Given two isomorphic functions @f@ and @g@, map over the + -- invariant parameter @a@. + -- + -- ==== __Examples__ + -- + -- >>> :t invmap @Identity (read @Bool) show + -- invmap @Identity (read @Bool) show :: Identity String -> Identity Bool + -- + -- >>> invmap @Identity (read @Bool) show (Identity "True") + -- Identity True invmap :: (a -> a') -> (a' -> a) -> f a -> f a' + default invmap :: Functor f => (a -> a') -> (a' -> a) -> f a -> f a' + invmap = invmapFunctor invIso :: Invariant f => Iso (->) a a' -> Iso (->) (f a) (f a') invIso (Iso f g) = Iso (invmap f g) (invmap g f) newtype FromFunctor f a = FromFunctor { runBi :: f a } + +-- | Every 'Functor' is also an 'Invariant' functor. +invmapFunctor :: Functor f => (a -> b) -> (b -> a) -> f a -> f b +invmapFunctor = flip $ const fmap instance Functor f => Invariant (FromFunctor f) where invmap :: (a -> a') -> (a' -> a) -> FromFunctor f a -> FromFunctor f a' diff --git a/src/Data/Functor/Module.hs b/src/Data/Functor/Module.hs --- a/src/Data/Functor/Module.hs +++ b/src/Data/Functor/Module.hs @@ -1,9 +1,362 @@ -module Data.Functor.Module where +module Data.Functor.Module + ( -- * LeftModule + LeftModule (..), + -- * RightModule + RightModule (..), + + -- * Bimodule + Bimodule, + ) +where + +-------------------------------------------------------------------------------- + +import Control.Applicative (ZipList) +import Data.Either (Either (..)) +import Data.Functor (Functor (..)) +import Data.Functor.Compose (Compose) +import Data.Functor.Const (Const) +import Data.Functor.Contravariant (Comparison, Contravariant (..), Equivalence, Op (Op), Predicate) +import Data.Functor.Identity (Identity) +import Data.Functor.Product (Product) +import Data.Functor.Sum (Sum) +import Data.List.NonEmpty (NonEmpty) +import Data.Maybe (Maybe) +import Data.Monoid (Alt) +import Data.Proxy (Proxy) +import Data.These (These (..)) +import Data.Tuple (fst, snd) +import GHC.Generics (K1, M1, Rec1, U1, V1, type (:*:), type (:+:), type (:.:)) +import Prelude (IO) + +-------------------------------------------------------------------------------- + +newtype FromContra f a = FromContra (f a) + deriving newtype (Contravariant) + +newtype FromFunctor f a = FromFunctor (f a) + deriving newtype (Functor) + +-------------------------------------------------------------------------------- + class LeftModule cat t1 f where - lstrength :: f a `cat` f (t1 a x) + -- | ==== __Examples__ + -- + -- >>> :t lstrength @(->) @(,) @Predicate (Predicate @Int (> 10)) + -- lstrength @(->) @(,) @Predicate (Predicate @Int (> 10)) :: Predicate (Int, x) + -- + -- >>> :t lstrength @(->) @Either @[] + -- lstrength @(->) @Either @[] :: a -> [Either a x] + -- + -- >>> lstrength @(->) @Either @[] [True, False] + -- [Left True,Left False] + lstrength :: cat (f a) (f (t1 a x)) +instance Contravariant f => LeftModule (->) (,) (FromContra f) where + lstrength :: FromContra f a -> FromContra f (a, x) + lstrength = contramap fst + +instance Contravariant f => LeftModule Op Either (FromContra f) where + lstrength = Op (contramap Left) + +instance Functor f => LeftModule (->) Either (FromFunctor f) where + lstrength :: FromFunctor f a -> FromFunctor f (Either a x) + lstrength = fmap Left + +instance Functor f => LeftModule (->) These (FromFunctor f) where + lstrength :: FromFunctor f a -> FromFunctor f (These a x) + lstrength = fmap This + +instance Functor f => LeftModule Op (,) (FromFunctor f) where + lstrength = Op (fmap fst) + +deriving via (FromContra Comparison) instance LeftModule (->) (,) Comparison +deriving via (FromContra Equivalence) instance LeftModule (->) (,) Equivalence +deriving via (FromContra Predicate) instance LeftModule (->) (,) Predicate +deriving via (FromContra (Op a)) instance LeftModule (->) (,) (Op a) +deriving via (FromContra Proxy) instance LeftModule (->) (,) Proxy +deriving via (FromContra U1) instance LeftModule (->) (,) U1 +deriving via (FromContra V1) instance LeftModule (->) (,) V1 +deriving via (FromContra (Const a)) instance LeftModule (->) (,) (Const a) +deriving via (FromContra (Alt f)) instance Contravariant f => LeftModule (->) (,) (Alt f) +deriving via (FromContra (Rec1 f)) instance Contravariant f => LeftModule (->) (,) (Rec1 f) +deriving via (FromContra (Product f g)) instance (Contravariant f, Contravariant g) => LeftModule (->) (,) (Product f g) +deriving via (FromContra (Sum f g)) instance (Contravariant f, Contravariant g) => LeftModule (->) (,) (Sum f g) +deriving via (FromContra (f :+: g)) instance (Contravariant f, Contravariant g) => LeftModule (->) (,) (f :+: g) +deriving via (FromContra (f :*: g)) instance (Contravariant f, Contravariant g) => LeftModule (->) (,) (f :*: g) +deriving via (FromContra (K1 i c)) instance LeftModule (->) (,) (K1 i c) +deriving via (FromContra (Compose f g)) instance (Functor f, Contravariant g) => LeftModule (->) (,) (Compose f g) +deriving via (FromContra (f :.: g)) instance (Functor f, Contravariant g) => LeftModule (->) (,) (f :.: g) +deriving via (FromContra (M1 i c f)) instance Contravariant f => LeftModule (->) (,) (M1 i c f) + +deriving via (FromContra Comparison) instance LeftModule Op Either Comparison +deriving via (FromContra Equivalence) instance LeftModule Op Either Equivalence +deriving via (FromContra Predicate) instance LeftModule Op Either Predicate +deriving via (FromContra (Op a)) instance LeftModule Op Either (Op a) +deriving via (FromContra Proxy) instance LeftModule Op Either Proxy +deriving via (FromContra U1) instance LeftModule Op Either U1 +deriving via (FromContra V1) instance LeftModule Op Either V1 +deriving via (FromContra (Const a)) instance LeftModule Op Either (Const a) +deriving via (FromContra (Alt f)) instance Contravariant f => LeftModule Op Either (Alt f) +deriving via (FromContra (Rec1 f)) instance Contravariant f => LeftModule Op Either (Rec1 f) +deriving via (FromContra (Product f g)) instance (Contravariant f, Contravariant g) => LeftModule Op Either (Product f g) +deriving via (FromContra (Sum f g)) instance (Contravariant f, Contravariant g) => LeftModule Op Either (Sum f g) +deriving via (FromContra (f :+: g)) instance (Contravariant f, Contravariant g) => LeftModule Op Either (f :+: g) +deriving via (FromContra (f :*: g)) instance (Contravariant f, Contravariant g) => LeftModule Op Either (f :*: g) +deriving via (FromContra (K1 i c)) instance LeftModule Op Either (K1 i c) +deriving via (FromContra (Compose f g)) instance (Functor f, Contravariant g) => LeftModule Op Either (Compose f g) +deriving via (FromContra (f :.: g)) instance (Functor f, Contravariant g) => LeftModule Op Either (f :.: g) +deriving via (FromContra (M1 i c f)) instance Contravariant f => LeftModule Op Either (M1 i c f) + +deriving via FromFunctor Identity instance LeftModule (->) Either Identity +deriving via FromFunctor (Compose f g) instance (Functor f, Functor g) => LeftModule (->) Either (Compose f g) +deriving via FromFunctor [] instance LeftModule (->) Either [] +deriving via FromFunctor ZipList instance LeftModule (->) Either ZipList +deriving via FromFunctor NonEmpty instance LeftModule (->) Either NonEmpty +deriving via FromFunctor Maybe instance LeftModule (->) Either Maybe +deriving via FromFunctor (Either e) instance LeftModule (->) Either (Either e) +deriving via FromFunctor (These a) instance LeftModule (->) Either (These a) +deriving via FromFunctor IO instance LeftModule (->) Either IO +deriving via FromFunctor (Sum f g) instance (Functor f, Functor g) => LeftModule (->) Either (Sum f g) +deriving via FromFunctor (Product f g) instance (Functor f, Functor g) => LeftModule (->) Either (Product f g) +deriving via (FromFunctor ((,) x1)) instance LeftModule (->) Either ((,) x1) +deriving via (FromFunctor ((,,) x1 x2)) instance LeftModule (->) Either ((,,) x1 x2) +deriving via (FromFunctor ((,,,) x1 x2 x3)) instance LeftModule (->) Either ((,,,) x1 x2 x3) + +deriving via FromFunctor Identity instance LeftModule (->) These Identity +deriving via FromFunctor (Compose f g) instance (Functor f, Functor g) => LeftModule (->) These (Compose f g) +deriving via FromFunctor [] instance LeftModule (->) These [] +deriving via FromFunctor ZipList instance LeftModule (->) These ZipList +deriving via FromFunctor NonEmpty instance LeftModule (->) These NonEmpty +deriving via FromFunctor Maybe instance LeftModule (->) These Maybe +deriving via FromFunctor (Either e) instance LeftModule (->) These (Either e) +deriving via FromFunctor (These a) instance LeftModule (->) These (These a) +deriving via FromFunctor IO instance LeftModule (->) These IO +deriving via FromFunctor (Sum f g) instance (Functor f, Functor g) => LeftModule (->) These (Sum f g) +deriving via FromFunctor (Product f g) instance (Functor f, Functor g) => LeftModule (->) These (Product f g) +deriving via (FromFunctor ((,) x1)) instance LeftModule (->) These ((,) x1) +deriving via (FromFunctor ((,,) x1 x2)) instance LeftModule (->) These ((,,) x1 x2) +deriving via (FromFunctor ((,,,) x1 x2 x3)) instance LeftModule (->) These ((,,,) x1 x2 x3) + +deriving via FromFunctor Identity instance LeftModule Op (,) Identity +deriving via FromFunctor (Compose f g) instance (Functor f, Functor g) => LeftModule Op (,) (Compose f g) +deriving via FromFunctor [] instance LeftModule Op (,) [] +deriving via FromFunctor ZipList instance LeftModule Op (,) ZipList +deriving via FromFunctor NonEmpty instance LeftModule Op (,) NonEmpty +deriving via FromFunctor Maybe instance LeftModule Op (,) Maybe +deriving via FromFunctor (Either e) instance LeftModule Op (,) (Either e) +deriving via FromFunctor IO instance LeftModule Op (,) IO +deriving via FromFunctor (Sum f g) instance (Functor f, Functor g) => LeftModule Op (,) (Sum f g) +deriving via FromFunctor (Product f g) instance (Functor f, Functor g) => LeftModule Op (,) (Product f g) +deriving via (FromFunctor ((,) x1)) instance LeftModule Op (,) ((,) x1) +deriving via (FromFunctor ((,,) x1 x2)) instance LeftModule Op (,) ((,,) x1 x2) +deriving via (FromFunctor ((,,,) x1 x2 x3)) instance LeftModule Op (,) ((,,,) x1 x2 x3) + +-------------------------------------------------------------------------------- + class RightModule cat t1 f where - rstrength :: f a `cat` f (t1 x a) + -- | ==== __Examples__ + -- + -- >>> :t rstrength @(->) @(,) @Predicate (Predicate @Int (> 10)) + -- rstrength @(->) @(,) @Predicate (Predicate @Int (> 10)) :: Predicate (x, Int) + -- + -- >>> :t rstrength @(->) @Either @[] + -- rstrength @(->) @Either @[] :: [a] -> [Either x a] + -- >>> rstrength @(->) @Either @[] [True, False] + -- [Right True,Right False] + rstrength :: cat (f a) (f (t1 x a)) +instance Contravariant f => RightModule (->) (,) (FromContra f) where + rstrength :: FromContra f a -> FromContra f (x, a) + rstrength = contramap snd + +instance Contravariant f => RightModule Op Either (FromContra f) where + rstrength :: Op (FromContra f a) (FromContra f (Either x a)) + rstrength = Op (contramap Right) + +instance Functor f => RightModule (->) Either (FromFunctor f) where + rstrength :: FromFunctor f a -> FromFunctor f (Either x a) + rstrength = fmap Right + +instance Functor f => RightModule (->) These (FromFunctor f) where + rstrength :: FromFunctor f a -> FromFunctor f (These x a) + rstrength = fmap That + +instance Functor f => RightModule Op (,) (FromFunctor f) where + rstrength :: Op (FromFunctor f a) (FromFunctor f (x, a)) + rstrength = Op (fmap snd) + +deriving via (FromContra Comparison) instance RightModule (->) (,) Comparison +deriving via (FromContra Equivalence) instance RightModule (->) (,) Equivalence +deriving via (FromContra Predicate) instance RightModule (->) (,) Predicate +deriving via (FromContra (Op a)) instance RightModule (->) (,) (Op a) +deriving via (FromContra Proxy) instance RightModule (->) (,) Proxy +deriving via (FromContra U1) instance RightModule (->) (,) U1 +deriving via (FromContra V1) instance RightModule (->) (,) V1 +deriving via (FromContra (Const a)) instance RightModule (->) (,) (Const a) +deriving via (FromContra (Alt f)) instance Contravariant f => RightModule (->) (,) (Alt f) +deriving via (FromContra (Rec1 f)) instance Contravariant f => RightModule (->) (,) (Rec1 f) +deriving via (FromContra (Product f g)) instance (Contravariant f, Contravariant g) => RightModule (->) (,) (Product f g) +deriving via (FromContra (Sum f g)) instance (Contravariant f, Contravariant g) => RightModule (->) (,) (Sum f g) +deriving via (FromContra (f :+: g)) instance (Contravariant f, Contravariant g) => RightModule (->) (,) (f :+: g) +deriving via (FromContra (f :*: g)) instance (Contravariant f, Contravariant g) => RightModule (->) (,) (f :*: g) +deriving via (FromContra (K1 i c)) instance RightModule (->) (,) (K1 i c) +deriving via (FromContra (Compose f g)) instance (Functor f, Contravariant g) => RightModule (->) (,) (Compose f g) +deriving via (FromContra (f :.: g)) instance (Functor f, Contravariant g) => RightModule (->) (,) (f :.: g) +deriving via (FromContra (M1 i c f)) instance Contravariant f => RightModule (->) (,) (M1 i c f) + +deriving via (FromContra Comparison) instance RightModule Op Either Comparison +deriving via (FromContra Equivalence) instance RightModule Op Either Equivalence +deriving via (FromContra Predicate) instance RightModule Op Either Predicate +deriving via (FromContra (Op a)) instance RightModule Op Either (Op a) +deriving via (FromContra Proxy) instance RightModule Op Either Proxy +deriving via (FromContra U1) instance RightModule Op Either U1 +deriving via (FromContra V1) instance RightModule Op Either V1 +deriving via (FromContra (Const a)) instance RightModule Op Either (Const a) +deriving via (FromContra (Alt f)) instance Contravariant f => RightModule Op Either (Alt f) +deriving via (FromContra (Rec1 f)) instance Contravariant f => RightModule Op Either (Rec1 f) +deriving via (FromContra (Product f g)) instance (Contravariant f, Contravariant g) => RightModule Op Either (Product f g) +deriving via (FromContra (Sum f g)) instance (Contravariant f, Contravariant g) => RightModule Op Either (Sum f g) +deriving via (FromContra (f :+: g)) instance (Contravariant f, Contravariant g) => RightModule Op Either (f :+: g) +deriving via (FromContra (f :*: g)) instance (Contravariant f, Contravariant g) => RightModule Op Either (f :*: g) +deriving via (FromContra (K1 i c)) instance RightModule Op Either (K1 i c) +deriving via (FromContra (Compose f g)) instance (Functor f, Contravariant g) => RightModule Op Either (Compose f g) +deriving via (FromContra (f :.: g)) instance (Functor f, Contravariant g) => RightModule Op Either (f :.: g) +deriving via (FromContra (M1 i c f)) instance Contravariant f => RightModule Op Either (M1 i c f) + +deriving via FromFunctor Identity instance RightModule (->) Either Identity +deriving via FromFunctor (Compose f g) instance (Functor f, Functor g) => RightModule (->) Either (Compose f g) +deriving via FromFunctor [] instance RightModule (->) Either [] +deriving via FromFunctor ZipList instance RightModule (->) Either ZipList +deriving via FromFunctor NonEmpty instance RightModule (->) Either NonEmpty +deriving via FromFunctor Maybe instance RightModule (->) Either Maybe +deriving via FromFunctor (Either e) instance RightModule (->) Either (Either e) +deriving via FromFunctor (These a) instance RightModule (->) Either (These a) +deriving via FromFunctor IO instance RightModule (->) Either IO +deriving via FromFunctor (Sum f g) instance (Functor f, Functor g) => RightModule (->) Either (Sum f g) +deriving via FromFunctor (Product f g) instance (Functor f, Functor g) => RightModule (->) Either (Product f g) +deriving via (FromFunctor ((,) x1)) instance RightModule (->) Either ((,) x1) +deriving via (FromFunctor ((,,) x1 x2)) instance RightModule (->) Either ((,,) x1 x2) +deriving via (FromFunctor ((,,,) x1 x2 x3)) instance RightModule (->) Either ((,,,) x1 x2 x3) + +deriving via FromFunctor Identity instance RightModule (->) These Identity +deriving via FromFunctor (Compose f g) instance (Functor f, Functor g) => RightModule (->) These (Compose f g) +deriving via FromFunctor [] instance RightModule (->) These [] +deriving via FromFunctor ZipList instance RightModule (->) These ZipList +deriving via FromFunctor NonEmpty instance RightModule (->) These NonEmpty +deriving via FromFunctor Maybe instance RightModule (->) These Maybe +deriving via FromFunctor (Either e) instance RightModule (->) These (Either e) +deriving via FromFunctor (These a) instance RightModule (->) These (These a) +deriving via FromFunctor IO instance RightModule (->) These IO +deriving via FromFunctor (Sum f g) instance (Functor f, Functor g) => RightModule (->) These (Sum f g) +deriving via FromFunctor (Product f g) instance (Functor f, Functor g) => RightModule (->) These (Product f g) +deriving via (FromFunctor ((,) x1)) instance RightModule (->) These ((,) x1) +deriving via (FromFunctor ((,,) x1 x2)) instance RightModule (->) These ((,,) x1 x2) +deriving via (FromFunctor ((,,,) x1 x2 x3)) instance RightModule (->) These ((,,,) x1 x2 x3) + +deriving via FromFunctor Identity instance RightModule Op (,) Identity +deriving via FromFunctor (Compose f g) instance (Functor f, Functor g) => RightModule Op (,) (Compose f g) +deriving via FromFunctor [] instance RightModule Op (,) [] +deriving via FromFunctor ZipList instance RightModule Op (,) ZipList +deriving via FromFunctor NonEmpty instance RightModule Op (,) NonEmpty +deriving via FromFunctor Maybe instance RightModule Op (,) Maybe +deriving via FromFunctor (Either e) instance RightModule Op (,) (Either e) +deriving via FromFunctor IO instance RightModule Op (,) IO +deriving via FromFunctor (Sum f g) instance (Functor f, Functor g) => RightModule Op (,) (Sum f g) +deriving via FromFunctor (Product f g) instance (Functor f, Functor g) => RightModule Op (,) (Product f g) +deriving via (FromFunctor ((,) x1)) instance RightModule Op (,) ((,) x1) +deriving via (FromFunctor ((,,) x1 x2)) instance RightModule Op (,) ((,,) x1 x2) +deriving via (FromFunctor ((,,,) x1 x2 x3)) instance RightModule Op (,) ((,,,) x1 x2 x3) + +-------------------------------------------------------------------------------- + class (LeftModule cat t1 f, RightModule cat t1 f) => Bimodule cat t1 f + +instance Contravariant f => Bimodule (->) (,) (FromContra f) where +instance Contravariant f => Bimodule Op Either (FromContra f) where +instance Functor f => Bimodule (->) Either (FromFunctor f) where +instance Functor f => Bimodule (->) These (FromFunctor f) where +instance Functor f => Bimodule Op (,) (FromFunctor f) where + +deriving via (FromContra Comparison) instance Bimodule (->) (,) Comparison +deriving via (FromContra Equivalence) instance Bimodule (->) (,) Equivalence +deriving via (FromContra Predicate) instance Bimodule (->) (,) Predicate +deriving via (FromContra (Op a)) instance Bimodule (->) (,) (Op a) +deriving via (FromContra Proxy) instance Bimodule (->) (,) Proxy +deriving via (FromContra U1) instance Bimodule (->) (,) U1 +deriving via (FromContra V1) instance Bimodule (->) (,) V1 +deriving via (FromContra (Const a)) instance Bimodule (->) (,) (Const a) +deriving via (FromContra (Alt f)) instance Contravariant f => Bimodule (->) (,) (Alt f) +deriving via (FromContra (Rec1 f)) instance Contravariant f => Bimodule (->) (,) (Rec1 f) +deriving via (FromContra (Product f g)) instance (Contravariant f, Contravariant g) => Bimodule (->) (,) (Product f g) +deriving via (FromContra (Sum f g)) instance (Contravariant f, Contravariant g) => Bimodule (->) (,) (Sum f g) +deriving via (FromContra (f :+: g)) instance (Contravariant f, Contravariant g) => Bimodule (->) (,) (f :+: g) +deriving via (FromContra (f :*: g)) instance (Contravariant f, Contravariant g) => Bimodule (->) (,) (f :*: g) +deriving via (FromContra (K1 i c)) instance Bimodule (->) (,) (K1 i c) +deriving via (FromContra (Compose f g)) instance (Functor f, Contravariant g) => Bimodule (->) (,) (Compose f g) +deriving via (FromContra (f :.: g)) instance (Functor f, Contravariant g) => Bimodule (->) (,) (f :.: g) +deriving via (FromContra (M1 i c f)) instance Contravariant f => Bimodule (->) (,) (M1 i c f) + +deriving via (FromContra Comparison) instance Bimodule Op Either Comparison +deriving via (FromContra Equivalence) instance Bimodule Op Either Equivalence +deriving via (FromContra Predicate) instance Bimodule Op Either Predicate +deriving via (FromContra (Op a)) instance Bimodule Op Either (Op a) +deriving via (FromContra Proxy) instance Bimodule Op Either Proxy +deriving via (FromContra U1) instance Bimodule Op Either U1 +deriving via (FromContra V1) instance Bimodule Op Either V1 +deriving via (FromContra (Const a)) instance Bimodule Op Either (Const a) +deriving via (FromContra (Alt f)) instance Contravariant f => Bimodule Op Either (Alt f) +deriving via (FromContra (Rec1 f)) instance Contravariant f => Bimodule Op Either (Rec1 f) +deriving via (FromContra (Product f g)) instance (Contravariant f, Contravariant g) => Bimodule Op Either (Product f g) +deriving via (FromContra (Sum f g)) instance (Contravariant f, Contravariant g) => Bimodule Op Either (Sum f g) +deriving via (FromContra (f :+: g)) instance (Contravariant f, Contravariant g) => Bimodule Op Either (f :+: g) +deriving via (FromContra (f :*: g)) instance (Contravariant f, Contravariant g) => Bimodule Op Either (f :*: g) +deriving via (FromContra (K1 i c)) instance Bimodule Op Either (K1 i c) +deriving via (FromContra (Compose f g)) instance (Functor f, Contravariant g) => Bimodule Op Either (Compose f g) +deriving via (FromContra (f :.: g)) instance (Functor f, Contravariant g) => Bimodule Op Either (f :.: g) +deriving via (FromContra (M1 i c f)) instance Contravariant f => Bimodule Op Either (M1 i c f) + +deriving via FromFunctor Identity instance Bimodule (->) Either Identity +deriving via FromFunctor (Compose f g) instance (Functor f, Functor g) => Bimodule (->) Either (Compose f g) +deriving via FromFunctor [] instance Bimodule (->) Either [] +deriving via FromFunctor ZipList instance Bimodule (->) Either ZipList +deriving via FromFunctor NonEmpty instance Bimodule (->) Either NonEmpty +deriving via FromFunctor Maybe instance Bimodule (->) Either Maybe +deriving via FromFunctor (Either e) instance Bimodule (->) Either (Either e) +deriving via FromFunctor (These a) instance Bimodule (->) Either (These a) +deriving via FromFunctor IO instance Bimodule (->) Either IO +deriving via FromFunctor (Sum f g) instance (Functor f, Functor g) => Bimodule (->) Either (Sum f g) +deriving via FromFunctor (Product f g) instance (Functor f, Functor g) => Bimodule (->) Either (Product f g) +deriving via (FromFunctor ((,) x1)) instance Bimodule (->) Either ((,) x1) +deriving via (FromFunctor ((,,) x1 x2)) instance Bimodule (->) Either ((,,) x1 x2) +deriving via (FromFunctor ((,,,) x1 x2 x3)) instance Bimodule (->) Either ((,,,) x1 x2 x3) + +deriving via FromFunctor Identity instance Bimodule (->) These Identity +deriving via FromFunctor (Compose f g) instance (Functor f, Functor g) => Bimodule (->) These (Compose f g) +deriving via FromFunctor [] instance Bimodule (->) These [] +deriving via FromFunctor ZipList instance Bimodule (->) These ZipList +deriving via FromFunctor NonEmpty instance Bimodule (->) These NonEmpty +deriving via FromFunctor Maybe instance Bimodule (->) These Maybe +deriving via FromFunctor (Either e) instance Bimodule (->) These (Either e) +deriving via FromFunctor (These a) instance Bimodule (->) These (These a) +deriving via FromFunctor IO instance Bimodule (->) These IO +deriving via FromFunctor (Sum f g) instance (Functor f, Functor g) => Bimodule (->) These (Sum f g) +deriving via FromFunctor (Product f g) instance (Functor f, Functor g) => Bimodule (->) These (Product f g) +deriving via (FromFunctor ((,) x1)) instance Bimodule (->) These ((,) x1) +deriving via (FromFunctor ((,,) x1 x2)) instance Bimodule (->) These ((,,) x1 x2) +deriving via (FromFunctor ((,,,) x1 x2 x3)) instance Bimodule (->) These ((,,,) x1 x2 x3) + +deriving via FromFunctor Identity instance Bimodule Op (,) Identity +deriving via FromFunctor (Compose f g) instance (Functor f, Functor g) => Bimodule Op (,) (Compose f g) +deriving via FromFunctor [] instance Bimodule Op (,) [] +deriving via FromFunctor ZipList instance Bimodule Op (,) ZipList +deriving via FromFunctor NonEmpty instance Bimodule Op (,) NonEmpty +deriving via FromFunctor Maybe instance Bimodule Op (,) Maybe +deriving via FromFunctor (Either e) instance Bimodule Op (,) (Either e) +deriving via FromFunctor IO instance Bimodule Op (,) IO +deriving via FromFunctor (Sum f g) instance (Functor f, Functor g) => Bimodule Op (,) (Sum f g) +deriving via FromFunctor (Product f g) instance (Functor f, Functor g) => Bimodule Op (,) (Product f g) +deriving via (FromFunctor ((,) x1)) instance Bimodule Op (,) ((,) x1) +deriving via (FromFunctor ((,,) x1 x2)) instance Bimodule Op (,) ((,,) x1 x2) +deriving via (FromFunctor ((,,,) x1 x2 x3)) instance Bimodule Op (,) ((,,,) x1 x2 x3) diff --git a/src/Data/Functor/Monoidal.hs b/src/Data/Functor/Monoidal.hs --- a/src/Data/Functor/Monoidal.hs +++ b/src/Data/Functor/Monoidal.hs @@ -1,62 +1,152 @@ -module Data.Functor.Monoidal where +module Data.Functor.Monoidal + ( -- * Semigroupal + Semigroupal (..), -import Prelude + -- * Unital + Unital (..), + + -- * Monoidal + Monoidal, + ) +where + import Control.Applicative import Control.Category.Tensor +import Data.Align +import Data.These import Data.Void +import Prelude --- | A is a Functor between two Monoidal Categories --- which preserves the monoidal structure. Eg., a homomorphism of --- monoidal categories. +-------------------------------------------------------------------------------- + +-- | Given monoidal categories \((\mathcal{C}, \otimes, I_{\mathcal{C}})\) and \((\mathcal{D}, \bullet, I_{\mathcal{D}})\). +-- A functor \(F : \mathcal{C} \to \mathcal{D}\) is 'Semigroupal' if it supports a natural transformation +-- \(\phi_{A,B} : F\ A \bullet F\ B \to F\ (A \otimes B)\), which we call 'combine'. -- --- = Laws --- Associativity: --- combine (combine fx fy) fz ⟶ combine fx (combine fy fz) --- ↓ ↓ --- f (x `t1` y) `t1` fz combine fx (f (y `t1` z)) --- ↓ ↓ --- f ((x `t1` y) `t1` z) ⟶ (f x `t1` (y `t1` z)) +-- === Laws -- --- Left Unitality: --- empty `t1` f x ⟶ f empty `t1` f x --- ↓ ↓ --- f x ← f (empty `t0` x) +-- __Associativity:__ -- --- Right Unitality: --- f x `t1` empty ⟶ f x `t1` f empty --- ↓ ↓ --- f x ← f (x `t0` empty) -class ( Tensor t1 i1 cat - , Tensor t0 i0 cat - , Semigroupal cat t1 t0 f - , Unital cat i1 i0 f - ) => Monoidal cat t1 i1 t0 i0 f - -class (Associative t1 cat, Associative t0 cat) => Semigroupal cat t1 t0 f where +-- \[ +-- \require{AMScd} +-- \begin{CD} +-- (F A \bullet F B) \bullet F C @>>{\alpha_{\mathcal{D}}}> F A \bullet (F B \bullet F C) \\ +-- @VV{\phi_{A,B} \bullet 1}V @VV{1 \bullet \phi_{B,C}}V \\ +-- F (A \otimes B) \bullet F C @. F A \bullet (F (B \otimes C)) \\ +-- @VV{\phi_{A \otimes B,C}}V @VV{\phi_{A,B \otimes C}}V \\ +-- F ((A \otimes B) \otimes C) @>>{F \alpha_{\mathcal{C}}}> F (A \otimes (B \otimes C)) \\ +-- \end{CD} +-- \] +-- +-- @ +-- 'combine' 'Control.Category..' 'grmap' 'combine' 'Control.Category..' 'bwd' 'assoc' ≡ 'fmap' ('bwd' 'assoc') 'Control.Category..' 'combine' 'Control.Category..' 'glmap' 'combine' +-- @ +class (Associative cat t1, Associative cat t0) => Semigroupal cat t1 t0 f where + -- | @combine@ is a natural transformation from functors \(\mathcal{C} × \mathcal{C}\) to \(\mathcal{D}\). + -- + -- ==== __Examples__ + -- + -- >>> combine @(->) @(,) @(,) @Maybe (Just True, Just "hello") + -- Just (True,"hello") + -- + -- >>> combine @(->) @(,) @(,) @Maybe (Just True, Nothing) + -- Nothing + -- + -- >>> combine @(->) @Either @(,) @Maybe (Just True, Nothing) + -- Just (Left True) + -- + -- >>> combine @(->) @Either @(,) @Maybe (Nothing, Just "hello") + -- Just (Right "hello") combine :: (f x `t0` f x') `cat` f (x `t1` x') -class Unital cat i1 i0 f where - introduce :: i0 `cat` f i1 - --- TODO: Should we create an Apply class? instance Applicative f => Semigroupal (->) (,) (,) f where combine :: (f x, f x') -> f (x, x') combine = uncurry (liftA2 (,)) -instance Applicative f => Unital (->) () () f where - introduce :: () -> f () - introduce = pure - -instance Applicative f => Monoidal (->) (,) () (,) () f - --- TODO: Should we create an Alt class? instance Alternative f => Semigroupal (->) Either (,) f where combine :: (f x, f x') -> f (Either x x') combine (fx, fx') = fmap Left fx <|> fmap Right fx' --- TODO: Should we create a Plus class? +instance Semialign f => Semigroupal (->) These (,) f where + combine :: (f x, f x') -> f (These x x') + combine = uncurry align + +-------------------------------------------------------------------------------- + +-- | Given monoidal categories \((\mathcal{C}, \otimes, I_{\mathcal{C}})\) and \((\mathcal{D}, \bullet, I_{\mathcal{D}})\). +-- A functor \(F : \mathcal{C} \to \mathcal{D}\) is 'Unital' if it supports a morphism \(\phi : I_{\mathcal{D}} \to F\ I_{\mathcal{C}}\), +-- which we call 'introduce'. +class Unital cat i1 i0 f where + -- | @introduce@ maps from the identity in \(\mathcal{C}\) to the + -- identity in \(\mathcal{D}\). + -- + -- ==== __Examples__ + -- + -- >>> introduce @(->) @() @() @Maybe () + -- Just () + -- + -- >>> :t introduce @(->) @Void @() @Maybe + -- introduce @(->) @Void @() @Maybe :: () -> Maybe Void + -- + -- >>> introduce @(->) @Void @() @Maybe () + -- Nothing + introduce :: cat i0 (f i1) + +instance Applicative f => Unital (->) () () f where + introduce :: () -> f () + introduce = pure + instance Alternative f => Unital (->) Void () f where introduce :: () -> f Void introduce () = empty +-------------------------------------------------------------------------------- + +-- | Given monoidal categories \((\mathcal{C}, \otimes, I_{\mathcal{C}})\) and \((\mathcal{D}, \bullet, I_{\mathcal{D}})\). +-- A functor \(F : \mathcal{C} \to \mathcal{D}\) is 'Monoidal' if it maps between \(\mathcal{C}\) and \(\mathcal{D}\) while +-- preserving their monoidal structure. Eg., a homomorphism of monoidal categories. +-- +-- See for more details. +-- +-- === Laws +-- +-- __Right Unitality__: +-- +-- \[ +-- \require{AMScd} +-- \begin{CD} +-- F A \bullet I_{\mathcal{D}} @>{1 \bullet \phi}>> F A \bullet F I_{\mathcal{C}};\\ +-- @VV{\rho_{\mathcal{D}}}V @VV{\phi A,I_{\mathcal{C}}}V \\ +-- F A @<<{F \rho_{\mathcal{C}}}< F (A \otimes I_{\mathcal{C}}); +-- \end{CD} +-- \] +-- +-- @ +-- 'combine' 'Control.Category..' 'grmap' 'introduce' ≡ 'bwd' 'unitr' 'Control.Category..' 'fwd' 'unitr' +-- @ +-- +-- __ Left Unitality__: +-- +-- \[ +-- \begin{CD} +-- I_{\mathcal{D}} \bullet F B @>{\phi \bullet 1}>> F I_{\mathcal{C}} \bullet F B;\\ +-- @VV{\lambda_{\mathcal{D}}}V @VV{\phi I_{\mathcal{C}},B}V \\ +-- F A @<<{F \lambda_{\mathcal{C}}}< F (A \otimes I_{\mathcal{C}} \otimes B); +-- \end{CD} +-- \] +-- +-- @ +-- 'combine' 'Control.Category..' 'glmap' 'introduce' ≡ 'fmap' ('bwd' 'unitl') 'Control.Category..' 'fwd' 'unitl' +-- @ +class + ( Tensor cat t1 i1 + , Tensor cat t0 i0 + , Semigroupal cat t1 t0 f + , Unital cat i1 i0 f + ) => Monoidal cat t1 i1 t0 i0 f + +instance Applicative f => Monoidal (->) (,) () (,) () f + instance Alternative f => Monoidal (->) Either Void (,) () f + +instance (Alternative f, Semialign f) => Monoidal (->) These Void (,) () f diff --git a/src/Data/Trifunctor/Module.hs b/src/Data/Trifunctor/Module.hs --- a/src/Data/Trifunctor/Module.hs +++ b/src/Data/Trifunctor/Module.hs @@ -1,10 +1,25 @@ -module Data.Trifunctor.Module where +module Data.Trifunctor.Module + ( -- * LeftModule + LeftModule (..), + -- * RightModule + RightModule (..), + -- * Bimodule + Bimodule, + ) +where + +-------------------------------------------------------------------------------- + class LeftModule cat t1 t2 t3 f where lstrength :: cat (f a b c) (f (t1 a x) (t2 b x) (t3 c x)) +-------------------------------------------------------------------------------- + class RightModule cat t1 t2 t3 f where rstrength :: cat (f a b c) (f (t1 x a) (t2 x b) (t3 x c)) + +-------------------------------------------------------------------------------- class (LeftModule cat t1 t2 t3 f, RightModule cat t1 t2 t3 f) => Bimodule cat t1 t2 t3 f diff --git a/src/Data/Trifunctor/Monoidal.hs b/src/Data/Trifunctor/Monoidal.hs --- a/src/Data/Trifunctor/Monoidal.hs +++ b/src/Data/Trifunctor/Monoidal.hs @@ -1,23 +1,106 @@ -module Data.Trifunctor.Monoidal where +module Data.Trifunctor.Monoidal + ( -- * Semigroupal + Semigroupal (..), -import Control.Category.Tensor + -- * Unital + Unital (..), + -- * Monoidal + Monoidal, + ) +where + +-------------------------------------------------------------------------------- + +import Control.Category.Tensor (Associative, Tensor) + +-------------------------------------------------------------------------------- + +-- | Given monoidal categories \((\mathcal{C}, \otimes, I_{\mathcal{C}})\) and \((\mathcal{D}, \bullet, I_{\mathcal{D}})\). +-- A bifunctor \(F : \mathcal{C_1} \times \mathcal{C_2} \times \mathcal{C_3} \to \mathcal{D}\) is 'Semigroupal' if it supports a +-- natural transformation \(\phi_{ABC,XYZ} : F\ A\ B\ C \bullet F\ X\ Y\ Z \to F\ (A \otimes X)\ (B \otimes Y)\ (C \otimes Z)\), which we call 'combine'. +-- +-- === Laws +-- +-- __Associativity:__ +-- +-- \[ +-- \require{AMScd} +-- \begin{CD} +-- (F A B C \bullet F X Y Z) \bullet F P Q R @>>{\alpha_{\mathcal{D}}}> F A B C \bullet (F X Y Z \bullet F P Q R) \\ +-- @VV{\phi_{ABC,XYZ} \bullet 1}V @VV{1 \bullet \phi_{XYZ,PQR}}V \\ +-- F (A \otimes X) (B \otimes Y) (C \otimes Z) \bullet F P Q R @. F A B C \bullet (F (X \otimes P) (Y \otimes Q) (Z \otimes R) \\ +-- @VV{\phi_{(A \otimes X)(B \otimes Y)(C \otimes Z),PQR}}V @VV{\phi_{ABC,(X \otimes P)(Y \otimes Q)(Z \otimes R)}}V \\ +-- F ((A \otimes X) \otimes P) ((B \otimes Y) \otimes Q) ((C \otimes Z) \otimes R) @>>{F \alpha_{\mathcal{C_1}}} \alpha_{\mathcal{C_2}}\alpha_{\mathcal{C_3}}> F (A \otimes (X \otimes P)) (B \otimes (Y \otimes Q)) (C \otimes (Z \otimes R)) \\ +-- \end{CD} +-- \] +-- +-- @ +-- 'combine' 'Control.Category..' 'Control.Category.Tensor.grmap' 'Control.Category.Tensor.combine' 'Control.Category..' 'Control.Category.Tensor.bwd' 'Control.Category.Tensor.assoc' ≡ 'Data.Functor.fmap' ('Control.Category.Tensor.bwd' 'Control.Category.Tensor.assoc') 'Control.Category..' 'combine' 'Control.Category..' 'Control.Category.Tensor.glmap' 'combine' +-- @ class - ( Associative t1 cat - , Associative t2 cat - , Associative t3 cat - , Associative to cat + ( Associative cat t1 + , Associative cat t2 + , Associative cat t3 + , Associative cat to ) => Semigroupal cat t1 t2 t3 to f where + -- | A natural transformation \(\phi_{ABC,XYZ} : F\ A\ B\ C \bullet F\ X\ Y\ Z \to F\ (A \otimes X)\ (B \otimes Y) (C \otimes Z)\). combine :: to (f x y z) (f x' y' z') `cat` f (t1 x x') (t2 y y') (t3 z z') +-------------------------------------------------------------------------------- + +-- | Given monoidal categories \((\mathcal{C}, \otimes, I_{\mathcal{C}})\) and \((\mathcal{D}, \bullet, I_{\mathcal{D}})\). +-- A bifunctor \(F : \mathcal{C_1} \times \mathcal{C_2} \times \mathcal{C_3} \to \mathcal{D}\) is 'Unital' if it supports a morphism +-- \(\phi : I_{\mathcal{D}} \to F\ I_{\mathcal{C_1}}\ I_{\mathcal{C_2}}\ I_{\mathcal{C_3}}\), which we call 'introduce'. class Unital cat i1 i2 i3 o f where + -- | @introduce@ maps from the identity in \(\mathcal{C_1} \times \mathcal{C_2} \times \mathcal{C_3}\) to the + -- identity in \(\mathcal{D}\). introduce :: o `cat` f i1 i2 i3 +-------------------------------------------------------------------------------- + +-- | Given monoidal categories \((\mathcal{C}, \otimes, I_{\mathcal{C}})\) and \((\mathcal{D}, \bullet, I_{\mathcal{D}})\). +-- A bifunctor \(F : \mathcal{C_1} \times \mathcal{C_2} \times \mathcal{C_3} \to \mathcal{D}\) is 'Monoidal' if it maps between +-- \(\mathcal{C_1} \times \mathcal{C_2}\ \times \mathcal{C_3}\) and \(\mathcal{D}\) while preserving their monoidal structure. +-- Eg., a homomorphism of monoidal categories. +-- +-- See for more details. +-- +-- === Laws +-- +-- __Right Unitality:__ +-- +-- \[ +-- \require{AMScd} +-- \begin{CD} +-- F A B C \bullet I_{\mathcal{D}} @>{1 \bullet \phi}>> F A B \bullet F I_{\mathcal{C_{1}}} I_{\mathcal{C_{2}}} I_{\mathcal{C_{3}}}\\ +-- @VV{\rho_{\mathcal{D}}}V @VV{\phi ABC,I_{\mathcal{C_{1}}}I_{\mathcal{C_{2}}}I_{\mathcal{C_{3}}}}V \\ +-- F A B C @<<{F \rho_{\mathcal{C_{1}}} \rho_{\mathcal{C_{2}}} \rho_{\mathcal{C_{3}}}}< F (A \otimes I_{\mathcal{C_{1}}}) (B \otimes I_{\mathcal{C_{2}}}) (C \otimes I_{\mathcal{C_{3}}}) +-- \end{CD} +-- \] +-- +-- @ +-- 'combine' 'Control.Category..' 'Control.Category.Tensor.grmap' 'introduce' ≡ 'Control.Category.Tensor.bwd' 'Control.Category.Tensor.unitr' 'Control.Category..' 'Control.Category.Tensor.fwd' 'Control.Category.Tensor.unitr' +-- @ +-- +-- __ Left Unitality__: +-- +-- \[ +-- \begin{CD} +-- I_{\mathcal{D}} \bullet F A B C @>{\phi \bullet 1}>> F I_{\mathcal{C_{1}}} I_{\mathcal{C_{2}}} \bullet F A B C\\ +-- @VV{\lambda_{\mathcal{D}}}V @VV{I_{\mathcal{C_{1}}}I_{\mathcal{C_{2}}}I_{\mathcal{C_{3}}},\phi ABC}V \\ +-- F A B C @<<{F \lambda_{\mathcal{C_{1}}} \lambda_{\mathcal{C_{2}}} \lambda_{\mathcal{C_{3}}}}< F (I_{\mathcal{C_{1}}} \otimes A) (I_{\mathcal{C_{2}}} \otimes B) (I_{\mathcal{C_{3}}} \otimes C) +-- \end{CD} +-- \] +-- +-- @ +-- 'combine' 'Control.Category..' 'Control.Category.Tensor.glmap' 'introduce' ≡ 'Data.Functor.fmap' ('Control.Category.Tensor.bwd' 'Control.Category.Tensor.unitl') 'Control.Category..' 'Control.Category.Tensor.fwd' 'Control.Category.Tensor.unitl' +-- @ class - ( Tensor t1 i1 cat - , Tensor t2 i2 cat - , Tensor t3 i3 cat - , Tensor to io cat + ( Tensor cat t1 i1 + , Tensor cat t2 i2 + , Tensor cat t3 i3 + , Tensor cat to io , Semigroupal cat t1 t2 t3 to f , Unital cat i1 i2 i3 io f ) => Monoidal cat t1 i1 t2 i2 t3 i3 to io f