Documentation for decidable is actually documentation for divisible.

[mpickering]

The documentation for Decidable states that..

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.

But this is precisely the same as the documentation for Divisible. Maybe this is deliberate but I find it confused to be repeated verbatim here. It would be perhaps be useful to draw the analogue to Alternative explicitly in this section as well for those who didn't read the header of the module.

[tomjaguarpaw]

I just noticed this too. Surely it must be a mistake?

[echatav]

Divisible f is equivalent to (Contravariant f, forall x. Monoid (f x)). It is also equivalent to a monoid object enriched in the category of Contravariants with unit given by the terminal contravariant U and multiplication given by contravariant Day convolution.

data Day f g a = forall b c. Day (f b) (g c) (a -> (b, c))
data U a = U

Decidable is equivalent to a monoid object enriched in the category of Contravariants with unit given by the initial contravariant V and multiplication given by what me might call contravariant Night convolution. This is just Day convolution in the general sense but where the underlying monoidal category is Hask with monoidal unit given by Void and monoidal product given by Either, instead of () and (,).

data Night f g a = forall b c. Night (f b) (g c) (a -> Either b c)
newtype V a = V (a -> Void)

[echatav]

Ok, I haven't written out proofs but here's how Applicative, Alternative, Divisible and Decidable are with "monoids all the way down".

Consider the following types;

data Day f g a = forall b c. Day (b -> c -> a) (f b) (g c)
data CoDay f g a = forall b c. CoDay (a -> (b, c)) (f b) (g c)
data Night f g a = forall b c. Night (Either b c -> a) (f b) (g c)
data CoNight f g a = forall b c. CoNight (a -> Either b c) (f b) (g c)

As well as these ones.

data U a = U
newtype I a = I a
newtype V a = V (a -> Void)

Then we have Functor instances for Day f g, Night f g, I and U. And we have Contravariant instances for CoDay f g, CoNight f g, V and U.

We can define a class MonoidIn like so.

class MonoidIn prod unit f where
  eta :: unit x -> f x
  mu :: prod f f x -> f x

Claims

The following are equivalent:

• Applicative f
• (Functor f, MonoidIn Day I f)

The following are equivalent:

• Alternative f
• (Applicative f, forall x. Monoid (f x))
• (Applicative f, MonoidIn Night U f)

The following are equivalent:

• Divisible f
• (Contravariant f, forall x. Monoid (f x))
• (Contravariant f, MonoidIn CoDay U f)

The following are equivalent:

• Decidable f
• (Divisible f, MonoidIn CoNight V f)