1{-# LANGUAGE CPP #-}
2{-# LANGUAGE TypeOperators #-}
3{-# OPTIONS_GHC -fno-warn-deprecations #-}
4
5-----------------------------------------------------------------------------
6-- |
7-- Module      :  Data.Functor.Contravariant.Divisible
8-- Copyright   :  (C) 2014-2015 Edward Kmett
9-- License     :  BSD-style (see the file LICENSE)
10--
11-- Maintainer  :  Edward Kmett <ekmett@gmail.com>
12-- Stability   :  provisional
13-- Portability :  portable
14--
15-- This module supplies contravariant analogues to the 'Applicative' and 'Alternative' classes.
16----------------------------------------------------------------------------
17module Data.Functor.Contravariant.Divisible
18  (
19  -- * Contravariant Applicative
20    Divisible(..), divided, conquered, liftD
21  -- * Contravariant Alternative
22  , Decidable(..), chosen, lost
23  -- * Mathematical definitions
24  -- ** Divisible
25  -- $divisible
26
27  -- *** A note on 'conquer'
28  -- $conquer
29
30  -- ** Decidable
31  -- $decidable
32  ) where
33
34import Control.Applicative
35import Control.Applicative.Backwards
36import Control.Arrow
37import Control.Monad.Trans.Error
38import Control.Monad.Trans.Except
39import Control.Monad.Trans.Identity
40import Control.Monad.Trans.List
41import Control.Monad.Trans.Maybe
42import qualified Control.Monad.Trans.RWS.Lazy as Lazy
43import qualified Control.Monad.Trans.RWS.Strict as Strict
44import Control.Monad.Trans.Reader
45import qualified Control.Monad.Trans.State.Lazy as Lazy
46import qualified Control.Monad.Trans.State.Strict as Strict
47import qualified Control.Monad.Trans.Writer.Lazy as Lazy
48import qualified Control.Monad.Trans.Writer.Strict as Strict
49
50import Data.Either
51import Data.Functor.Compose
52import Data.Functor.Constant
53import Data.Functor.Contravariant
54import Data.Functor.Product
55import Data.Functor.Reverse
56import Data.Void
57
58#if MIN_VERSION_base(4,8,0)
59import Data.Monoid (Alt(..))
60#else
61import Data.Monoid (Monoid(..))
62#endif
63
64#if MIN_VERSION_base(4,7,0) || defined(MIN_VERSION_tagged)
65import Data.Proxy
66#endif
67
68#ifdef MIN_VERSION_StateVar
69import Data.StateVar
70#endif
71
72#if __GLASGOW_HASKELL__ >= 702
73#define GHC_GENERICS
74import GHC.Generics
75#endif
76
77--------------------------------------------------------------------------------
78-- * Contravariant Applicative
79--------------------------------------------------------------------------------
80
81-- |
82--
83-- A 'Divisible' contravariant functor is the contravariant analogue of 'Applicative'.
84--
85-- Continuing the intuition that 'Contravariant' functors consume input, a 'Divisible'
86-- contravariant functor also has the ability to be composed "beside" another contravariant
87-- functor.
88--
89-- Serializers provide a good example of 'Divisible' contravariant functors. To begin
90-- let's start with the type of serializers for specific types:
91--
92-- @
93-- newtype Serializer a = Serializer { runSerializer :: a -> ByteString }
94-- @
95--
96-- This is a contravariant functor:
97--
98-- @
99-- instance Contravariant Serializer where
100--   contramap f s = Serializer (runSerializer s . f)
101-- @
102--
103-- That is, given a serializer for @a@ (@s :: Serializer a@), and a way to turn
104-- @b@s into @a@s (a mapping @f :: b -> a@), we have a serializer for @b@:
105-- @contramap f s :: Serializer b@.
106--
107-- Divisible gives us a way to combine two serializers that focus on different
108-- parts of a structure. If we postulate the existance of two primitive
109-- serializers - @string :: Serializer String@ and @int :: Serializer Int@, we
110-- would like to be able to combine these into a serializer for pairs of
111-- @String@s and @Int@s. How can we do this? Simply run both serializers and
112-- combine their output!
113--
114-- @
115-- data StringAndInt = StringAndInt String Int
116--
117-- stringAndInt :: Serializer StringAndInt
118-- stringAndInt = Serializer $ \\(StringAndInt s i) ->
119--   let sBytes = runSerializer string s
120--       iBytes = runSerializer int i
121--   in sBytes <> iBytes
122-- @
123--
124-- 'divide' is a generalization by also taking a 'contramap' like function to
125-- split any @a@ into a pair. This conveniently allows you to target fields of
126-- a record, for instance, by extracting the values under two fields and
127-- combining them into a tuple.
128--
129-- To complete the example, here is how to write @stringAndInt@ using a
130-- @Divisible@ instance:
131--
132-- @
133-- instance Divisible Serializer where
134--   conquer = Serializer (const mempty)
135--
136--   divide toBC bSerializer cSerializer = Serializer $ \\a ->
137--     case toBC a of
138--       (b, c) ->
139--         let bBytes = runSerializer bSerializer b
140--             cBytes = runSerializer cSerializer c
141--         in bBytes <> cBytes
142--
143-- stringAndInt :: Serializer StringAndInt
144-- stringAndInt =
145--   divide (\\(StringAndInt s i) -> (s, i)) string int
146-- @
147--
148class Contravariant f => Divisible f where
149  --- | If one can handle split `a` into `(b, c)`, as well as handle `b`s and `c`s, then one can handle `a`s
150  divide  :: (a -> (b, c)) -> f b -> f c -> f a
151
152  -- | Conquer acts as an identity for combining @Divisible@ functors.
153  conquer :: f a
154
155-- |
156-- @
157-- 'divided' = 'divide' 'id'
158-- @
159divided :: Divisible f => f a -> f b -> f (a, b)
160divided = divide id
161
162-- | Redundant, but provided for symmetry.
163--
164-- @
165-- 'conquered' = 'conquer'
166-- @
167conquered :: Divisible f => f ()
168conquered = conquer
169
170-- |
171-- This is the divisible analogue of 'liftA'. It gives a viable default definition for 'contramap' in terms
172-- of the members of 'Divisible'.
173--
174-- @
175-- 'liftD' f = 'divide' ((,) () . f) 'conquer'
176-- @
177liftD :: Divisible f => (a -> b) -> f b -> f a
178liftD f = divide ((,) () . f) conquer
179
180instance Monoid r => Divisible (Op r) where
181  divide f (Op g) (Op h) = Op $ \a -> case f a of
182    (b, c) -> g b `mappend` h c
183  conquer = Op $ const mempty
184
185instance Divisible Comparison where
186  divide f (Comparison g) (Comparison h) = Comparison $ \a b -> case f a of
187    (a',a'') -> case f b of
188      (b',b'') -> g a' b' `mappend` h a'' b''
189  conquer = Comparison $ \_ _ -> EQ
190
191instance Divisible Equivalence where
192  divide f (Equivalence g) (Equivalence h) = Equivalence $ \a b -> case f a of
193    (a',a'') -> case f b of
194      (b',b'') -> g a' b' && h a'' b''
195  conquer = Equivalence $ \_ _ -> True
196
197instance Divisible Predicate where
198  divide f (Predicate g) (Predicate h) = Predicate $ \a -> case f a of
199    (b, c) -> g b && h c
200  conquer = Predicate $ const True
201
202instance Monoid m => Divisible (Const m) where
203  divide _ (Const a) (Const b) = Const (mappend a b)
204  conquer = Const mempty
205
206#if MIN_VERSION_base(4,8,0)
207instance Divisible f => Divisible (Alt f) where
208  divide f (Alt l) (Alt r) = Alt $ divide f l r
209  conquer = Alt conquer
210#endif
211
212#ifdef GHC_GENERICS
213instance Divisible U1 where
214  divide _ U1 U1 = U1
215  conquer = U1
216
217instance Divisible f => Divisible (Rec1 f) where
218  divide f (Rec1 l) (Rec1 r) = Rec1 $ divide f l r
219  conquer = Rec1 conquer
220
221instance Divisible f => Divisible (M1 i c f) where
222  divide f (M1 l) (M1 r) = M1 $ divide f l r
223  conquer = M1 conquer
224
225instance (Divisible f, Divisible g) => Divisible (f :*: g) where
226  divide f (l1 :*: r1) (l2 :*: r2) = divide f l1 l2 :*: divide f r1 r2
227  conquer = conquer :*: conquer
228
229instance (Applicative f, Divisible g) => Divisible (f :.: g) where
230  divide f (Comp1 l) (Comp1 r) = Comp1 (divide f <$> l <*> r)
231  conquer = Comp1 $ pure conquer
232#endif
233
234instance Divisible f => Divisible (Backwards f) where
235  divide f (Backwards l) (Backwards r) = Backwards $ divide f l r
236  conquer = Backwards conquer
237
238instance Divisible m => Divisible (ErrorT e m) where
239  divide f (ErrorT l) (ErrorT r) = ErrorT $ divide (funzip . fmap f) l r
240  conquer = ErrorT conquer
241
242instance Divisible m => Divisible (ExceptT e m) where
243  divide f (ExceptT l) (ExceptT r) = ExceptT $ divide (funzip . fmap f) l r
244  conquer = ExceptT conquer
245
246instance Divisible f => Divisible (IdentityT f) where
247  divide f (IdentityT l) (IdentityT r) = IdentityT $ divide f l r
248  conquer = IdentityT conquer
249
250instance Divisible m => Divisible (ListT m) where
251  divide f (ListT l) (ListT r) = ListT $ divide (funzip . map f) l r
252  conquer = ListT conquer
253
254instance Divisible m => Divisible (MaybeT m) where
255  divide f (MaybeT l) (MaybeT r) = MaybeT $ divide (funzip . fmap f) l r
256  conquer = MaybeT conquer
257
258instance Divisible m => Divisible (ReaderT r m) where
259  divide abc (ReaderT rmb) (ReaderT rmc) = ReaderT $ \r -> divide abc (rmb r) (rmc r)
260  conquer = ReaderT $ \_ -> conquer
261
262instance Divisible m => Divisible (Lazy.RWST r w s m) where
263  divide abc (Lazy.RWST rsmb) (Lazy.RWST rsmc) = Lazy.RWST $ \r s ->
264    divide (\ ~(a, s', w) -> case abc a of
265                                  ~(b, c) -> ((b, s', w), (c, s', w)))
266           (rsmb r s) (rsmc r s)
267  conquer = Lazy.RWST $ \_ _ -> conquer
268
269instance Divisible m => Divisible (Strict.RWST r w s m) where
270  divide abc (Strict.RWST rsmb) (Strict.RWST rsmc) = Strict.RWST $ \r s ->
271    divide (\(a, s', w) -> case abc a of
272                                (b, c) -> ((b, s', w), (c, s', w)))
273           (rsmb r s) (rsmc r s)
274  conquer = Strict.RWST $ \_ _ -> conquer
275
276instance Divisible m => Divisible (Lazy.StateT s m) where
277  divide f (Lazy.StateT l) (Lazy.StateT r) = Lazy.StateT $ \s ->
278    divide (lazyFanout f) (l s) (r s)
279  conquer = Lazy.StateT $ \_ -> conquer
280
281instance Divisible m => Divisible (Strict.StateT s m) where
282  divide f (Strict.StateT l) (Strict.StateT r) = Strict.StateT $ \s ->
283    divide (strictFanout f) (l s) (r s)
284  conquer = Strict.StateT $ \_ -> conquer
285
286instance Divisible m => Divisible (Lazy.WriterT w m) where
287  divide f (Lazy.WriterT l) (Lazy.WriterT r) = Lazy.WriterT $
288    divide (lazyFanout f) l r
289  conquer = Lazy.WriterT conquer
290
291instance Divisible m => Divisible (Strict.WriterT w m) where
292  divide f (Strict.WriterT l) (Strict.WriterT r) = Strict.WriterT $
293    divide (strictFanout f) l r
294  conquer = Strict.WriterT conquer
295
296instance (Applicative f, Divisible g) => Divisible (Compose f g) where
297  divide f (Compose l) (Compose r) = Compose (divide f <$> l <*> r)
298  conquer = Compose $ pure conquer
299
300instance Monoid m => Divisible (Constant m) where
301  divide _ (Constant l) (Constant r) = Constant $ mappend l r
302  conquer = Constant mempty
303
304instance (Divisible f, Divisible g) => Divisible (Product f g) where
305  divide f (Pair l1 r1) (Pair l2 r2) = Pair (divide f l1 l2) (divide f r1 r2)
306  conquer = Pair conquer conquer
307
308instance Divisible f => Divisible (Reverse f) where
309  divide f (Reverse l) (Reverse r) = Reverse $ divide f l r
310  conquer = Reverse conquer
311
312#if MIN_VERSION_base(4,7,0) || defined(MIN_VERSION_tagged)
313instance Divisible Proxy where
314  divide _ Proxy Proxy = Proxy
315  conquer = Proxy
316#endif
317
318#ifdef MIN_VERSION_StateVar
319instance Divisible SettableStateVar where
320  divide k (SettableStateVar l) (SettableStateVar r) = SettableStateVar $ \ a -> case k a of
321    (b, c) -> l b >> r c
322  conquer = SettableStateVar $ \_ -> return ()
323#endif
324
325lazyFanout :: (a -> (b, c)) -> (a, s) -> ((b, s), (c, s))
326lazyFanout f ~(a, s) = case f a of
327  ~(b, c) -> ((b, s), (c, s))
328
329strictFanout :: (a -> (b, c)) -> (a, s) -> ((b, s), (c, s))
330strictFanout f (a, s) = case f a of
331  (b, c) -> ((b, s), (c, s))
332
333funzip :: Functor f => f (a, b) -> (f a, f b)
334funzip = fmap fst &&& fmap snd
335
336--------------------------------------------------------------------------------
337-- * Contravariant Alternative
338--------------------------------------------------------------------------------
339
340-- | A 'Decidable' contravariant functor is the contravariant analogue of 'Alternative'.
341--
342-- Noting the superclass constraint that @f@ must also be 'Divisible', a @Decidable@
343-- functor has the ability to "fan out" input, under the intuition that contravariant
344-- functors consume input.
345--
346-- In the discussion for @Divisible@, an example was demonstrated with @Serializer@s,
347-- that turn @a@s into @ByteString@s. @Divisible@ allowed us to serialize the /product/
348-- of multiple values by concatenation. By making our @Serializer@ also @Decidable@-
349-- we now have the ability to serialize the /sum/ of multiple values - for example
350-- different constructors in an ADT.
351--
352-- Consider serializing arbitrary identifiers that can be either @String@s or @Int@s:
353--
354-- @
355-- data Identifier = StringId String | IntId Int
356-- @
357--
358-- We know we have serializers for @String@s and @Int@s, but how do we combine them
359-- into a @Serializer@ for @Identifier@? Essentially, our @Serializer@ needs to
360-- scrutinise the incoming value and choose how to serialize it:
361--
362-- @
363-- identifier :: Serializer Identifier
364-- identifier = Serializer $ \\identifier ->
365--   case identifier of
366--     StringId s -> runSerializer string s
367--     IntId i -> runSerializer int i
368-- @
369--
370-- It is exactly this notion of choice that @Decidable@ encodes. Hence if we add
371-- an instance of @Decidable@ for @Serializer@...
372--
373-- @
374-- instance Decidable Serializer where
375--   lose f = Serializer $ \\a -> absurd (f a)
376--   choose split l r = Serializer $ \\a ->
377--     either (runSerializer l) (runSerializer r) (split a)
378-- @
379--
380-- Then our @identifier@ @Serializer@ is
381--
382-- @
383-- identifier :: Serializer Identifier
384-- identifier = choose toEither string int where
385--   toEither (StringId s) = Left s
386--   toEither (IntId i) = Right i
387-- @
388class Divisible f => Decidable f where
389  -- | Acts as identity to 'choose'.
390  lose :: (a -> Void) -> f a
391
392  choose :: (a -> Either b c) -> f b -> f c -> f a
393
394-- |
395-- @
396-- 'lost' = 'lose' 'id'
397-- @
398lost :: Decidable f => f Void
399lost = lose id
400
401-- |
402-- @
403-- 'chosen' = 'choose' 'id'
404-- @
405chosen :: Decidable f => f b -> f c -> f (Either b c)
406chosen = choose id
407
408instance Decidable Comparison where
409  lose f = Comparison $ \a _ -> absurd (f a)
410  choose f (Comparison g) (Comparison h) = Comparison $ \a b -> case f a of
411    Left c -> case f b of
412      Left d -> g c d
413      Right{} -> LT
414    Right c -> case f b of
415      Left{} -> GT
416      Right d -> h c d
417
418instance Decidable Equivalence where
419  lose f = Equivalence $ \a -> absurd (f a)
420  choose f (Equivalence g) (Equivalence h) = Equivalence $ \a b -> case f a of
421    Left c -> case f b of
422      Left d -> g c d
423      Right{} -> False
424    Right c -> case f b of
425      Left{} -> False
426      Right d -> h c d
427
428instance Decidable Predicate where
429  lose f = Predicate $ \a -> absurd (f a)
430  choose f (Predicate g) (Predicate h) = Predicate $ either g h . f
431
432instance Monoid r => Decidable (Op r) where
433  lose f = Op $ absurd . f
434  choose f (Op g) (Op h) = Op $ either g h . f
435
436#if MIN_VERSION_base(4,8,0)
437instance Decidable f => Decidable (Alt f) where
438  lose = Alt . lose
439  choose f (Alt l) (Alt r) = Alt $ choose f l r
440#endif
441
442#ifdef GHC_GENERICS
443instance Decidable U1 where
444  lose _ = U1
445  choose _ U1 U1 = U1
446
447instance Decidable f => Decidable (Rec1 f) where
448  lose = Rec1 . lose
449  choose f (Rec1 l) (Rec1 r) = Rec1 $ choose f l r
450
451instance Decidable f => Decidable (M1 i c f) where
452  lose = M1 . lose
453  choose f (M1 l) (M1 r) = M1 $ choose f l r
454
455instance (Decidable f, Decidable g) => Decidable (f :*: g) where
456  lose f = lose f :*: lose f
457  choose f (l1 :*: r1) (l2 :*: r2) = choose f l1 l2 :*: choose f r1 r2
458
459instance (Applicative f, Decidable g) => Decidable (f :.: g) where
460  lose = Comp1 . pure . lose
461  choose f (Comp1 l) (Comp1 r) = Comp1 (choose f <$> l <*> r)
462#endif
463
464instance Decidable f => Decidable (Backwards f) where
465  lose = Backwards . lose
466  choose f (Backwards l) (Backwards r) = Backwards $ choose f l r
467
468instance Decidable f => Decidable (IdentityT f) where
469  lose = IdentityT . lose
470  choose f (IdentityT l) (IdentityT r) = IdentityT $ choose f l r
471
472instance Decidable m => Decidable (ReaderT r m) where
473  lose f = ReaderT $ \_ -> lose f
474  choose abc (ReaderT rmb) (ReaderT rmc) = ReaderT $ \r -> choose abc (rmb r) (rmc r)
475
476instance Decidable m => Decidable (Lazy.RWST r w s m) where
477  lose f = Lazy.RWST $ \_ _ -> contramap (\ ~(a, _, _) -> a) (lose f)
478  choose abc (Lazy.RWST rsmb) (Lazy.RWST rsmc) = Lazy.RWST $ \r s ->
479    choose (\ ~(a, s', w) -> either (Left  . betuple3 s' w)
480                                    (Right . betuple3 s' w)
481                                    (abc a))
482           (rsmb r s) (rsmc r s)
483
484instance Decidable m => Decidable (Strict.RWST r w s m) where
485  lose f = Strict.RWST $ \_ _ -> contramap (\(a, _, _) -> a) (lose f)
486  choose abc (Strict.RWST rsmb) (Strict.RWST rsmc) = Strict.RWST $ \r s ->
487    choose (\(a, s', w) -> either (Left  . betuple3 s' w)
488                                  (Right . betuple3 s' w)
489                                  (abc a))
490           (rsmb r s) (rsmc r s)
491
492instance Divisible m => Decidable (ListT m) where
493  lose _ = ListT conquer
494  choose f (ListT l) (ListT r) = ListT $ divide ((lefts &&& rights) . map f) l r
495
496instance Divisible m => Decidable (MaybeT m) where
497  lose _ = MaybeT conquer
498  choose f (MaybeT l) (MaybeT r) = MaybeT $
499    divide ( maybe (Nothing, Nothing)
500                   (either (\b -> (Just b, Nothing))
501                           (\c -> (Nothing, Just c)))
502           . fmap f) l r
503
504instance Decidable m => Decidable (Lazy.StateT s m) where
505  lose f = Lazy.StateT $ \_ -> contramap lazyFst (lose f)
506  choose f (Lazy.StateT l) (Lazy.StateT r) = Lazy.StateT $ \s ->
507    choose (\ ~(a, s') -> either (Left . betuple s') (Right . betuple s') (f a))
508           (l s) (r s)
509
510instance Decidable m => Decidable (Strict.StateT s m) where
511  lose f = Strict.StateT $ \_ -> contramap fst (lose f)
512  choose f (Strict.StateT l) (Strict.StateT r) = Strict.StateT $ \s ->
513    choose (\(a, s') -> either (Left . betuple s') (Right . betuple s') (f a))
514           (l s) (r s)
515
516instance Decidable m => Decidable (Lazy.WriterT w m) where
517  lose f = Lazy.WriterT $ contramap lazyFst (lose f)
518  choose f (Lazy.WriterT l) (Lazy.WriterT r) = Lazy.WriterT $
519    choose (\ ~(a, s') -> either (Left . betuple s') (Right . betuple s') (f a)) l r
520
521instance Decidable m => Decidable (Strict.WriterT w m) where
522  lose f = Strict.WriterT $ contramap fst (lose f)
523  choose f (Strict.WriterT l) (Strict.WriterT r) = Strict.WriterT $
524    choose (\(a, s') -> either (Left . betuple s') (Right . betuple s') (f a)) l r
525
526instance (Applicative f, Decidable g) => Decidable (Compose f g) where
527  lose = Compose . pure . lose
528  choose f (Compose l) (Compose r) = Compose (choose f <$> l <*> r)
529
530instance (Decidable f, Decidable g) => Decidable (Product f g) where
531  lose f = Pair (lose f) (lose f)
532  choose f (Pair l1 r1) (Pair l2 r2) = Pair (choose f l1 l2) (choose f r1 r2)
533
534instance Decidable f => Decidable (Reverse f) where
535  lose = Reverse . lose
536  choose f (Reverse l) (Reverse r) = Reverse $ choose f l r
537
538betuple :: s -> a -> (a, s)
539betuple s a = (a, s)
540
541betuple3 :: s -> w -> a -> (a, s, w)
542betuple3 s w a = (a, s, w)
543
544lazyFst :: (a, b) -> a
545lazyFst ~(a, _) = a
546
547#if MIN_VERSION_base(4,7,0) || defined(MIN_VERSION_tagged)
548instance Decidable Proxy where
549  lose _ = Proxy
550  choose _ Proxy Proxy = Proxy
551#endif
552
553#ifdef MIN_VERSION_StateVar
554instance Decidable SettableStateVar where
555  lose k = SettableStateVar (absurd . k)
556  choose k (SettableStateVar l) (SettableStateVar r) = SettableStateVar $ \ a -> case k a of
557    Left b -> l b
558    Right c -> r c
559#endif
560
561-- $divisible
562--
563-- In denser jargon, a 'Divisible' contravariant functor is a monoid object in the category
564-- of presheaves from Hask to Hask, equipped with Day convolution mapping the Cartesian
565-- product of the source to the Cartesian product of the target.
566--
567-- By way of contrast, an 'Applicative' functor can be viewed as a monoid object in the
568-- category of copresheaves from Hask to Hask, equipped with Day convolution mapping the
569-- Cartesian product of the source to the Cartesian product of the target.
570--
571-- Given the canonical diagonal morphism:
572--
573-- @
574-- delta a = (a,a)
575-- @
576--
577-- @'divide' 'delta'@ should be associative with 'conquer' as a unit
578--
579-- @
580-- 'divide' 'delta' m 'conquer' = m
581-- 'divide' 'delta' 'conquer' m = m
582-- 'divide' 'delta' ('divide' 'delta' m n) o = 'divide' 'delta' m ('divide' 'delta' n o)
583-- @
584--
585-- With more general arguments you'll need to reassociate and project using the monoidal
586-- structure of the source category. (Here fst and snd are used in lieu of the more restricted
587-- lambda and rho, but this construction works with just a monoidal category.)
588--
589-- @
590-- 'divide' f m 'conquer' = 'contramap' ('fst' . f) m
591-- 'divide' f 'conquer' m = 'contramap' ('snd' . f) m
592-- 'divide' f ('divide' g m n) o = 'divide' f' m ('divide' 'id' n o) where
593--   f' a = let (bc, d) = f a; (b, c) = g bc in (b, (c, d))
594-- @
595
596-- $conquer
597-- The underlying theory would suggest that this should be:
598--
599-- @
600-- conquer :: (a -> ()) -> f a
601-- @
602--
603-- However, as we are working over a Cartesian category (Hask) and the Cartesian product, such an input
604-- morphism is uniquely determined to be @'const' 'mempty'@, so we elide it.
605
606-- $decidable
607--
608-- A 'Divisible' contravariant functor is a monoid object in the category of presheaves
609-- from Hask to Hask, equipped with Day convolution mapping the cartesian product of the
610-- source to the Cartesian product of the target.
611--
612-- @
613-- 'choose' 'Left' m ('lose' f)  = m
614-- 'choose' 'Right' ('lose' f) m = m
615-- 'choose' f ('choose' g m n) o = 'choose' f' m ('choose' 'id' n o) where
616--   f' = 'either' ('either' 'id' 'Left' . g) ('Right' . 'Right') . f
617-- @
618--
619-- In addition, we expect the same kind of distributive law as is satisfied by the usual
620-- covariant 'Alternative', w.r.t 'Applicative', which should be fully formulated and
621-- added here at some point!
622