Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Add Cochoice instances for Joker and Star #31

Open
wants to merge 1 commit into
base: master
Choose a base branch
from

Conversation

masaeedu
Copy link
Contributor

@masaeedu masaeedu commented Oct 8, 2019

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.

@masaeedu masaeedu changed the title Add cochoice instances for Joker and Star Add Cochoice instances for Joker and Star Oct 8, 2019
@LiamGoodacre
Copy link
Member

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
Copy link
Member

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

@masaeedu
Copy link
Contributor Author

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

@LiamGoodacre
Copy link
Member

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

@masaeedu
Copy link
Contributor Author

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

@hdgarrood
Copy link
Contributor

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
Copy link
Contributor Author

masaeedu commented Feb 20, 2020

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.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants