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:
Contravariant
?Contravariant
, but not Divisible
?Divisible
, but is not a Decidable
?Decidable
?(partial answer)
newtype F a = K (Bool -> a)
is not contravariant (it is, however, a covariant functor).
newtype F a = F { runF :: a -> Void }
is contravariant but it can not be Divisible
since otherwise
runF (conquer :: F ()) () :: Void
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.)
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
(partial derivative answer?)
I belive @chi is correct when they hypothesize that Const m
can't be a lawful Decidable
for all Monoid
s 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 Monoid
s—so Const m
could still be a lawful Decidable
if m
is a distributive monoid).
If you love us? You can donate to us via Paypal or buy me a coffee so we can maintain and grow! Thank you!
Donate Us With