Attempt to provide some intuition for contravariant and divisible

[ocharles]

There was recently confusion (and, as I read it, frustration) on Twitter regarding Contravariant and Divisible.

• Exhibit A - Will felt he had little more than a type signature to go on for Contravariant.

• Exhibit B - points out that 'Divisible' has nothing but a dense technical explanation. I posture that barely 1% of the people who use Haskell have even heard of a presheave, let alone understanding what the category Presheave even is.

I provided a few tweet replies, but this comes up time and time again. @tomjaguarpaw has explained 'Contravariant' once (https://ocharles.org.uk/blog/guest-posts/2013-12-21-24-days-of-hackage-contravariant.html), @phaazon spoke about divisible (https://phaazon.blogspot.co.uk/2015/08/contravariance-and-luminance-to-add.html), but I think it's about time we bought at least some of this into contravariant proper.

Yes, the examples do not do justice to what a Contravariant functor truly is, but I believe they provide at least a gentle ramp to begin wading towards the deep end. I will understand if you feel this is the wrong place for this documentation.

@jb55 this is written for you, so I'd appreciate knowing if it even helps. @acowley expressed not knowing what Divisible even was, so likewise feedback would be appreciated.

[tomjaguarpaw]

This is sorely needed.

[acowley]

Thanks so much for taking action on this @ocharles! I had forgotten about @phaazon’s blog post, and it really is an excellent example. If linking to such things from the docs is viewed as okay, I’d be in favor of doing so.

[Blaisorblade]

Thanks a lot for this! That's the sort of thing we need more of. If I may ask: do you also understand Decidable?

[jb55]

I haven't decided to dive into that yet but it looks more approachable 👍

[hadronized]

Feel free to use my blog post, of course! :)

^{_{I just re-read it, and found the comments below. Oh my. :D}}

[ekmett]

I have no particular objection to including links to blog posts about the topic.

[ocharles]

@Blaisorblade yes, I'll do Decidable too, if people feel this is useful. It's not much of a step up from Divisible.

[ocharles]

Ok, I've added an explanation for Decidable too, and addressed @phadej's point that my Divisible example doesn't actually show a use of divide.

[RyanGlScott]

This looks nice overall. I have one gripe in that these changes move the laws for Decidable and Divisible away from their Haddocks and sequesters them elsewhere. I'd prefer to keep the laws close to the classes themselves, although I don't care if they're accompanied by the current category theoretic jargon or not. I'd be OK with repeating the laws in the additional section you've added, but explained in further detail.

[ocharles]

Agree, I think the laws should be front and center. I'll try and move them

On Sun, 24 Sep 2017, 2:56 pm Ryan Scott notifications@github.com wrote:

This looks nice overall. I have one gripe in that these changes move the laws for Decidable and Divisible away from their Haddocks and sequesters them elsewhere. I'd prefer to keep the laws close to the classes themselves, although I don't care if they're accompanied by the current category theoretic jargon or not. I'd be OK with repeating the laws in the additional section you've added, but explained in further detail.

— You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub https://github.com/ekmett/contravariant/pull/33#issuecomment-331711704, or mute the thread https://github.com/notifications/unsubscribe-auth/AABRjhUvIaeMfjxZWZwAF3FWb29z00Bwks5sll9WgaJpZM4Pdxy0 .

[mitchellwrosen]

Is this still being worked on? If so, there's a pattern I've used in the past to make Divisible feel more like Applicative that might be worth mentioning in some sort of tutorial. I'm not sure.

-- Right fixity, higher than >$<
infixr 5 >*<
(>*<) :: Divisible f => f a -> f b -> f (a, b)
(>*<) = divided

Here's how you use it:

data Person = Person
  { name :: String
  , age :: Int
  , living :: Bool
  }

longName :: Predicate String
longName = Predicate (\name -> length name > 8)

old :: Predicate Int
old = Predicate (\age -> age > 60)

alive :: Predicate Bool
alive = Predicate id

oldAndAliveWithLongName :: Predicate Person
oldAndAliveWithLongName =
  (\p -> (name p, (age p, living p)))
    >$< longName
    >*< old
    >*< alive

[tomjaguarpaw]

@mitchellwrosen I have to say I don't like that at all. Why not

(<||>) :: Divisible f => f a -> f a -> f a
(<||>) = divide (\x -> (x, x))

oldAndAliveWithLongName :: Predicate Person
oldAndAliveWithLongName = contramap name longName
                     <||> contramap age old
                     <||> contramap living alive

[Not type checked!]

[jb55]

@tomjaguarpaw yours is cleaner, @mitchellwrosen's fits the Applicative analogy a bit better from a learning perspective

[tomjaguarpaw]

It only feels like Applicative until you actually try to use it, at which point you notice you can never get rid of the tuple nesting because they type parameter is contravariant. Then it becomes too painful to use.

[mitchellwrosen]

That's a good operator too, but it looks more like <> for the Monoid that every Divisible gives rise to, so I don't think it needs its own name.

mempty = conquer
mappend = divide (\x -> (x, x))

(except that Predicate isn't a Semigroup/Monoid right now)

[phadej]

For Predicate, deriving via a -> All or a -> Any instances also makes sense. So it's not an easy choice.

EDIT or will they boil down to the same instance?

[mitchellwrosen]

Wouldn't the more natural/obvious Monoid instance correspond to a -> All, per how Predicate's Divisible instance works?

[tomjaguarpaw]

Maybe, but that's just shifting the observation to "there are two choices of Divisible instance"!

[mitchellwrosen]

Of course, but it's odd to mix-and-match the two, no? Anywho, I feel like I am spamming this issue unnecessarily :) Thanks for the discussion!

On Oct 17, 2017 6:13 PM, "tomjaguarpaw" notifications@github.com wrote:

Maybe, but that's just shifting the observation to "there are two choices of Divisible instance"!

— You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub https://github.com/ekmett/contravariant/pull/33#issuecomment-337389718, or mute the thread https://github.com/notifications/unsubscribe-auth/ABBlpvloNxFvyZSVDM52kUGCAoTOXby7ks5stSZxgaJpZM4Pdxy0 .

[ocharles]

Yes, this is being worked on, but the scope of this PR is to just improve documentation. All I need to do is add the laws, and I'm done. I'll happily take a patch from anyone else adding those laws, too.

[ekmett]

I'd say the Monoid for any of these should match up with the conquer and divide delta if they are missing. This corresponds exactly to what you'd derive if you used (a -> All) and (a -> a -> All) and (a -> a -> Ordering), etc. I'm actually surprised I didn't add them.

[ekmett]

Ah, we're just missing the Predicate one. Adding it. (Off topic digression ends)

[ekmett]

Merged what you have. We can do more intensive edits as we go.

[ekmett]

@ocharles you have commit access to the repo now, feel free to push further updates directly.

[jb55]

Thanks guys!

[hadronized]

\o/