Functor Optics

Posted on 2017-12-23 by Oleg Grenrus lens

It's good time to write tongue-in-cheek posts on Christmas Holidays.

You have probably have heard about Profunctor Optics, there is a paper by Matthew Pickering et. al, and my Glassery post. Functor optics are similar and simple. With profunctors you can define type-changing optics, with bare Functor you can define only so called simple optics.

#Functor optics?

As I mentioned already, to express type changing optics the OpticP (P for profunctor) type synonym takes five arguments: a profunctor and four type variables:

But what if you don't want to change types? When s ~ t and a ~ b, we can simplify the above into Functor optics:

As with profunctor optics, there are different type-classes constraining variable a -functor, that's how we get lenses, prisms, getters, setters etc. We will explore them below.

#Functor

Every Haskell programmer is familiar with the Functor type class:

What might be surprising, in functor optics it's used to define Review (similarly as Bifunctor is used to define Review in profunctor optics, this kind of analogy is visible through all definitions).

We have upto to create Review and review to use one. upto is simply a fmap, and to define review we use Identity functor: a -> b ≅ Identity a -> Identity b.

By the way, A Representation Theorem for Second-Order Functionals by Mauro Jaskelioff and Russell O'Connor tells us that

which is intuitively true. The left to right is witnessed by review, and other direction by upto. However, the paper has more rigorous and general proof.

#Existing classes

Let's continue with classes more or less widely used, i.e. there is a package on Hackage!

#Contravariant

"Dually" to Functor (dual of Functor is Functor), the Contravariant type class gives rise to a Getter.

Whereas in Haskell, one can think of a Functor as containing or producing values, a contravariant functor, Contravariant is a functor that can be thought of as consuming values.

Contravariant lives in a contravariant package.

As with Review, constructor of Getter is simply a member of the class, in this case contramap:

to was easy to define, for view we will need a new newtype Flipped:

#Invariant

The Invariant class is less known. It's a moral superclass of both, Functor and Contravariant type classes. In fact, any * -> * type parametric (i.e. ADTs) in the argument permits an instance of Invariant. It lives in invariant package.

For example, Flipped is also an Invariant functor:

Reader could guess that invmap is a constructor for Iso.

view and review work with optics constructed with iso, e.g.

One remark about Invariant. In Profunctor Optics: The Categorical view Bartosz Milewski looks into profunctor optics. In very similar way, we can look into Functor optics, yet instead of using pairs <a, b> and <s, t>, it's enought to use a and s, then we arrive to the similar conclusion:

#No class at all

If we don't constraint f, we have an equality. Note: data a :~: b is a non-parametric GADT, and therefore not even an Invariant.

Also note, here we havee a Leibnizian equality as in eq package, just without a newtype wrapper:

#New classes

So far we handled the edges of optics lattice: Identity, Iso, Getter, and Review. But how about simple Lens?

We can define over using a Endo newtype.

Note: Endo is neither Functor, nor Contravariant, but it's Invariant!

But what's the type-class for Setter? Here, we can use what we know about profunctor optics. There, the class is Mapping, we can have similar class too

Endo is an instance of this class, but Flipped isn't (we cannot view through a Setter!):

So we can defined Setter as

For setting we need an auxiliary Functor Context:

Setter was defined in a very same way as it would be in a profunctor optics, so are many other optics, e.g. Lens we cover next.

#Strong

We'll conclude the journey by defining Lens. As with Setter, we can piggyback on what we know from profunctors:

There aren't that many Strong functors, Endo and Flipped are (we we can over / set and view through the lens, respectively):

So finally we can define Lens type-alias and lens constructor:

#Conclusion

In this post we saw definitions Functor optics, which are simple versions of Profunctor optics. This simplicity might be useful when experimenting with optics, as there is less type-variables to deal with. Working out Prism or Traversal is this "formalism" is left as an exercise to the reader. Another interesting exercise is to figure out Free Strong, apply it in the construction of Jaskelioff & O'Connor & Bartosz, turn the category theory wheels and see data ConcreteLens s a = CL (s -> a) (s -> a -> s) pop out.

Please comment on Reddit thread or on Twitter.

#Postscriptum

Edward Kmett mentions on Twitter

Fun fact: We figured out prisms, etc. for this form of optic before we figured out the profunctor versions.

#To and from Profunctor optics

Phil Freeman wonders on Reddit on how you go between Profunctor and Functor optics.

Let's see a simple example converting Lens. From functor to profunctor is simple using Trace newtype Phil mentions:

Other way around is a little tricker!

Phil thinks using existential Split would work. And he is right.

We can even write Strong instance:

So we can convert Profunctor Lens into Functor one:

This direction, using Split, isn't as elegant as other one using Trace, but seems to work!


This work is licensed under a “CC BY SA 4.0” license.

Site proudly generated by Hakyll