Use profunctor encoding & other improvements

[arybczak]

So this is quite big, but roughly speaking it does the following:

• Converts to profunctor encoding
• Adds affine fold and traversal
• Adds some utility functions for various optics
• Removes vl* functions (apart from vlLens and vlTraversal) as the other ones were using internal versions of typeclasses, so they wouldn't work with external ones
• Reorganizes subtyping module for better error messages and no orphan instances

Implements #18, solves #10 and #15.

[arybczak]

I fixed compilation with GHC 8.2.2 (it looks like some weird bug, it typechecked with 8.0.2 and 8.4.3).

[adamgundry]

Thanks for this! There's a lot here to page back in and review, so apologies that it is taking us a while to find time to dig into it. I'll try to go through the details and understand the impact of these changes.

One question is to what extent this unavoidably moves us away from API-compatibility with lens (although we haven't really verified to what extent that held in practice).

[arybczak]

One question is to what extent this unavoidably moves us away from API-compatibility with lens (although we haven't really verified to what extent that held in practice).

The only thing I can think of is that there is no from to turn Iso around, as re can be more general with profunctor encoding, thus it's also used for Iso.

Other than that, what I noticed:

• We can't use traverse directly, but I added a traversal called traversed mirroring similar helpers for other optics such as mapped or folded.
• . is %.
• view is now more compatible with lens, but it uses a type class and chooses view1, view01 or viewN depending on the optic it's called with.

What is more (this is not related to the encoding, rather than wrapping things in newtypes), optic transformers (such as e.g. choosing) cannot be written for many flavors as one function (as an example, see my implementation of re - there is one internal implementation, but it needs to be done with the help of typeclass where a flavor of optic is known, otherwise GHC can't solve the constraints. There isn't many functions like that so I guess it's not a big deal, but I'm just pointing it out.

Actually, if it comes to choosing, I don't think it can be written as easily for profunctor encoding as in lens - see my question here. I've since then concluded that it's not possible to use SumProfunctor to do that because then I couldn't write appropriate Re instance - I've gotten further than in the post, but at the end it boils down to the fact that you can split the merged optics, but you can't decide which path you are supposed to take as that depends on the input value and there is no access to it. But still, if it had a single implementation, it would have to be done with the type class anyway (just as re), so that's not that big of a deal - we can write choosing for all relevant optic types, it will just be different for each of them (without introducing any other profunctor constraints).

[arybczak]

I added implementation of indexed traversals, folds and setters. Maybe stacking all of it in a single PR is not the best idea, but in principle profunctor encoding doesn't bring anything new, so I wanted to make it more complete and appealing to review (heh).

Implements #12.

This explores idea(s) from http://oleg.fi/gists/posts/2017-04-26-indexed-poptics.html (specifically, CPS variant) to make regular optics "index-preserving" (which is reflected by the additional type parameter), so that both indexed and regular optics have the same form and can seamlessly compose.

λ> iover (_Left % imapped % _1) (,) $ Left [('a', "hey"), ('b', "there"), ('c', "bye")]
Left [((0,'a'),"hey"),((1,'b'),"there"),((2,'c'),"bye")]

λ> iover (imapped % _Left) (,) $ [Left 'a', Right "hi", Left 'c']
[Left (0,'a'),Right "hi",Left (2,'c')]

The difference from how lens library handles these:

• All indices from indexed optics carry through with the usual composition (lens only preserves the rightmost index by default)

lens:

λ> iover (itraversed . itraversed) (,) ["hey", "bye"]
[[(0,'h'),(1,'e'),(2,'y')],[(0,'b'),(1,'y'),(2,'e')]]

optics:

λ> iover (icompose (,) % itraversed % itraversed) (,) ["hey", "bye"]
[[((0,0),'h'),((0,1),'e'),((0,2),'y')],[((1,0),'b'),((1,1),'y'),((1,2),'e')]]

λ> :t itraversed % itraversed
itraversed % itraversed
  :: (TraversableWithIndex i1 t1, TraversableWithIndex i2 t2) =>
     Optic
       An_IxTraversal i3 (i1 -> i2 -> i3) (t1 (t2 a)) (t1 (t2 b)) a b
λ> :t itraversed % itraversed % itraversed
itraversed % itraversed % itraversed
  :: (TraversableWithIndex i1 t1, TraversableWithIndex i2 t2,
      TraversableWithIndex i3 t3) =>
     Optic
       An_IxTraversal
       i4
       (i1 -> i2 -> i3 -> i4)
       (t1 (t2 (t3 a)))
       (t1 (t2 (t3 b)))
       a
       b
λ> :t icompose3 (,,) % itraversed % itraversed % itraversed
icompose3 (,,) % itraversed % itraversed % itraversed
  :: (TraversableWithIndex a1 t1, TraversableWithIndex b1 t2,
      TraversableWithIndex c t3) =>
     Optic
       An_IxTraversal
       r
       ((a1, b1, c) -> r)
       (t1 (t2 (t3 a2)))
       (t1 (t2 (t3 b2)))
       a2
       b2
λ> :t itraverseOf $ icompose3 (,,) % itraversed % itraversed % itraversed
itraverseOf $ icompose3 (,,) % itraversed % itraversed % itraversed
  :: (TraversableWithIndex a1 t1, TraversableWithIndex b1 t2,
      TraversableWithIndex c t3, Applicative f) =>
     ((a1, b1, c) -> a2 -> f b2)
     -> t1 (t2 (t3 a2)) -> f (t1 (t2 (t3 b2)))

• Indexed optics can't be used as regular ones. This is a conscious API decision as internal implementation allows for that (i.e. in principle IxTraversal can be implemented via Traversal etc.), but without the conjoined trick using indexed optics as regular ones incurs a performance loss as opposed to using equivalent, regular optic directly, so I opted out from doing it this way (I'm also not a fan of implicit degradation like that).

Illustration of current optic hierarchy:

1. Black arrow means "is".
2. Blue arrow means "can be converted to with re".
3. Orange arrow means "can be used as one, assuming it's composed with any optic below the orange arrow first" (e.g. _1 is not an indexed fold, but itraversed % _1 is, because it's an indexed traversal, so it's also an indexed fold).

[adamgundry]

Interesting! Thanks for exploring this. I've had a brief play around with it, and I quite like this approach to indexed optics. Here are some scattered initial thoughts...

Have you thought about coindexed prisms at all?

The Haddocks should explain the i and o parameters of Optic, perhaps with a brief comment and a link to Optics.IxTraversal with a discussion of how to understand and compose indexed optics.

The reorganisation means that the definitions of optic flavours are now a bit less modular, although we couldn't add in optic flavours to the subtyping hierarchy after the fact anyway, so this is no great loss. I imagine that making Join a closed type family is a bit more flexible in other ways.

In #18 you sketched a hierarchy in which re was always reversible, but it seems you haven't done that here. Did you try it? Or do you think the extra flavours are not worth it?

The CheckIndices i o overlapping instance breaks inference, I think. For example itoListOf itraversed "hello" fails due to overlap, but works without this instance. Perhaps using a closed type family rather than overlapping instances might behave better? More generally I find it a bit puzzling that CheckIndices doesn't carry any evidence.

Generalising view using a type class seems plausible to me, as it makes the differences for different optic flavours a bit more explicit than in lens. I like the fact that things like :t view @A_Lens give sensible answers.

[arybczak]

Have you thought about coindexed prisms at all?

Not really, I was deterred by 9 type variables ;)

In #18 you sketched a hierarchy in which re was always reversible, but it seems you haven't done that here. Did you try it? Or do you think the extra flavours are not worth it?

I had it done without the Optic newtype. I pushed a commit with them as a test. I though they might not be of much use as in practice no one will probably call re twice on an optic to get an original, but I suppose it's good to include it for elegancy's sake. Here's the updated hierarchy (I also added Equality for good measure):

The CheckIndices i o overlapping instance breaks inference, I think. For example itoListOf itraversed "hello" fails due to overlap, but works without this instance. Perhaps using a closed type family rather than overlapping instances might behave better? More generally I find it a bit puzzling that CheckIndices doesn't carry any evidence.

Right, I fixed that. CheckIndices is a bit tricky. It needs to be a class rather than type family because we need the o ~ (i -> i) equality to always be there for unsolved constraint in order for the definition of itoListOf etc. to typecheck. On the other hand we can't include it directly in the function signature, because then GHC picks it up and for unflattened indices immediately returns cannot construct the infinite type error. However, when the equality is on the LHS of the instance head, it picks the appropriate instance first, then checks the LHS, sees bogus type equality leading to infinite type error, but it also sees TypeError and then it ignores the bogus equality and returns custom type error instead. Though I wonder if it works by accident.

Generalising view using a type class seems plausible to me, as it makes the differences for different optic flavours a bit more explicit than in lens. I like the fact that things like :t view @A_Lens give sensible answers.

Hmm, yes, I didn't think of its usage like that. Now I feel less bad for introducing these classes, haha.

[adamgundry]

Have you thought about coindexed prisms at all?

Not really, I was deterred by 9 type variables ;)

Heh, I don't blame you... I do wonder if it is possible to get away with a single type parameter that gets instantiated to a promoted datatype with multiple fields, i.e. something like

data IX = I Type Type Type Type -- i j k l
newtype Optic k (ix :: IX) s t a b

but perhaps it's difficult to keep the parameter as a variable even when not using (co)indexed stuff.

Thanks, I now understand CheckIndices a bit better. I'd missed the superclass constraint carrying the evidence. It does seem a bit dubious to rely on GHC giving the right error message here, but if it turns out to be unreliable one can probably use an equality datatype instead.

[adamgundry]

We agreed to merge this and continue polishing on master. I've raised issues for the outstanding things of which I'm aware.