Attempt to provide some intuition for contravariant and divisible #33

ocharles · 2017-09-20T12:17:55Z

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.

sjoerdvisscher · 2017-09-20T12:25:48Z

src/Data/Functor/Contravariant/Divisible.hs

-- category of copresheaves from Hask to Hask, equipped with Day convolution mapping the
-- Cartesian product of the source to the Cartesian product of the target.
+-- Continuing the intuition that 'Contravariant' functors consume input, a 'Divisible'
+-- contravariant functor also has the ability to composed "beside" another contravariant


'the ability to be composed' I think?

Yep, thanks!

phadej · 2017-09-20T12:31:23Z

src/Data/Functor/Contravariant/Divisible.hs

+-- 'divide' is a generalization by also taking a 'contramap' like function to
+-- split any @a@ into a pair. This conveniently allows you to target fields of
+-- a record, for instance, by extracting the values under two fields and
+-- combining them into a tuple.


this lacks an example, so can I write serializeStringAndInt using divide, how?

phadej · 2017-09-20T12:35:25Z

src/Data/Functor/Contravariant.hs

+-- on a persons bank balance to work out if they are currently overdrawn:
+--
+-- @
+-- newtype Predicate a = Predicate (a -> Bool)


I'd define it as in the module

phadej

Looks good. Could you add links in @@ sections around contramap Contravariant etc.

tomjaguarpaw · 2017-09-20T12:44:44Z

This is sorely needed.

acowley · 2017-09-20T12:50:53Z

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.

VitorCBSB · 2017-09-20T13:03:54Z

src/Data/Functor/Contravariant.hs

+--
+-- As an example, consider the type of predicate functions  @a -> Bool@. One
+-- such predicate might be @negative x = x < 0@, which
+-- classisifies integers as to whether they are negative. However, given this


Classifies, I think?

jb55 · 2017-09-20T16:37:30Z

src/Data/Functor/Contravariant/Divisible.hs

-- structure of the source category. (Here fst and snd are used in lieu of the more restricted
-- lambda and rho, but this construction works with just a monoidal category.)
+-- That is, given a serializer for @a@ (@s :: Serializer a@), and a way to turn
+-- @b@s into @a@s (a mapping @f :: b -> a@), we have a serializer for @b@:


This sentence is what made it click for me, the only difficulty I had when reading this was that a and b are reversed compared to the type signature of contramap.

Specifically, this is what made Contravariant click for me. 👍

Blaisorblade · 2017-09-20T22:47:57Z

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 · 2017-09-20T23:16:58Z

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

hadronized · 2017-09-20T23:20:04Z

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

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

ekmett · 2017-09-21T07:21:30Z

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

ocharles · 2017-09-21T10:27:32Z

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

ocharles · 2017-09-21T12:05:07Z

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.

phadej · 2017-09-21T12:19:07Z

src/Data/Functor/Contravariant/Divisible.hs

+--             iBytes = runSerializer serializeB b
+--         in sBytes <> iBytes
+--
+-- stringAndInt :: Serializer (String, Int)


StringAndInt

Thanks, type checker!

RyanGlScott · 2017-09-24T13:55:34Z

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 · 2017-09-24T14:02:15Z

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 ***@***.***> 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 <#33 (comment)>, or mute the thread <https://github.com/notifications/unsubscribe-auth/AABRjhUvIaeMfjxZWZwAF3FWb29z00Bwks5sll9WgaJpZM4Pdxy0> .

mitchellwrosen · 2017-10-17T17:34:46Z

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 · 2017-10-17T18:12:52Z

@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 · 2017-10-17T19:18:12Z

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

tomjaguarpaw · 2017-10-17T19:23:27Z

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 · 2017-10-17T19:46:52Z

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 · 2017-10-17T20:12:53Z

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 · 2017-10-17T22:11:23Z

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

tomjaguarpaw · 2017-10-17T22:13:05Z

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

mitchellwrosen · 2017-10-17T22:17:34Z

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" ***@***.***> 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 <#33 (comment)>, or mute the thread <https://github.com/notifications/unsubscribe-auth/ABBlpvloNxFvyZSVDM52kUGCAoTOXby7ks5stSZxgaJpZM4Pdxy0> .

ocharles · 2017-10-18T07:17:02Z

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 · 2017-10-18T15:02:19Z

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 · 2017-10-18T15:05:13Z

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

ekmett · 2017-10-18T15:07:50Z

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

ekmett · 2017-10-18T15:08:42Z

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

jb55 · 2017-10-18T16:51:58Z

Thanks guys!

hadronized · 2017-10-19T10:29:00Z

\o/

ocharles added 2 commits September 20, 2017 12:57

Provide an intuitive explanation of Contravariant

d604deb

Explain Divisible

cff1bca

sjoerdvisscher reviewed Sep 20, 2017

View reviewed changes

phadej reviewed Sep 20, 2017

View reviewed changes

VitorCBSB reviewed Sep 20, 2017

View reviewed changes

jb55 reviewed Sep 20, 2017

View reviewed changes

ocharles added 3 commits September 21, 2017 10:15

Fix typos in Contravariant

ee30aad

Fix typos in Divisible

9e5341f

Accidental typo

14847e0

ocharles added 2 commits September 21, 2017 12:58

Explain Decidable

5b7f819

Rewrite Divisible documentation to actually show Divisible

5bdb02d

phadej reviewed Sep 21, 2017

View reviewed changes

Correct type error in stringAndInt example

901b1da

ekmett merged commit 20994af into ekmett:master Oct 18, 2017

RyanGlScott added a commit that referenced this pull request Jan 8, 2018

Add CHANGELOG entries for #30, #33, and #39

270ca8a

Attempt to provide some intuition for contravariant and divisible #33

Attempt to provide some intuition for contravariant and divisible #33

Conversation

ocharles commented Sep 20, 2017 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

phadej left a comment

Choose a reason for hiding this comment

tomjaguarpaw commented Sep 20, 2017

acowley commented Sep 20, 2017

VitorCBSB Sep 20, 2017 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Blaisorblade commented Sep 20, 2017

jb55 commented Sep 20, 2017 via email

hadronized commented Sep 20, 2017 • edited Loading

ekmett commented Sep 21, 2017

ocharles commented Sep 21, 2017

ocharles commented Sep 21, 2017

Choose a reason for hiding this comment

Choose a reason for hiding this comment

RyanGlScott commented Sep 24, 2017

ocharles commented Sep 24, 2017 via email

mitchellwrosen commented Oct 17, 2017 • edited Loading

tomjaguarpaw commented Oct 17, 2017 • edited Loading

jb55 commented Oct 17, 2017

tomjaguarpaw commented Oct 17, 2017

mitchellwrosen commented Oct 17, 2017

phadej commented Oct 17, 2017 • edited Loading

mitchellwrosen commented Oct 17, 2017

tomjaguarpaw commented Oct 17, 2017

mitchellwrosen commented Oct 17, 2017 via email

ocharles commented Oct 18, 2017

ekmett commented Oct 18, 2017

ekmett commented Oct 18, 2017

ekmett commented Oct 18, 2017

ekmett commented Oct 18, 2017

jb55 commented Oct 18, 2017

hadronized commented Oct 19, 2017

ocharles commented Sep 20, 2017 •

edited

Loading

VitorCBSB Sep 20, 2017 •

edited

Loading

hadronized commented Sep 20, 2017 •

edited

Loading

mitchellwrosen commented Oct 17, 2017 •

edited

Loading

tomjaguarpaw commented Oct 17, 2017 •

edited

Loading

phadej commented Oct 17, 2017 •

edited

Loading