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