Good examples of not a Contravariant/Contravariant/Divisible/Decidable?

Question

The Contravariant family of typeclasses represents standard and fundamental abstractions in the Haskell ecosystem:

class Contravariant f where
    contramap :: (a -> b) -> f b -> f a

class Contravariant f => Divisible f where
    conquer :: f a
    divide  :: (a -> (b, c)) -> f b -> f c -> f a

class Divisible f => Decidable f where
    lose   :: (a -> Void) -> f a
    choose :: (a -> Either b c) -> f b -> f c -> f a

However, it's not that easy to understand the concepts behind these typeclasses. I think it would help to understand these typeclasses better if you could see some counterexamples for them. So, in the spirit of Good examples of Not a Functor/Functor/Applicative/Monad?, I'm looking for contrasting examples of data types which satisfy the following requirements:

• A type constructor which is not a Contravariant?
• A type constructor which is a Contravariant, but not Divisible?
• A type constructor which is a Divisible, but is not a Decidable?
• A type constructor which is a Decidable?

Answer 1

(partial answer)

Not contravariant

newtype F a = K (Bool -> a)

is not contravariant (it is, however, a covariant functor).

Contravariant, but not divisible

newtype F a = F { runF :: a -> Void }

is contravariant but it can not be Divisible since otherwise

runF (conquer :: F ()) () :: Void

A note on "divisible but non decidable"

I don't have a reasonable example for a divisible which is not decidable. We can observe that such a counterexample must be such because it violates the laws, and not just the type signature. Indeed, if Divisible F holds,

instance Decidable F where
    lose _ = conquer
    choose _ _ _ = conquer

satisfies the type signatures of the methods.

In libraries we find Const m as a divisible, when m is a monoid.

instance Monoid m => Divisible (Const m) where
  divide _ (Const a) (Const b) = Const (mappend a b)
  conquer = Const mempty

Perhaps this can not be a lawful Decidable? (I'm unsure, it seems to satisfy the Decidable laws, but there's no Decidable (Const m) instance in the libraries.)

Decidable

Taken from the libraries:

newtype Predicate a = Predicate (a -> Bool)

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

instance Decidable Predicate where
  lose f = Predicate $ \a -> absurd (f a)
  choose f (Predicate g) (Predicate h) = Predicate $ either g h . f

Answer 2

(partial derivative answer?)

I belive @chi is correct when they hypothesize that Const m can't be a lawful Decidable for all Monoids m, but I'm basing that off of some speculation about the Decidable laws.

In the docs, we get this tantalizing hint at a Decidable law:

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!

What sort of distributive relationship should Decidable and Divisible have with each other? Well, Divisible has chosen, which builds a product-accepting thing out of element-accepting things, and Decidable has divided, which builds a sum-accepting thing out of element-accepting things. Since products distribute over sums, perhaps the law we're seeking relates f (a, Either b c) to f (Either (a, b) (a, c)), values of which can be constructed via a `divided` (b `chosen` c) and (a `divided` b) `chosen` (a `divided` c), respectively.

So I'll hypothesize that the missing Decidable law is something along the lines of

a `divided` (b `chosen` c) = contramap f ((a `divided` b) `chosen` (a `divided` c))
  where f (x, y) = bimap ((,) x) ((,) x) y

which is indeed satisfied for Predicate, Equivalence, and Op (the three Decidable instances I've taken the time to check, so far).

Now I believe the only instance you can have for instance Monoid m => Decidable (Const m) uses mempty for lose and mappend for choose; any other choices and then lose is no longer an identity for choose. This means that the above distributive law simplifies to

a `mappend` (b `mappend` c) = (a `mappend` b) `mappend` (a `mappend` c)

which is clearly bogus not true in an arbitrary Monoid (though, as Sjoerd Visscher observes, is true in some Monoids—so Const m could still be a lawful Decidable if m is a distributive monoid).