Add `Contraversable`

[masaeedu]

Hello there. I find it very nice to have an analog for Applicative for Contravariant functors. But it feels like something is missing; where are our nice Traversables?

It seems like there is room for a typeclass like this:

class Functor t => Contraversable t
  where
  {-# MINIMAL contraverse | consequence #-}
  contraverse :: Decidable f => (a -> f b) -> t a -> f (t b)
  consequence :: Decidable f => t (f a) -> f (t b)

A simple application is to note that finite products (e.g. Vec n) are Contraversable. Thus the consequence of a container-ful of Predicates conditions :: Vec n (Predicate a) is consequence conditions :: Predicate (Vec n a), a predicate that gives the conjunction of the result of each predicate in conditions. Similarly, a finite productful of flipped folds can be consequenced to a flipped fold over the product. etc. etc.

Would you be open to a PR that adds this typeclass?

[sofia-m-a]

Should it be rather

contraverse :: Divisible f => (a -> f b) -> t a -> f (t b)

etc?

[endgame]

Is this collect from distributive?

[endgame]

It is not.

But it is useful. A HKD-flavoured version might be worth proposing in one of the various HKD libraries, because it gives you a good story for using Divisible with records: https://discourse.haskell.org/t/hasql-inserting-many-values-that-arent-tuples/10799/4

A rank-1 version would be useful, as @masaeedu says, and also provide an intuition to help people reading about a HKD version.