contravariant
contravariant copied to clipboard
Documentation for decidable is actually documentation for divisible.
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.
I just noticed this too. Surely it must be a mistake?
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 Contravariant
s 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 Contravariant
s 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)
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)