Contravariant hierarchy

[subttle]

I think it makes more sense to have a more precise hierarchy for contravariant functors.

• Separate divide and conquer into two classes?
• Seperate lose and choose into two classes?
• Add class to handle These?
• What about analog for Selective functors?

I need to figure out some laws that should give better guidance. For now, here is some spit-balling. All names here are subject to change.

class (Contravariant f) ⇒ Losable f where
  emptied ∷ f Void
  emptied' ∷ (Decidable f) ⇒ f Void
  emptied' = lost
  -- `covacuous`?
  empty ∷ f a → f Void
  empty = contramap absurd

class (Decidable f) ⇒ RenameMe f where
  renameme ∷ (a → These b c) → f b → f c → f a

renamed ∷ (RenameMe f) ⇒ f b → f c → f (These b c)
renamed = renameme id

renamed' ∷ (RenameMe f) ⇒ f a → f a → f a
renamed' = renameme (\s → These s s)

[subttle]

Experiment:

class Alternative f ⇒ Combines f where
  one ∷ f (These a b) → f (a → c) → f (b → c) → f c
class Applicative f ⇒ Composes f where
  two ∷ f (These a b) → f (a → b) → f (b → c) → f c

class Alternative f ⇒ Selective' f where
  select' ∷ f (Either a b) → f (a → c) → f (b → c) → f c

[subttle]

Another experiment:

class (Contravariant f) ⇒ MaybeH f where
  maybeh ∷ (a → Maybe b) → f b → f a

instance MaybeH Predicate where
  -- FIXME not sure `False` is the correct default value here
  -- TODO compare with `Either () b` instance?
  -- TODO could also just require `Monoid b` and use `mempty` in place of `False`
  maybeh ∷ ∀ a b . (a → Maybe b) → Predicate b → Predicate a
{-
  maybeh h (Predicate pᵇ) = Predicate pᵃ
    where
      pᵃ ∷ a → Bool
      pᵃ = maybe False pᵇ . h
-}
  -- maybeh h (Predicate pᵇ) = Predicate (maybe False pᵇ . h)
  maybeh h (Predicate pᵇ) = h >$< Predicate (maybe False pᵇ)

[subttle]

And if that works, why stop there? See if something like the following makes sense.

data List a = Nil | Cons a (List a)
class (Contravariant f) ⇒ ListH f where
  listh ∷ (a → List b) → f b → f a

But should probably consider both foldr and unfoldr destructors.
And then would need to consider how that might play out:

instance ListH Predicate where
  listh ∷ ∀ a b . (a → List b) → Predicate b → Predicate a
  listh h (Predicate pᵇ) = Predicate pᵃ
    where
      pᵃ ∷ Predicate a
      -- pᵃ = Predicate (\a → null (filter pᵇ (h a))) -- not (any pᵇ (h a))
      pᵃ = Predicate (null . filter pᵇ . h) -- not . any pᵇ . h

listh ∷ ∀ a b . (a → List b) → Equivalence b → Equivalence a

implying something like ∷ List b → List b → Bool so maybe equivalence of lists by length? So then I would imagine ∷ List b → List b → Ordering would then be comparing lists by length?