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?

Eponymous

Note that most (i.e. all 'nontrivial') functors are not contravariant. – Dunnock

@AJFarmar Yeah, it's not that difficult to come up with the example of a data type which is not a Contravariant, but this also not the most interesting part of the question :) – Eponymous

newtype C a = C (a -> Int) is contravariant. – Frumenty

Decidable is actually the dual of Alternative, so perhaps in the spirit of the original question then Comonad should be included in our inquisition of hierarchy? – Accustomed

I really wish Divisible had a superclass with divide but not conquer, dual to Apply. – Dineric

This question is being discussed on Meta. – Lousewort

@Lousewort Interesting. My question received 4 downvotes today... English is not my native language, so if something can be improved in terms of wording to make the statement or question clear, I'm happy to accept any useful suggestions! But I don't think that the question should be closed. – Eponymous

Potential close voters: this question should not be closed, for the reasons discussed in my Meta answer. – Lousewort

@Eponymous "But I don't think that the question should be closed" -- Nor do I. Those votes, I believe, are mostly an artefact of the SO review system, which sometimes tricks people into developing strong opinions about questions they probably should refrain from passing judgement on. – Lousewort

@Accustomed The issue with including Comonad here is that it is not a subclass of Divisible. Its relationship with Monad is not the same as the one between Divisible and Alternative. (In a cursory way: (1a) A Monad is a monad in Hask; (1b) A Comonad is a monad in the dual category Hask^op, which we encode within Hask by flipping some arrows; (2a) An Applicative is a monoidal endofunctor in Hask; (2b) A Divisible is a monoidal functor from Hask^op to Hask, which we encode within Hask by flipping some arrows, but not quite in the same way.) – Lousewort

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

Hybridism

What are the laws for Divisible? The documentation only mentions that lose should be an identity for choose (what does this mean, exactly, given the extra function arguments?); should there also be some analog of associativity? – Lyonnais

@DanielWagner hackage.haskell.org/package/contravariant-1.5.1/docs/… has some more laws – Accustomed

I don't think Identity can be an instance of Contravariant – Bidentate

@Bidentate I don't know what I was thinking. Thanks. – Hybridism

I like your examples! @user11228628 has detailed explanation on why Const cannot be Decidable. I think the documentation for the contravariant package can benefit a lot from these examples :) – Eponymous

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

Eohippus

Thanks for the detailed explanation! Now it really makes sense why Const cannot be Decidable. – Eponymous

Const can be Decidable, just not for any monoid, but only for those that satisfy that law, ie left distributive monoids. – Teleology