module Data.Functor.Contravariant.Divisible ( -- * Contravariant Applicative Divisible(..), divided, conquered, liftD -- * Contravariant Alternative , Decidable(..), chosen, lost ) where import Data.Functor.Contravariant import Data.Monoid import Data.Void -------------------------------------------------------------------------------- -- * Contravariant Applicative -------------------------------------------------------------------------------- -- | -- -- A 'Divisible' contravariant functor is the contravariant analogue of 'Applicative'. -- -- In denser jargon, a 'Divisible' contravariant functor is a monoid object in the category -- of presheaves from Hask to Hask, equipped with Day convolution mapping the Cartesian -- product of the source to the Cartesian product of the target. -- -- By way of contrast, an 'Applicative' functor can be viewed as a monoid object in the -- category of copresheaves from Hask to Hask, equipped with Day convolution mapping the -- Cartesian product of the source to the Cartesian product of the target. -- -- Given the canonical diagonal morphism: -- -- @ -- delta a = (a,a) -- @ -- -- @'divide' 'delta'@ should be associative with 'conquer' as a unit -- -- @ -- 'divide' 'delta' m 'conquer' = m -- 'divide' 'delta' 'conquer' m = m -- 'divide' 'delta' ('divide' 'delta' m n) o = 'divide' 'delta' m ('divide' 'delta' n o) -- @ -- -- With more general arguments you'll need to reassociate and project using the monoidal -- structure of the source category. (Here fst and snd are used in lieu of the more restricted -- lambda and rho, but this construction works with just a monoidal category.) -- -- @ -- 'divide' f m 'conquer' = 'contramap' ('fst' . f) m -- 'divide' f 'conquer' m = 'contramap' ('snd' . f) m -- 'divide' f ('divide' g m n) o = 'divide' f' m ('divide' 'id' n o) where -- f' a = case f a of (bc,d) -> case g bc of (b,c) -> (a,(b,c)) -- @ class Contravariant f => Divisible f where divide :: (a -> (b, c)) -> f b -> f c -> f a -- | The underlying theory would suggest that this should be: -- -- @ -- conquer :: (a -> ()) -> f a -- @ -- -- However, as we are working over a Cartesian category (Hask) and the Cartesian product, such an input -- morphism is uniquely determined to be @'const' 'mempty'@, so we elide it. conquer :: f a -- | -- @ -- 'divided' = 'divide' 'id' -- @ divided :: Divisible f => f a -> f b -> f (a, b) divided = divide id -- | Redundant, but provided for symmetry. -- -- @ -- 'conquered' = 'conquer -- @ conquered :: Divisible f => f () conquered = conquer -- | -- This is the divisible analogue of 'liftA'. It gives a viable default definition for 'contramap' in terms -- of the members of 'Divisible'. -- -- @ -- 'liftD' f = 'divide' ((,) () . f) 'conquer' -- @ liftD :: Divisible f => (a -> b) -> f b -> f a liftD f = divide ((,) () . f) conquer instance Monoid r => Divisible (Op r) where divide f (Op g) (Op h) = Op \$ \a -> case f a of (b, c) -> g b `mappend` h c conquer = Op \$ const mempty instance Divisible Comparison where divide f (Comparison g) (Comparison h) = Comparison \$ \a b -> case f a of (a',a'') -> case f b of (b',b'') -> g a' b' `mappend` h a'' b'' conquer = Comparison \$ \_ _ -> EQ instance Divisible Equivalence where divide f (Equivalence g) (Equivalence h) = Equivalence \$ \a b -> case f a of (a',a'') -> case f b of (b',b'') -> g a' b' && h a'' b'' conquer = Equivalence \$ \_ _ -> True instance Divisible Predicate where divide f (Predicate g) (Predicate h) = Predicate \$ \a -> case f a of (b, c) -> g b && h c conquer = Predicate \$ const True -------------------------------------------------------------------------------- -- * Contravariant Alternative -------------------------------------------------------------------------------- -- | -- -- A 'Divisible' contravariant functor is a monoid object in the category of presheaves -- from Hask to Hask, equipped with Day convolution mapping the cartesian product of the -- source to the Cartesian product of the target. -- -- @ -- 'choose' Left m ('lose' f) = m -- 'choose' Right ('lose' f) m = m -- 'choose' f ('choose' g m n) o = 'divide' f' m ('divide' 'id' n o) where -- f' bcd = 'either' ('either' 'id' ('Right' . 'Left') . g) ('Right' . 'Right') . f -- @ -- -- In addition, we expect the same kind of distributive law as is satisfied by the usual -- covariant 'Alternative', w.r.t 'Applicative', which should be fully formulated and -- added here at some point! class Divisible f => Decidable f where -- | The only way to win is not to play. lose :: (a -> Void) -> f a choose :: (a -> Either b c) -> f b -> f c -> f a -- | -- @ -- 'lost' = 'lose' 'id' -- @ lost :: Decidable f => f Void lost = lose id -- | -- @ -- 'chosen' = 'choose' 'id' -- @ chosen :: Decidable f => f b -> f c -> f (Either b c) chosen = choose id instance Decidable Comparison where lose f = Comparison \$ \a _ -> absurd (f a) choose f (Comparison g) (Comparison h) = Comparison \$ \a b -> case f a of Left c -> case f b of Left d -> g c d Right{} -> LT Right c -> case f b of Left{} -> GT Right d -> h c d instance Decidable Equivalence where lose f = Equivalence \$ \a -> absurd (f a) choose f (Equivalence g) (Equivalence h) = Equivalence \$ \a b -> case f a of Left c -> case f b of Left d -> g c d Right{} -> False Right c -> case f b of Left{} -> False Right d -> h c d instance Decidable Predicate where lose f = Predicate \$ \a -> absurd (f a) choose f (Predicate g) (Predicate h) = Predicate \$ either g h . f instance Monoid r => Decidable (Op r) where lose f = Op \$ absurd . f choose f (Op g) (Op h) = Op \$ either g h . f