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