Copyright	(C) 2014-2015 Edward Kmett
License	BSD-style (see the file LICENSE)
Maintainer	Edward Kmett <ekmett@gmail.com>
Stability	provisional
Portability	portable
Safe Haskell	Safe
Language	Haskell98

Data.Functor.Contravariant.Divisible

Contents

Contravariant Applicative
Contravariant Alternative

Description

This module supplies contravariant analogues to the Applicative and Alternative classes.

Synopsis

Contravariant Applicative

class Contravariant f => Divisible f where Source

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))

Methods

divide :: (a -> (b, c)) -> f b -> f c -> f a Source

conquer :: f a Source

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.

Instances

Divisible U1 Source
Methods divide :: (a -> (b, c)) -> U1 b -> U1 c -> U1 a Source conquer :: U1 a Source
Divisible Equivalence Source
Methods divide :: (a -> (b, c)) -> Equivalence b -> Equivalence c -> Equivalence a Source conquer :: Equivalence a Source
Divisible Comparison Source
Methods divide :: (a -> (b, c)) -> Comparison b -> Comparison c -> Comparison a Source conquer :: Comparison a Source
Divisible Predicate Source
Methods divide :: (a -> (b, c)) -> Predicate b -> Predicate c -> Predicate a Source conquer :: Predicate a Source
Divisible f => Divisible (Rec1 f) Source
Methods divide :: (a -> (b, c)) -> Rec1 f b -> Rec1 f c -> Rec1 f a Source conquer :: Rec1 f a Source
Monoid m => Divisible (Const m) Source
Methods divide :: (a -> (b, c)) -> Const m b -> Const m c -> Const m a Source conquer :: Const m a Source
Divisible (Proxy *) Source
Methods divide :: (a -> (b, c)) -> Proxy * b -> Proxy * c -> Proxy * a Source conquer :: Proxy * a Source
Divisible f => Divisible (Reverse f) Source
Methods divide :: (a -> (b, c)) -> Reverse f b -> Reverse f c -> Reverse f a Source conquer :: Reverse f a Source
Divisible f => Divisible (Backwards f) Source
Methods divide :: (a -> (b, c)) -> Backwards f b -> Backwards f c -> Backwards f a Source conquer :: Backwards f a Source
Divisible m => Divisible (MaybeT m) Source
Methods divide :: (a -> (b, c)) -> MaybeT m b -> MaybeT m c -> MaybeT m a Source conquer :: MaybeT m a Source
Divisible m => Divisible (ListT m) Source
Methods divide :: (a -> (b, c)) -> ListT m b -> ListT m c -> ListT m a Source conquer :: ListT m a Source
Divisible f => Divisible (IdentityT f) Source
Methods divide :: (a -> (b, c)) -> IdentityT f b -> IdentityT f c -> IdentityT f a Source conquer :: IdentityT f a Source
Monoid m => Divisible (Constant m) Source
Methods divide :: (a -> (b, c)) -> Constant m b -> Constant m c -> Constant m a Source conquer :: Constant m a Source
Monoid r => Divisible (Op r) Source
Methods divide :: (a -> (b, c)) -> Op r b -> Op r c -> Op r a Source conquer :: Op r a Source
(Divisible f, Divisible g) => Divisible ((:*:) f g) Source
Methods divide :: (a -> (b, c)) -> (f :: g) b -> (f :: g) c -> (f :: g) a Source conquer :: (f :: g) a Source
(Applicative f, Divisible g) => Divisible ((:.:) f g) Source
Methods divide :: (a -> (b, c)) -> (f :.: g) b -> (f :.: g) c -> (f :.: g) a Source conquer :: (f :.: g) a Source
Divisible f => Divisible (Alt * f) Source
Methods divide :: (a -> (b, c)) -> Alt * f b -> Alt * f c -> Alt * f a Source conquer :: Alt * f a Source
(Divisible f, Divisible g) => Divisible (Product f g) Source
Methods divide :: (a -> (b, c)) -> Product f g b -> Product f g c -> Product f g a Source conquer :: Product f g a Source
(Applicative f, Divisible g) => Divisible (Compose f g) Source
Methods divide :: (a -> (b, c)) -> Compose f g b -> Compose f g c -> Compose f g a Source conquer :: Compose f g a Source
Divisible m => Divisible (WriterT w m) Source
Methods divide :: (a -> (b, c)) -> WriterT w m b -> WriterT w m c -> WriterT w m a Source conquer :: WriterT w m a Source
Divisible m => Divisible (WriterT w m) Source
Methods divide :: (a -> (b, c)) -> WriterT w m b -> WriterT w m c -> WriterT w m a Source conquer :: WriterT w m a Source
Divisible m => Divisible (ErrorT e m) Source
Methods divide :: (a -> (b, c)) -> ErrorT e m b -> ErrorT e m c -> ErrorT e m a Source conquer :: ErrorT e m a Source
Divisible m => Divisible (ExceptT e m) Source
Methods divide :: (a -> (b, c)) -> ExceptT e m b -> ExceptT e m c -> ExceptT e m a Source conquer :: ExceptT e m a Source
Divisible m => Divisible (StateT s m) Source
Methods divide :: (a -> (b, c)) -> StateT s m b -> StateT s m c -> StateT s m a Source conquer :: StateT s m a Source
Divisible m => Divisible (StateT s m) Source
Methods divide :: (a -> (b, c)) -> StateT s m b -> StateT s m c -> StateT s m a Source conquer :: StateT s m a Source
Divisible m => Divisible (ReaderT r m) Source
Methods divide :: (a -> (b, c)) -> ReaderT r m b -> ReaderT r m c -> ReaderT r m a Source conquer :: ReaderT r m a Source
(Divisible f, Applicative g) => Divisible (ComposeCF f g) Source
Methods divide :: (a -> (b, c)) -> ComposeCF f g b -> ComposeCF f g c -> ComposeCF f g a Source conquer :: ComposeCF f g a Source
(Applicative f, Divisible g) => Divisible (ComposeFC f g) Source
Methods divide :: (a -> (b, c)) -> ComposeFC f g b -> ComposeFC f g c -> ComposeFC f g a Source conquer :: ComposeFC f g a Source
Divisible f => Divisible (M1 i c f) Source
Methods divide :: (a -> (b, d)) -> M1 i c f b -> M1 i c f d -> M1 i c f a Source conquer :: M1 i c f a Source
Divisible m => Divisible (RWST r w s m) Source
Methods divide :: (a -> (b, c)) -> RWST r w s m b -> RWST r w s m c -> RWST r w s m a Source conquer :: RWST r w s m a Source
Divisible m => Divisible (RWST r w s m) Source
Methods divide :: (a -> (b, c)) -> RWST r w s m b -> RWST r w s m c -> RWST r w s m a Source conquer :: RWST r w s m a Source

divided :: Divisible f => f a -> f b -> f (a, b) Source

divided = divide id

conquered :: Divisible f => f () Source

Redundant, but provided for symmetry.

conquered = conquer

liftD :: Divisible f => (a -> b) -> f b -> f a Source

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

Contravariant Alternative

class Divisible f => Decidable f where Source

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!

Methods

lose :: (a -> Void) -> f a Source

The only way to win is not to play.

choose :: (a -> Either b c) -> f b -> f c -> f a Source

Instances

Decidable U1 Source
Methods lose :: (a -> Void) -> U1 a Source choose :: (a -> Either b c) -> U1 b -> U1 c -> U1 a Source
Decidable Equivalence Source
Methods lose :: (a -> Void) -> Equivalence a Source choose :: (a -> Either b c) -> Equivalence b -> Equivalence c -> Equivalence a Source
Decidable Comparison Source
Methods lose :: (a -> Void) -> Comparison a Source choose :: (a -> Either b c) -> Comparison b -> Comparison c -> Comparison a Source
Decidable Predicate Source
Methods lose :: (a -> Void) -> Predicate a Source choose :: (a -> Either b c) -> Predicate b -> Predicate c -> Predicate a Source
Decidable f => Decidable (Rec1 f) Source
Methods lose :: (a -> Void) -> Rec1 f a Source choose :: (a -> Either b c) -> Rec1 f b -> Rec1 f c -> Rec1 f a Source
Decidable (Proxy *) Source
Methods lose :: (a -> Void) -> Proxy * a Source choose :: (a -> Either b c) -> Proxy * b -> Proxy * c -> Proxy * a Source
Decidable f => Decidable (Reverse f) Source
Methods lose :: (a -> Void) -> Reverse f a Source choose :: (a -> Either b c) -> Reverse f b -> Reverse f c -> Reverse f a Source
Decidable f => Decidable (Backwards f) Source
Methods lose :: (a -> Void) -> Backwards f a Source choose :: (a -> Either b c) -> Backwards f b -> Backwards f c -> Backwards f a Source
Divisible m => Decidable (MaybeT m) Source
Methods lose :: (a -> Void) -> MaybeT m a Source choose :: (a -> Either b c) -> MaybeT m b -> MaybeT m c -> MaybeT m a Source
Divisible m => Decidable (ListT m) Source
Methods lose :: (a -> Void) -> ListT m a Source choose :: (a -> Either b c) -> ListT m b -> ListT m c -> ListT m a Source
Decidable f => Decidable (IdentityT f) Source
Methods lose :: (a -> Void) -> IdentityT f a Source choose :: (a -> Either b c) -> IdentityT f b -> IdentityT f c -> IdentityT f a Source
Monoid r => Decidable (Op r) Source
Methods lose :: (a -> Void) -> Op r a Source choose :: (a -> Either b c) -> Op r b -> Op r c -> Op r a Source
(Decidable f, Decidable g) => Decidable ((:*:) f g) Source
Methods lose :: (a -> Void) -> (f :: g) a Source choose :: (a -> Either b c) -> (f :: g) b -> (f :: g) c -> (f :: g) a Source
(Applicative f, Decidable g) => Decidable ((:.:) f g) Source
Methods lose :: (a -> Void) -> (f :.: g) a Source choose :: (a -> Either b c) -> (f :.: g) b -> (f :.: g) c -> (f :.: g) a Source
Decidable f => Decidable (Alt * f) Source
Methods lose :: (a -> Void) -> Alt * f a Source choose :: (a -> Either b c) -> Alt * f b -> Alt * f c -> Alt * f a Source
(Decidable f, Decidable g) => Decidable (Product f g) Source
Methods lose :: (a -> Void) -> Product f g a Source choose :: (a -> Either b c) -> Product f g b -> Product f g c -> Product f g a Source
(Applicative f, Decidable g) => Decidable (Compose f g) Source
Methods lose :: (a -> Void) -> Compose f g a Source choose :: (a -> Either b c) -> Compose f g b -> Compose f g c -> Compose f g a Source
Decidable m => Decidable (WriterT w m) Source
Methods lose :: (a -> Void) -> WriterT w m a Source choose :: (a -> Either b c) -> WriterT w m b -> WriterT w m c -> WriterT w m a Source
Decidable m => Decidable (WriterT w m) Source
Methods lose :: (a -> Void) -> WriterT w m a Source choose :: (a -> Either b c) -> WriterT w m b -> WriterT w m c -> WriterT w m a Source
Decidable m => Decidable (StateT s m) Source
Methods lose :: (a -> Void) -> StateT s m a Source choose :: (a -> Either b c) -> StateT s m b -> StateT s m c -> StateT s m a Source
Decidable m => Decidable (StateT s m) Source
Methods lose :: (a -> Void) -> StateT s m a Source choose :: (a -> Either b c) -> StateT s m b -> StateT s m c -> StateT s m a Source
Decidable m => Decidable (ReaderT r m) Source
Methods lose :: (a -> Void) -> ReaderT r m a Source choose :: (a -> Either b c) -> ReaderT r m b -> ReaderT r m c -> ReaderT r m a Source
(Applicative f, Decidable g) => Decidable (ComposeFC f g) Source
Methods lose :: (a -> Void) -> ComposeFC f g a Source choose :: (a -> Either b c) -> ComposeFC f g b -> ComposeFC f g c -> ComposeFC f g a Source
Decidable f => Decidable (M1 i c f) Source
Methods lose :: (a -> Void) -> M1 i c f a Source choose :: (a -> Either b d) -> M1 i c f b -> M1 i c f d -> M1 i c f a Source
Decidable m => Decidable (RWST r w s m) Source
Methods lose :: (a -> Void) -> RWST r w s m a Source choose :: (a -> Either b c) -> RWST r w s m b -> RWST r w s m c -> RWST r w s m a Source
Decidable m => Decidable (RWST r w s m) Source
Methods lose :: (a -> Void) -> RWST r w s m a Source choose :: (a -> Either b c) -> RWST r w s m b -> RWST r w s m c -> RWST r w s m a Source

chosen :: Decidable f => f b -> f c -> f (Either b c) Source

chosen = choose id

lost :: Decidable f => f Void Source

lost = lose id