From 2a221267ace22d04386a87461e868786331275be Mon Sep 17 00:00:00 2001
From: Tom Ellis <tom-git@jaguarpaw.co.uk>
Date: Sat, 23 Oct 2021 11:10:18 +0100
Subject: [PATCH] Implement a new typeclass hierarchy

Defines:

* Profunctor => SemiproductProfunctor => ProductProfunctor

  This operates on tuples, and gives the operations from the
  Applicative(Apply) and Divisible(Divise) typeclasses.

* Profunctor => SemisumProfunctor => SumProfunctor

  This operates on Eithers, and gives the operations from the
  Decidable (Decide/Conclude) typeclasses.

Patch courtesy of Jack Kelly @endgame
---
 Data/Profunctor/Product.hs               | 219 +++++++++++-------
 Data/Profunctor/Product/Class.hs         | 282 +++++++++++++++--------
 Data/Profunctor/Product/Default.hs       |   1 -
 Data/Profunctor/Product/Default/Class.hs |   2 +-
 Data/Profunctor/Product/Examples.hs      |  27 ++-
 Data/Profunctor/Product/Internal/TH.hs   |   2 +-
 Data/Profunctor/Product/Tuples/TH.hs     |   7 +-
 7 files changed, 350 insertions(+), 190 deletions(-)

diff --git a/Data/Profunctor/Product.hs b/Data/Profunctor/Product.hs
index 68a63604..43bc1cc7 100644
--- a/Data/Profunctor/Product.hs
+++ b/Data/Profunctor/Product.hs
@@ -1,21 +1,58 @@
 {-# OPTIONS_GHC -Wno-orphans #-}
 {-# LANGUAGE TemplateHaskell #-}
 
+-- | The classes in this module provide "profunctorial" analogues to
+-- the operations from the 'Applicative' (@Apply@),
+-- 'Data.Functor.Contravariant.Divisible.Divisible' (@Divise@) and
+-- 'Data.Functor.Contravariant.Divisible.Decidable' (@Conclude@) type
+-- classes:
+--
+-- @
+-- ('<*>')  :: 'Applicative'           f => f   (a -> b) -> f   a -> f   b
+-- ('****') :: 'SemiproductProfunctor' p => p x (a -> b) -> p x a -> p x b
+--
+-- 'Control.Applicative.liftA2' :: 'Applicative'           f => (a -> b -> c) -> f   a -> f   b -> f   c
+-- 'liftP2' :: 'SemiproductProfunctor' p => (a -> b -> c) -> p x a -> p x b -> p x c
+--
+-- pure  :: 'Applicative'           f => a -> f   a
+-- 'pureP' :: 'SemiproductProfunctor' p => a -> p x a
+--
+-- divide  ::                           'Data.Functor.Contravariant.Divisible.Divisible' f  => (a -> (b, c)) -> f b   -> f c   -> f a -- From contravariant
+-- divise  ::                              Divise f  => (a -> (b, c)) -> f b   -> f c   -> f a -- From semigroupoids
+-- 'diviseP' :: ('Semigroup' x, 'SemiproductProfunctor' p) => (a -> (b, c)) -> p a x -> p b x -> p c x
+--
+-- conquer ::                      'Data.Functor.Contravariant.Divisible.Decidable' f => f a -- From contravariant
+-- 'conquerP' :: ('Monoid' x, 'ProductProfunctor' p) => p a x
+--
+-- choose  :: 'Data.Functor.Contravariant.Divisible.Decidable'         f => (a -> 'Either' b c) -> f b   -> f c   -> f a -- From contravariant
+-- decide  :: Decide            f => (a -> 'Either' b c) -> f b   -> f c   -> f a -- From semigroupoids
+-- 'decideP' :: 'SemisumProfunctor' p => (a -> 'Either' b c) -> p b x -> p c x -> p a x
+--
+-- lose      :: 'Data.Functor.Contravariant.Divisible.Decidable'     f => (a -> 'Void') -> f a -- From contravariant
+-- conclude  :: Conclude      f => (a -> 'Void') -> f a -- From semigroupoids
+-- 'concludeP' :: 'SumProfunctor' p => (a -> 'Void') -> p a x
+-- @
+--
+-- The @(Semi){Sum,Product}Profunctor@ classes also provide more
+-- primitive operations using @Either@ and @(,)@. These can be very
+-- useful with the @<https://hackage.haskell.org/package/generics-eot generics-eot>@
+-- package, which can automatically convert data types that have a
+-- 'Generic' instance into Eithers-of-Tuples.
 module Data.Profunctor.Product (module Data.Profunctor.Product.Class,
                                 module Data.Profunctor.Product.Newtype,
                                 module Data.Profunctor.Product) where
 
 import Prelude hiding (id)
-import Data.Profunctor (Profunctor, lmap, WrappedArrow, Star(..), Costar)
+import Data.Profunctor (Profunctor(..), WrappedArrow, Star(..), Costar, Forget(..))
 import qualified Data.Profunctor as Profunctor
 import Data.Profunctor.Composition (Procompose(..))
-import Data.Functor.Contravariant.Divisible (Divisible(..), Decidable, chosen)
+import Data.Functor.Contravariant.Divisible (Divisible(..), Decidable, chosen, lost)
 import Control.Category (id)
-import Control.Arrow (Arrow, (***), ArrowChoice, (+++))
-import Control.Applicative (Applicative, liftA2, pure, (<*>), Alternative, (<|>), (<$>))
+import Control.Arrow (Arrow(..), ArrowChoice(..))
+import Control.Applicative (Applicative(..), Alternative(..))
 
-import Data.Monoid (Monoid, mempty)
 import Data.Tagged
+import Data.Void (absurd)
 
 import Data.Bifunctor.Biff
 import Data.Bifunctor.Clown
@@ -30,51 +67,6 @@ import Data.Profunctor.Product.Flatten
 import Data.Profunctor.Product.Tuples
 import Data.Profunctor.Product.Tuples.TH (pTns, maxTupleSize, pNs)
 
--- ProductProfunctor and ProductContravariant are potentially
--- redundant type classes.  It seems to me that these are equivalent
--- to Profunctor with Applicative, and Contravariant with Monoid
--- respectively:
---
---    import Data.Profunctor
---    import Control.Applicative hiding (empty)
---    import Data.Functor.Contravariant
---    import Data.Monoid
---
---    empty :: (Applicative (p ())) => p () ()
---    empty = pure ()
---
---    (***!) :: (Applicative (p (a, a')), Profunctor p) =>
---                p a b -> p a' b' -> p (a, a') (b, b')
---    p ***! p' = (,) <$> lmap fst p <*> lmap snd p'
---
---    point :: Monoid (f ()) => f ()
---    point = mempty
---
---    (***<) :: (Monoid (f (a, b)), Contravariant f) =>
---                f a -> f b -> f (a, b)
---    p ***< p' = contramap fst p <> contramap snd p'
---
---
--- The only thing that makes me think that they are not *completely*
--- redundant is that (***!) and (***<) have to be defined
--- polymorphically in the type arguments, whereas if we took the
--- Profunctor+Applicative or Contravariant+Monoid approach we do not
--- have a guarantee that these operations are polymorphic.
---
--- Previously I wanted to replace ProductProfunctor and
--- ProductContravariant entirely.  This proved difficult as it is not
--- possible to expand the class constraints to require Applicative and
--- Monoid respectively.  We can't enforce a constraint 'Applicative (p
--- a)' where 'a' does not appear in the head.  This seems closely
--- related to the above issue of adhoc implementations.
---
--- There is a potential method of working around this issue using the
--- 'constraints' package:
--- stackoverflow.com/questions/12718268/polymorphic-constraint/12718620
---
--- Still, at least we now have default implementations of the class
--- methods, which makes things simpler.
-
 -- | '***$' is the generalisation of 'Functor''s @\<$\>@.
 --
 -- '***$' = 'Profunctor.rmap', just like '<$>' = 'fmap'.
@@ -84,92 +76,153 @@ import Data.Profunctor.Product.Tuples.TH (pTns, maxTupleSize, pNs)
 (***$) :: Profunctor p => (b -> c) -> p a b -> p a c
 (***$) = Profunctor.rmap
 
-instance ProductProfunctor (->) where
-  purePP = pure
+-- { Product
+
+instance SemiproductProfunctor (->) where
   (****) = (<*>)
 
-instance Arrow arr => ProductProfunctor (WrappedArrow arr) where
-  empty  = id
+instance ProductProfunctor (->) where
+  pureP = pure
+
+instance Arrow arr => SemiproductProfunctor (WrappedArrow arr) where
   (***!) = (***)
 
+instance Arrow arr => ProductProfunctor (WrappedArrow arr) where
+  unitP = arr id
+
+instance SemiproductProfunctor Tagged where
+  (****) = (<*>)
+
 instance ProductProfunctor Tagged where
-  purePP = pure
+  pureP = pure
+
+-- Should this use Apply?
+instance Applicative f => SemiproductProfunctor (Star f) where
   (****) = (<*>)
 
 instance Applicative f => ProductProfunctor (Star f) where
-  purePP = pure
+  pureP = pure
+
+instance Functor f => SemiproductProfunctor (Costar f) where
   (****) = (<*>)
 
 instance Functor f => ProductProfunctor (Costar f) where
-  purePP = pure
-  (****) = (<*>)
+  pureP = pure
 
-instance (ProductProfunctor p, ProductProfunctor q) => ProductProfunctor (Procompose p q) where
-  purePP a = Procompose (purePP a) (purePP ())
+instance (SemiproductProfunctor p, SemiproductProfunctor q) => SemiproductProfunctor (Procompose p q) where
   Procompose pf qf **** Procompose pa qa =
-    Procompose (lmap fst pf **** lmap snd pa) ((,) ***$ qf **** qa)
+    Procompose (lmap fst pf **** lmap snd pa) (liftP2 (,) qf qa)
+
+instance (ProductProfunctor p, ProductProfunctor q) => ProductProfunctor (Procompose p q) where
+  pureP a = Procompose (pureP a) (pureP ())
+
+instance (Functor f, Applicative g, SemiproductProfunctor p) => SemiproductProfunctor (Biff p f g) where
+  Biff abc **** Biff ab = Biff $ liftP2 (<*>) abc ab
 
 instance (Functor f, Applicative g, ProductProfunctor p) => ProductProfunctor (Biff p f g) where
-  purePP = Biff . purePP . pure
-  Biff abc **** Biff ab = Biff $ (<*>) ***$ abc **** ab
+  pureP = Biff . pureP . pure
 
-instance Applicative f => ProductProfunctor (Joker f) where
-  purePP = Joker . pure
+-- Should this use Apply?
+instance Applicative f => SemiproductProfunctor (Joker f) where
   Joker bc **** Joker b = Joker $ bc <*> b
 
-instance Divisible f => ProductProfunctor (Clown f) where
-  purePP _ = Clown conquer
+instance Applicative f => ProductProfunctor (Joker f) where
+  pureP = Joker . pure
+
+-- Should this use Devise?
+instance Divisible f => SemiproductProfunctor (Clown f) where
   Clown l **** Clown r = Clown $ divide (\a -> (a, a)) l r
 
-instance (ProductProfunctor p, ProductProfunctor q) => ProductProfunctor (Product p q) where
-  purePP a = Pair (purePP a) (purePP a)
+instance Divisible f => ProductProfunctor (Clown f) where
+  pureP _ = Clown conquer
+
+instance (SemiproductProfunctor p, SemiproductProfunctor q) => SemiproductProfunctor (Product p q) where
   Pair l1 l2 **** Pair r1 r2 = Pair (l1 **** r1) (l2 **** r2)
 
-instance (Applicative f, ProductProfunctor p) => ProductProfunctor (Tannen f p) where
-  purePP = Tannen . pure . purePP
+instance (ProductProfunctor p, ProductProfunctor q) => ProductProfunctor (Product p q) where
+  pureP a = Pair (pureP a) (pureP a)
+
+-- Should this use Apply?
+instance (Applicative f, SemiproductProfunctor p) => SemiproductProfunctor (Tannen f p) where
   Tannen f **** Tannen a = Tannen $ liftA2 (****) f a
 
+instance (Applicative f, ProductProfunctor p) => ProductProfunctor (Tannen f p) where
+  pureP = Tannen . pure . pureP
+
+-- }
+
 -- { Sum
 
-instance SumProfunctor (->) where
+instance SemisumProfunctor (->) where
   f +++! g = either (Left . f) (Right . g)
 
-instance ArrowChoice arr => SumProfunctor (WrappedArrow arr) where
+instance SumProfunctor (->) where
+  voidP = id
+
+instance ArrowChoice arr => SemisumProfunctor (WrappedArrow arr) where
   (+++!) = (+++)
 
-instance Applicative f => SumProfunctor (Star f) where
+instance ArrowChoice arr => SumProfunctor (WrappedArrow arr) where
+  voidP = arr id
+
+instance SemisumProfunctor (Forget r) where
+  Forget f +++! Forget g = Forget $ either f g
+
+instance SumProfunctor (Forget r) where
+  voidP = Forget absurd
+
+instance Functor f => SemisumProfunctor (Star f) where
   Star f +++! Star g = Star $ either (fmap Left . f) (fmap Right . g)
 
-instance (SumProfunctor p, SumProfunctor q) => SumProfunctor (Procompose p q) where
+instance Applicative f => SumProfunctor (Star f) where
+  voidP = Star pure
+
+instance (SemisumProfunctor p, SemisumProfunctor q) => SemisumProfunctor (Procompose p q) where
   Procompose pa qa +++! Procompose pb qb = Procompose (pa +++! pb) (qa +++! qb)
 
-instance Alternative f => SumProfunctor (Joker f) where
+instance (SumProfunctor p, SumProfunctor q) => SumProfunctor (Procompose p q) where
+  voidP = Procompose voidP voidP
+
+-- Should this use Alt?
+instance Alternative f => SemisumProfunctor (Joker f) where
   Joker f +++! Joker g = Joker $ Left <$> f <|> Right <$> g
 
-instance Decidable f => SumProfunctor (Clown f) where
+instance Alternative f => SumProfunctor (Joker f) where
+  voidP = Joker $ absurd <$> empty
+
+-- Should this use Decide?
+instance Decidable f => SemisumProfunctor (Clown f) where
   Clown f +++! Clown g = Clown $ chosen f g
 
-instance (SumProfunctor p, SumProfunctor q) => SumProfunctor (Product p q) where
+-- Should this use Conclude?
+instance Decidable f => SumProfunctor (Clown f) where
+  voidP = Clown lost
+
+instance (SemisumProfunctor p, SemisumProfunctor q) => SemisumProfunctor (Product p q) where
   Pair l1 l2 +++! Pair r1 r2 = Pair (l1 +++! r1) (l2 +++! r2)
 
-instance (Applicative f, SumProfunctor p) => SumProfunctor (Tannen f p) where
+instance (SumProfunctor p, SumProfunctor q) => SumProfunctor (Product p q) where
+  voidP = Pair voidP voidP
+
+-- Should this use Apply?
+instance (Applicative f, SemisumProfunctor p) => SemisumProfunctor (Tannen f p) where
   Tannen l +++! Tannen r = Tannen $ liftA2 (+++!) l r
 
+instance (Applicative f, SumProfunctor p) => SumProfunctor (Tannen f p) where
+  voidP = Tannen $ pure voidP
+
 -- | A generalisation of @map :: (a -> b) -> [a] -> [b]@.  It is also,
 -- in spirit, a generalisation of @traverse :: (a -> f b) -> [a] -> f
 -- [b]@, but the types need to be shuffled around a bit to make that
 -- work.
 list :: (ProductProfunctor p, SumProfunctor p) => p a b -> p [a] [b]
-list p = Profunctor.dimap fromList toList (empty +++! (p ***! list p))
+list p = Profunctor.dimap fromList toList (unitP +++! (p ***! list p))
   where toList :: Either () (a, [a]) -> [a]
         toList = either (const []) (uncurry (:))
         fromList :: [a] -> Either () (a, [a])
         fromList []     = Left ()
         fromList (a:as) = Right (a, as)
 
--- SumContravariant would be 'Data.Functor.Contravariant.Decidable'
--- (without the requirement to also be Divisible).
-
 -- }
 
 pTns [0..maxTupleSize]
diff --git a/Data/Profunctor/Product/Class.hs b/Data/Profunctor/Product/Class.hs
index c8c11b56..a7c73921 100644
--- a/Data/Profunctor/Product/Class.hs
+++ b/Data/Profunctor/Product/Class.hs
@@ -1,45 +1,17 @@
 module Data.Profunctor.Product.Class where
 
-import           Data.Profunctor (Profunctor)
-import qualified Data.Profunctor as Profunctor
-
--- | 'ProductProfunctor' is a generalization of
--- 'Control.Applicative.Applicative'.
--- It has the usual 'Control.Applicative.Applicative' "output"
--- (covariant) parameter on the right.  Additionally it has an "input"
--- (contravariant) type parameter on the left.
---
--- The methods for 'ProductProfunctor' correspond closely to those for
--- 'Control.Applicative.Applicative' as laid out in the following
--- table.
--- The only difference between them is that the 'ProductProfunctor'
--- has a contravariant type parameter on the left.  We can use the
--- contravariant to compose them in nice ways as described at
--- "Data.Profunctor.Product".
---
--- @
--- | Correspondence between Applicative and ProductProfunctor
--- |
--- |  'Control.Applicative.Applicative' f           'ProductProfunctor' p
--- |
--- |  'Control.Applicative.pure'                    'purePP'
--- |    :: b -> f b             :: b -> p a b
--- |
--- |  ('Control.Applicative.<$>')                   ('Data.Profunctor.Product.***$')
--- |    :: (b -> b')            :: (b -> b')
--- |    -> f b                  -> p a b
--- |    -> f b'                 -> p a b'
--- |
--- |  ('Control.Applicative.<*>')                   ('****')
--- |    :: f (b -> b')          :: p a (b -> b')
--- |    -> f b                  -> p a b
--- |    -> f b'                 -> p a b'
--- @
---
--- If @p@ is an instance of 'ProductProfunctor' then @p a a'@
--- represents a sort of process for turning @a@s into @a'@s that can
--- be "laid out side-by-side" with other values of @p@ to form "wider"
--- processes.  For example, if I have
+import           Data.Profunctor (Profunctor(..))
+import           Data.Void (Void, absurd)
+
+-- | A 'SemiproductProfunctor' is a profunctor whose input and output
+-- values can be combined with @(,)@. ('***!') makes this most
+-- obvious, though ('****') and 'liftP2' are equivalent in power.
+--
+-- A value of type @p a x@ with an @instance 'SemiproductProfunctor' p@
+-- often represents some sort of process for turning @a@s into @x@s
+-- that can be "laid out side-by-side" with other similar values of
+-- @p@ to form "wider" processes. For example, if I have three such
+-- encoders:
 --
 -- @
 -- p :: p a x -- a process for turning as into xs
@@ -47,69 +19,199 @@ import qualified Data.Profunctor as Profunctor
 -- r :: p c z -- a process for turning cs into zs
 -- @
 --
--- then I can combine them using 'p3' to get
+-- I can then combine them using 'p3' to get:
 --
 -- @
--- p3 p q r :: p (a, b, c) (x, y, z)
 -- -- a process for turning (a, b, c)s into (x, y, z)s
+-- p3 p q r :: p (a, b, c) (x, y, z)
 -- @
 --
 -- You would typically compose 'ProductProfunctor's using
--- 'Profunctors''s 'Profunctor.lmap' and 'Applicative''s 'pure',
--- '<$>' / 'fmap' and '<*>'.
+-- 'Profunctor'\'s 'lmap', '<$>' \/ 'fmap', and @Apply@ \/
+-- 'Applicative'\'s 'pure' and @\<.\>@ \/ @('<*>')@.
 --
--- It's easy to make instances of 'ProductProfunctor'.  Just make
--- instances
+-- You can often write these instances mechancially:
 --
 -- @
---  instance 'Profunctor' MyProductProfunctor where
---    ...
---
---  instance 'Control.Applicative.Applicative' (MyProductProfunctor a) where
---    ...
+-- instance SemiproductProfunctor P where
+--   (****) = (\<.\>) -- If you have `instance Apply (P a)`
+--   (****) = ('<*>') -- If you have `instance 'Applicative' (P a)`
 -- @
 --
--- and then write
+-- Laws:
+--
+--  * @('***!')@ is associative up to tuple rearrangement.
+--
+--  * If @p@ is also a 'SemisumProfunctor', @('***!')@ should
+--    distribute over @('+++!')@ up to tuple/@Either@ rearrangement.
+class Profunctor p => SemiproductProfunctor p where
+  (***!) :: p a c -> p b d -> p (a, b) (c, d)
+  p ***! q = liftP2 (,) (lmap fst p) (lmap snd q)
+
+  -- | Analogue to @('<*>')@.
+  (****) :: p x (a -> b) -> p x a -> p x b
+  p **** q = dimap (\x -> (x, x)) (uncurry ($)) $ p ***! q
+
+  -- | Analogue to 'liftA2'.
+  liftP2 :: (a -> b -> c) -> p x a -> p x b -> p x c
+  liftP2 f p q = rmap f p **** q
+
+  -- | Analogue to @divise@ (from "semigroupoids") or
+  -- 'Data.Functor.Contravariant.Divisible.decide' (from
+  -- "contravariant"). The 'Semigroup' constraint is necessary to
+  -- combine the "output" values.
+  --
+  -- Why didn't we need a constraint when writing the analogues to
+  -- 'Applicative' operations? In the absence of linear types, there
+  -- are only trivial comonoids; we can always produce a function to
+  -- "duplicate" the input.
+  diviseP :: Semigroup x => (a -> (b,c)) -> p b x -> p c x -> p a x
+  diviseP f p q = dimap f (uncurry (<>)) $ p ***! q
+  {-# MINIMAL (***!) | (****) | liftP2 #-}
+
+-- | Analogue to @divised@ from "semigroupoids" or
+-- 'Data.Functor.Contravariant.Divisible.divided' from
+-- "contravariant".
+divisedP ::
+  (SemiproductProfunctor p, Semigroup x) => p a x -> p b x -> p (a, b) x
+divisedP = diviseP id
+
+-- | 'SemiproductProfunctor's with a unit.
+--
+-- If you have an 'Applicative' instance for @P a@, you can write this
+-- instance mechanically:
 --
 -- @
---  instance 'ProductProfunctor' MyProductProfunctor where
---    'purePP' = 'Control.Applicative.pure'
---    ('****') = ('Control.Applicative.<*>')
+-- instance ProductProfunctor p where
+--   pureP = pure
 -- @
-class Profunctor p => ProductProfunctor p where
-  -- | 'purePP' is the generalisation of @Applicative@'s
-  -- 'Control.Applicative.pure'.
+--
+-- Law: @unitP@ is an identity for @('***!')@, up to tuple
+-- rearrangement.
+class SemiproductProfunctor p => ProductProfunctor p where
+  -- | Unit for @('***!')@.
+  unitP :: p () ()
+  unitP = pureP ()
+
+  -- | Analogue to 'pure'.
+  pureP :: a -> p x a
+  pureP a = dimap (const ()) (const a) unitP
+
+  -- | Analogue to 'Data.Functor.Contravariant.Divisible.conquer'
+  -- (from "contravariant"). The 'Monoid' constraint is necessary to
+  -- provide a "default" value to emit.
   --
-  -- (You probably won't need to use this except to define
-  -- 'ProductProfunctor' instances.  In your own code @pure@ should be
-  -- sufficient.)
-  purePP :: b -> p a b
-  purePP b = Profunctor.dimap (const ()) (const b) empty
-
-  -- | '****' is the generalisation of @Applicative@'s
-  -- 'Control.Applicative.<*>'.
+  -- Unit for 'diviseP'.
+  conquerP :: Monoid x => p a x
+  conquerP = pureP mempty
+  {-# MINIMAL unitP | pureP #-}
+
+-- | As redundant as 'Data.Functor.Contravariant.Divisible.conquered'
+-- from "contravariant", but also provided for symmetry.
+conqueredP :: (ProductProfunctor p, Monoid x) => p () x
+conqueredP = conquerP
+
+-- | A 'SemisumProfunctor' is a profunctor whose input and output
+-- values can be combined with 'Either'.
+--
+-- You can often write these instances mechanically:
+--
+-- @
+-- instance SemisumProfunctor P where
+--   decideP f p q = 'Data.Bifunctor.Flip.runFlip' $ decide f ('Data.Bifunctor.Flip.Flip' p) ('Data.Bifunctor.Flip.Flip' q) -- If you have `instance Decide (Flip P a)`
+--   decideP f p q = 'Data.Bifunctor.Flip.runFlip' $ 'Data.Functor.Contravariant.Divisible.choose' f ('Data.Bifunctor.Flip.Flip' p) ('Data.Bifunctor.Flip.Flip' q) -- If you have `instance 'Data.Functor.Contravariant.Divisible.Decidable' (Flip P a)`
+-- @
+--
+-- Laws:
+--
+--  * @('+++!')@ is associative up to 'Either' rearrangement.
+--
+--  * If @p@ is also a 'SemiproductProfunctor', @('***!')@ should
+--    distribute over @('+++!')@ up to tuple/'Either' rearrangement.
+--
+-- === Where is the 'Control.Applicative.Alternative' analogue?
+--
+-- It is possible to write a version of @('Control.Applicative.<|>')@
+-- that uses 'Either's:
+--
+-- @
+-- alt :: 'Control.Applicative.Alternative' f => f a -> f b -> f ('Either' a b)
+-- alt f g = Left \<$\> f 'Control.Applicative.<|>' Right \<$\> g
+-- @
+--
+-- From this, you might expect 'SemisumProfunctor' to contain an
+-- analogue to @('Control.Applicative.<|>')@ like this:
+--
+-- @
+-- (\<|||!\>) :: 'SemisumProfunctor' p => p x a -> p x a -> p x a
+-- p \<|||!\> q = dimap _____ (either id id) $ p '+++!' q
+--                     ???
+-- @
+--
+-- The type of that hole is @x -> 'Either' x x@, and we cannot choose
+-- a sensible default. We also cannot introduce a typeclass like we
+-- did with 'diviseP', as this would require us to create a strange
+-- comonoid class with 'Either' as the bifunctor:
+--
+-- @
+-- -- Yuck:
+-- class ComonoidE w where
+--   comappendE :: w -> Either w w
+--   comemptyE :: w -> 'Void'
+-- @
+--
+-- There are no @ComonoidE@ instances because we can never define a
+-- @comemptyE@: 'Void' is uninhabited. Even if we restrict ourselves
+-- to a @Cosemigroup@ class, it seems unlikely that it will have any
+-- useful instances, so we do not bother defining an
+-- 'Control.Applicative.Alternative'-style interface from a
+-- 'SemisumProfunctor'.
+class Profunctor p => SemisumProfunctor p where
+  (+++!) :: p a c -> p b d -> p (Either a b) (Either c d)
+  (+++!) p q = decideP id (rmap Left p) (rmap Right q)
+
+  -- | Analogue to @decide@ (from "semigroupoids") or
+  -- 'Data.Functor.Contravariant.Divisible.choose' (from
+  -- "contravariant").
+  decideP :: (a -> Either b c) -> p b x -> p c x -> p a x
+  decideP f p q = dimap f (either id id) $ p +++! q
+  {-# MINIMAL (+++!) | decideP #-}
+
+-- | Analogue to @decided@ (from "semigroupoids") or
+-- 'Data.Functor.Contravariant.Divisible.chosen' (from
+-- "contravariant").
+decidedP :: SemisumProfunctor p => p b x -> p c x -> p (Either b c) x
+decidedP = decideP id
+
+-- | 'SemisumProfunctor's with a unit.
+--
+-- You can often write these instances mechanically:
+--
+-- @
+-- instance SumProfunctor p where
+--   concludeP f = 'Data.Bifunctor.Flip.runFlip' $ conclude f -- If you have `instance Conclude ('Data.Bifunctor.Flip.Flip' P a)`
+--   concludeP f = 'Data.Bifunctor.Flip.runFlip' $ 'Data.Functor.Contravariant.Divisible.lose' f -- If you have `instance 'Data.Functor.Contravariant.Divisible.Decidable' ('Data.Bifunctor.Flip.Flip' P a)`
+-- @
+--
+-- Law: @voidP@ is an identity for @('+++!')@, up to @Either@
+-- rearrangement.
+class SemisumProfunctor p => SumProfunctor p where
+  -- | Unit for @('+++!')@.
+  voidP :: p Void Void
+  voidP = concludeP id
+
+  -- | Analogue to @conclude@ (from "semigroupoids") or
+  -- 'Data.Functor.Contravariant.Divisible.lose' (from
+  -- "contravariant").
   --
-  -- (You probably won't need to use this except to define
-  -- 'ProductProfunctor' instances.  In your own code @\<*\>@ should
-  -- be sufficient.)
-  (****) :: p a (b -> c) -> p a b -> p a c
-  (****) f x = Profunctor.dimap dup (uncurry ($)) (f ***! x)
-    where dup y = (y, y)
-
-  -- | Use @pure ()@ instead.  @empty@ may be deprecated in a future
-  -- version.
-  empty  :: p () ()
-  empty = purePP ()
-
-  -- | Use @\\f g -> (,) 'Control.Applicative.<$>'
-  -- 'Data.Profunctor.lmap' fst f 'Control.Applicative.<*>'
-  -- 'Data.Profunctor.lmap' snd g@ instead.
-  -- @(***!)@ may be deprecated in a future version.
-  (***!) :: p a b -> p a' b' -> p (a, a') (b, b')
-  f ***! g = (,) `Profunctor.rmap` Profunctor.lmap fst f
-                  **** Profunctor.lmap snd g
-
-class Profunctor p => SumProfunctor p where
-  -- Morally we should have 'zero :: p Void Void' but I don't think
-  -- that would actually be useful
-  (+++!) :: p a b -> p a' b' -> p (Either a a') (Either b b')
+  -- Unit for 'decideP'.
+  concludeP :: (a -> Void) -> p a x
+  concludeP f = dimap f absurd voidP
+  {-# MINIMAL voidP | concludeP #-}
+
+-- | Analogue to @concluded@ (from "semigroupoids") or
+-- 'Data.Functor.Contravariant.Divisible.lost'. Potentially more
+-- meaningful than 'concludeP', as it shows that we definitely cannot
+-- receive _anything_ on the input side.
+concludedP :: SumProfunctor p => p Void x
+concludedP = concludeP id
diff --git a/Data/Profunctor/Product/Default.hs b/Data/Profunctor/Product/Default.hs
index 776be6a7..20f0ffaa 100644
--- a/Data/Profunctor/Product/Default.hs
+++ b/Data/Profunctor/Product/Default.hs
@@ -49,7 +49,6 @@ module Data.Profunctor.Product.Default
 import Control.Applicative (Const (Const))
 import Data.Functor.Identity (Identity (Identity))
 import Data.Profunctor (Profunctor, dimap)
--- TODO: vv this imports a lot of names.  Should we list them all?
 import Data.Profunctor.Product
 import Data.Tagged (Tagged (Tagged))
 
diff --git a/Data/Profunctor/Product/Default/Class.hs b/Data/Profunctor/Product/Default/Class.hs
index edd7bb28..7ede3478 100644
--- a/Data/Profunctor/Product/Default/Class.hs
+++ b/Data/Profunctor/Product/Default/Class.hs
@@ -76,7 +76,7 @@ class GDefault p f g where
 
 instance ProductProfunctor p => GDefault p U1 U1 where
   type GDefCnstr p U1 U1 = ()
-  gdef1 = dimap (const ()) (const U1) empty
+  gdef1 = dimap (const ()) (const U1) unitP
 
 instance (Profunctor p, GDefault p f g) => GDefault p (M1 i c f) (M1 i c g) where
   type GDefCnstr p (M1 i c f) (M1 i c g) = GDefCnstr p f g
diff --git a/Data/Profunctor/Product/Examples.hs b/Data/Profunctor/Product/Examples.hs
index 3de2803a..590f0707 100644
--- a/Data/Profunctor/Product/Examples.hs
+++ b/Data/Profunctor/Product/Examples.hs
@@ -9,8 +9,7 @@ module Data.Profunctor.Product.Examples where
 import qualified Data.Profunctor                 as P
 import qualified Data.Profunctor.Product         as PP
 import qualified Data.Profunctor.Product.Default as D
-import           Control.Applicative             (Applicative, liftA2, pure, (<*>),
-                                                  ZipList(ZipList), getZipList)
+import           Control.Applicative             (liftA2, ZipList(..))
 
 newtype Replicator r f a b = Replicator (r -> f b)
   deriving Functor
@@ -48,10 +47,12 @@ instance Applicative f => Applicative (Replicator r f a) where
 instance Functor f => P.Profunctor (Replicator r f) where
   dimap _ h (Replicator f) = Replicator ((fmap . fmap) h f)
 
-instance Applicative f=> PP.ProductProfunctor (Replicator r f) where
-  purePP = pure
+instance Applicative f => PP.SemiproductProfunctor (Replicator r f) where
   (****) = (<*>)
 
+instance Applicative f => PP.ProductProfunctor (Replicator r f) where
+  pureP = pure
+
 -- In the real world this would be 'StateT [a] Maybe b' but I don't want to
 -- pick up the transformers dependency here
 newtype Take a z b = Take ([a] -> Maybe ([a], b))
@@ -93,10 +94,12 @@ instance Applicative (Take a z) where
 instance P.Profunctor (Take a) where
   dimap _ g (Take h) = Take ((fmap . fmap . fmap) g h)
 
-instance PP.ProductProfunctor (Take a) where
-  purePP = pure
+instance PP.SemiproductProfunctor (Take a) where
   (****) = (<*>)
 
+instance PP.ProductProfunctor (Take a) where
+  pureP = pure
+
 newtype Traverse f a b = Traverse { runTraverse :: a -> f b } deriving Functor
 
 -- | Use 'sequenceT' instead.  It has a better name.
@@ -132,10 +135,12 @@ instance Applicative f => Applicative (Traverse f a) where
 instance Functor f => P.Profunctor (Traverse f) where
   dimap g h (Traverse f) = Traverse (P.dimap g (fmap h) f)
 
-instance Applicative f => PP.ProductProfunctor (Traverse f) where
-  purePP = pure
+instance Applicative f => PP.SemiproductProfunctor (Traverse f) where
   (****) = (<*>)
 
+instance Applicative f => PP.ProductProfunctor (Traverse f) where
+  pureP = pure
+
 newtype Zipper a b = Zipper { unZipper :: Traverse ZipList a b }
   deriving Functor
 
@@ -151,10 +156,12 @@ instance Applicative (Zipper a) where
   pure = Zipper . pure
   f <*> x = Zipper ((<*>) (unZipper f) (unZipper x))
 
-instance PP.ProductProfunctor Zipper where
-  purePP = pure
+instance PP.SemiproductProfunctor Zipper where
   (****) = (<*>)
 
+instance PP.ProductProfunctor Zipper where
+  pureP = pure
+
 -- }
 
 -- | A challenge from a Clojurist on Hacker News
diff --git a/Data/Profunctor/Product/Internal/TH.hs b/Data/Profunctor/Product/Internal/TH.hs
index fac66997..981efdfa 100644
--- a/Data/Profunctor/Product/Internal/TH.hs
+++ b/Data/Profunctor/Product/Internal/TH.hs
@@ -21,7 +21,7 @@ import Language.Haskell.TH (Dec(DataD, SigD, FunD, InstanceD, NewtypeD),
 import Language.Haskell.TH.Datatype.TyVarBndr (TyVarBndr_, TyVarBndrSpec,
                                                plainTVSpecified, tvName)
 import Control.Monad ((<=<))
-import Control.Applicative (pure, liftA2, (<$>), (<*>))
+import Control.Applicative (liftA2)
 
 makeAdaptorAndInstanceI :: Bool -> Maybe String -> Name -> Q [Dec]
 makeAdaptorAndInstanceI inferrable adaptorNameM =
diff --git a/Data/Profunctor/Product/Tuples/TH.hs b/Data/Profunctor/Product/Tuples/TH.hs
index edbc73c1..bf3282d0 100644
--- a/Data/Profunctor/Product/Tuples/TH.hs
+++ b/Data/Profunctor/Product/Tuples/TH.hs
@@ -13,9 +13,8 @@ import Language.Haskell.TH
 import Language.Haskell.TH.Datatype.TyVarBndr
 
 import Data.Profunctor (Profunctor (dimap))
-import Data.Profunctor.Product.Class (ProductProfunctor, (***!), empty)
+import Data.Profunctor.Product.Class (ProductProfunctor, (***!), unitP)
 import Data.Profunctor.Product.Default.Class (Default (def))
-import Control.Applicative (pure)
 
 mkTs :: [Int] -> Q [Dec]
 mkTs = mapM mkT
@@ -61,7 +60,7 @@ pTn n = sequence [sig, fun]
                        `appT` foldl appT (conT tN) (map varT . take n $ bs)
     fun = funD (pT n) [ clause [] (normalB bdy) [] ]
     bdy = case n of
-      0 -> [| const empty |]
+      0 -> [| const unitP |]
       1 -> [| id |]
       2 -> [| uncurry (***!) |]
       _ -> [| chain $(varE (pT (n - 1))) |]
@@ -174,7 +173,7 @@ mkDefaultN n =
     mkTupT = foldl appT (tupleT n) . map varT
     mkFun = funD 'def [clause [] bdy []]
     bdy = normalB $ case n of
-      0 -> varE 'empty
+      0 -> [| unitP |]
       _ -> varE (mkName $ 'p':show n) `appE` tupE (replicate n [| def |])
     p = mkName "p"
     x = varT (mkName "x")