Optic Category

[tysonzero]

Currently Optic uses 4 type variables for s t a b and thus is not a category. However conceptually Optic seems like a pretty ideal Category. So I figured I'd at least bring up the possibility.

This would essentially involve changing the kind of Optic from:

OpticKind -> IxList -> Type -> Type -> Type -> Type -> Type

to:

OpticKind -> IxList -> (Type, Type) -> (Type, Type) -> Type

I think the majority of the type signatures either don't directly manipulate s and t, or they manipulate them simultaneously / in-sync (e.g. %). So I actually think most type signatures would be simplified by this change.

As mentioned this would allow us to give Optic a Category instance, and thus >>> / category's . could be used for composition. It would also allow any existing functionality based around Category to seamlessly be used on Optic.

Currently % allows for some type changing outside of the s t a b changes, which could not be reflected in >>>. I have not use optics enough to know how problematic this would be, and I would propose keeping % around either way. I am also unsure if it's possible to use more lens-style polymorphism to handle this, where the lenses have all the polymorphism, and the call sites are where the lenses are made concrete.

I know this is a very large change, so it might not be realistic or desirable, but I figured it couldn't hurt to mention the idea.

[phadej]

>>> would be very problematic, you don't compose _1 >>> traversed. Optic-kind changing thing is very common

[tysonzero]

Ah yes I see. Would someone be able to give me a quick summary behind the reasoning for making the lenses themselves monomorphic, but the combinators that use them polymorphic, as opposed to lens's approach which is the opposite. It seems like this would avoid a lot of the Is / explicit supercasting stuff to follow in lens's footsteps here.

[phadej]

I think @adamgundry could comment better on that choice, I don't have a quick answer. For me it follows from the fact, that if you try to define an opaque Optic type, then if you try to also have monomorphic combinators with polymorphic optics, you'll have hard time getting it all to work.

I invite you to try yourself to make it work:

-- this isn't really opaque, but ok it's not transparent either
type Optic k s a = forall token. k token => OpticLike token s a 
newtype Optic token s a = Optic ...

the token would probably be the same A_Lens, A_Traversal enumeration... try to define lens, traversed, traverseOf for your choice on internal representation.

---

As a particular example, note that optics don't form full lattice, we don't have all combinations:

>>> sets map % to not
...
...A_Setter cannot be composed with A_Getter

See https://hackage.haskell.org/package/optics-0.2/docs/Optics.html#g:4

[tysonzero]

I invite you to try yourself to make it work

Now i'm very curious, so i'll think I'll have to give it a go.

As a particular example, note that optics don't form full lattice, we don't have all combinations

That's not particularly problematic. Composing typeclasses can lead to a type that is uninhabited, for example some types implement (Monad, Comonad), and some types implement Contravariant, but if you need a single type to both then you are out of luck.

[tysonzero]

Here is what I came up with.

It's simplified and doesn't deal with type changing updates / prisms / indexing. However it should hopefully give a good idea for how this kind of thing would work.

If you wanted to consolidate all the types under a single Optic type you would be perfectly able to. You could even just do newtype Optic o s a = Optic (o s a) and go from there, or you could use profunctors / van laarhoven. I used separate concrete types for simplicity.

Your sets map >>> to not example would have the type (FromGetter cat, FromSetter cat, Category cat) => cat [Bool] Bool, which no type implements, so it would fail to typecheck regardless of which combinator you tried to use it with.

[phadej]

That is nice, you even have comprehensible type-errors:

*Optics> Nothing ^. _Just

<interactive>:1:12: error:
    • No instance for (FromTraversal Getter)

and reasonable type inference

Optics> :t _1 >>> _Just
_1 >>> traversed
  :: (Category cat, FromTraversal cat, Traversable t) =>
     cat (t c, b) c

Note: it says FromTraversal, because your _Just is traversal, not prism. It would say

  :: (Category cat, FromLens cat, FromPrism cat, Traversable t) =>

otherwise.

---

Compare that with optics:

*Optics> view _Just Nothing

<interactive>:1:1: error:
    • A_Prism cannot be used as A_Getter

*Optics> :t _1 % traversed
_1 % _Just
  :: Field1 s t (Maybe a) (Maybe b) =>
     Optic An_AffineTraversal '[] s t a b

optics say directly that it's An_AffineTraversal. By using concrete kinds, we can compute lower bound. Users don't need to refer to the graph in a documentation to find out what's combination of Lens and Prism.

---

Your design looks promising, but it's up to you to develop it.

[phadej]

Another example which works with optics is following:

foo :: Lens' A Int -> A -> A
foo l x | view l x == 0 = x               -- using as getter
        | otherwise     = over l succ x   -- using as setter

you'd need to add explicit fromLens calls. (you can argue that user could use single over in this example, but that's not the point).

So there are trade-offs to make between whether actual optics or combinators are monomorphic in a optic kind. I cannot say that one is clearly better than another.

I still vaguely remember that @adamgundry had very good point about this, but somehow I cannot recall it.

[tysonzero]

Yeah I honestly don't know where I fall on this ultimately.

If you want two terms with a shared supertype or one as a supertype of the other, you ultimately have to either choose polymorphism and get it implicitly, or choose monomorphism and have operators do it explicitly.

The former approach feels more elegant and gives you things like Category, but it does tend to make the values in question a little more awkward to pass around without RankNTypes or from*. Personally I have never needed to pass around lenses in that way, so I think it'd be my personal preference, but I can appreciate that others might have different needs.

[tysonzero]

Your design looks promising, but it's up to you to develop it.

Thanks, i'm glad it seemed reasonable to you. At some point I will try and do so, particularly depending on what ends up happening with .foo.bar desugaring.

It also leads to a somewhat interesting and different approach where you build in the opposite direction.

You start with the most powerful lens, so presumably something like Equality or Iso, and then you weaken from there. This is somewhat atypical, although it honestly doesn't sound so bad. It could even allow you to build an impure hierarchy on top of the pure hierarchy, as opposed to the opposite which most would probably not be willing to do.

[arybczak]

Hmm, this looks interesting. It seems equally powerful, there are just different tradeoffs.

It seems like this would avoid a lot of the Is / explicit supercasting stuff to follow in lens's footsteps here.

Doesn't that just change their names and move them to a different place? Instead of Is A_Lens A_Traversal you need to have FromLens Traversal instance (which would be pretty much the same, i.e. id modulo rewrapping newtypes).

[tysonzero]

@arybczak

It seems equally powerful, there are just different tradeoffs.

Yeah that sounds right to me.

It seems like composition is nicer with the polymorphic lens approach, but passing around and storing lenses is nicer with the monomorphic lens approach. There are probably some other tradeoffs too.

Doesn't that just change their names and move them to a different place? Instead of Is A_Lens A_Traversal you need to have FromLens Traversal instance

Yeah you are right. Either way you essentially have Is under some name or another, either on the producer of the lens side or on the consumer of the lens side.

However it does seem like you get to avoid needing Join for composition. Since the end use of the lens monomorphizes everything in the chain immediately to the needed type.

[adamgundry]

However it does seem like you get to avoid needing Join for composition. Since the end use of the lens monomorphizes everything in the chain immediately to the needed type.

This is an interesting point. People have previously observed that Join is somehow a bit ad hoc (because it is computing something that in principle should be predetermined), and it makes it impossible to define optics in a modular way (because we need a Join instance for all pairs of optic kinds). So getting rid of it might be no bad thing. And it would be nice to have optics form a Category.

That said, overall I still think the ergonomics are better with monomorphic introduction forms and polymorphic elimination forms. Monomorphic inferred types of composed optics are definitely preferable (Optic An_AffineTraversal says what it means in a way that (FromLens cat, FromPrism cat) => ... doesn't). Moreover, with polymorphic introduction forms users have to make sure they don't accidentally lose the polymorphism too early (e.g. due to the monomorphism restriction, or by giving something a type Lens s a rather than forall o . FromLens s a => o s a).

I'd be very interested to see how your approach develops, though. I wonder how much it is possible to reuse optics internals and implement this as an alternative Optic newtype wrapper...