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