Add Cochoice instances for Joker and Star

[masaeedu]

These should help with the long standing problem of how to make "failable" optics. If your profunctor supports a Cochoice instance, you can simply apply a Prism backwards to it.

This lets you "demote" e.g. a:

f :: MonadPlus m => Star m (Either a String) (Either a String)

to a:

f' :: MonadPlus m => Star m String String
f' = re _Right f

by running the _Right prism backwards.

[LiamGoodacre]

In profunctors they specify Traversable f => Cochoice (Star f).

I don't have the experience to know which instance makes more sense. Any thoughts @paf31?

[LiamGoodacre]

Oh they also comment it with -- NB: Another instance that's highly questionable aha

[masaeedu]

I wonder if that coincidentally works out to the same thing for stuff like [] or Maybe.

[LiamGoodacre]

I don't believe so. The questionable instance has the potential to loop forever.

[masaeedu]

Would some generative tests to ensure (probable) conformity with the laws help this along?

[hdgarrood]

Yes, but also I think proofs of law conformity, and/or justifications of why these instances are appropriate (as opposed to any other instances these types might permit) would be more persuasive.

[masaeedu]

I played around with this a little bit more today, and while unfortunately I didn't manage to find the proof of correctness we're looking for, I did manage to relate it to a more obviously lawful structure.

I believe the instances below are more correct than what I had before (although for the couple of concrete instantiations I've tried it actually doesn't behave differently):

class Functor f => Filterable f
  where
  partition :: f (Either a b) -> (f a, f b)
-- This represents an oplax monoidal functor, so the laws are analogous to those for @Apply@ expressed in terms of @zip :: (f a, f b) -> f (a, b)@
-- https://github.com/masaeedu/filterable for quickcheckable laws and more

instance Filterable m => Cochoice (Kleisli m)
  where
  unleft (Kleisli amb) = Kleisli $ fst . partition . amb . Left

instance (Filterable m) => Cochoice (Joker m)
  where
  unleft (Joker m) = Joker $ fst $ partition m

These two profunctors give rise to the following combinators for using coprisms:

whittle :: Filterable f => Coprism s t a b -> f b -> f t
whittle p f = runJoker $ p $ Joker $ f

speculate :: Filterable f => Coprism s t a b -> (a -> f b) -> s -> f t
speculate = dimap Kleisli runKleisli

Here are a few instances of Filterable that I know about:

instance Filterable []
  where
  partition [] = ([], [])
  partition (Left x : xs) = first (x :) $ partition xs
  partition (Right x : xs) = second (x :) $ partition xs

instance Filterable Maybe
  where
  partition Nothing = (Nothing, Nothing)
  partition (Just (Left a)) = (Just a, Nothing)
  partition (Just (Right b)) = (Nothing, Just b)

instance Ord k => Filterable (Map k)
  where
  partition = foldrWithKey (\k -> either (first . insert k) (second . insert k)) (empty, empty)

Here is what using everything together looks like: https://github.com/masaeedu/co-optics/blob/3f0e51cbc3bab9d94a86ead63352fe1a04f211c8/src/Main.hs

To prove this is correct I need to start from the assumption that partition is a valid (op)laxity between the Either and (,) monoidal structures, and derive that the unlefts expressed in terms of it are valid strengths for the relevant profunctors with respect to the Either monoidal structure. I'll try to find someone to help me with this tomorrow.