Optics make it possible to conveniently access and modify data structures in an immutable, composable way. Thanks to that, they catch lots of attention from the functional programming community. Still, you can have a hard time understanding how they work just by looking at data declarations and type definitions.

In this post, I present a way of encoding optics that is different from usual. This encoding, called existential optics, is easier to understand than the other encodings, since it makes more explicit the structure of each optic. This is not new and is well known in the category theory academic circles. Still, these ideas do not seem to appear in libraries for languages like Haskell, Purescript, or Scala.

The most well-known type of optics are lenses, which were also the first to be analyzed and used. We will use them as our recurring example to compare the several ways we have to encode optics.

Lenses 101

A Lens is effectively the immutable version of a getter/setter pair you will often find in object-oriented programming, and especially in Object-Relational mappers. It allows focusing on a component of a container data type.

For example, consider an Address record that contains a street field. A Lens Address Street allows us to retrieve the Street from an address.

streetLens :: Lens Address Street

view streetLens (Address { street = "Baker Street", number = "221B" })
-- "Baker Street"

We could reuse the same lens to update the street inside the address.

over streetLens toUpper (Address { street = "Baker Street", number = "221B" })
-- Address { street = "BAKER STREET", number = "221B" }

Optics generalize this pattern. Intuitively, while Lenses generalize the notion of a field, Prisms generalize the notion of a constructor and Traversals generalize both to to an arbitrary number of values.

Lenses, and optics in general, compose extremely well. For example, if we also had a User record containing an address field of type Address, we could easily access and modify the street field of the address.

addressLens :: Lens User Address

view (streetLens . addressLens)
  (User { address = Address { street = "Baker Street", number = "221B" }, name = "Sherlock" })
-- "Baker Street"

over (streetLens . addressLens) toUpper
  (User { address = Address { street = "Baker Street", number = "221B" }, name = "Sherlock" })
-- User { address = Address { street = "BAKER STREET", number = "221B" }, name = "Sherlock" }

Now it is time to ask ourselves how a Lens s a could be encoded. Next, I will present some possible alternatives for lenses and compare them with respect to the following aspects:

• how easy it is to understand what the encoding actually describes;
• how easily composition works;
• how easily we can generalize the encoding to other optics.

Explicit encoding

The easiest option is to encode a Lens just as a getter and a setter

data Lens s a = Lens
  { get :: s -> a
  , set :: s -> a -> s
  }

This encoding is extremely easy to grasp, packing together exactly the API we would like to use. On the other hand, it is not immediate to understand how a Lens s a and a Lens a b could compose to return a Lens s b. Also, it turns out that this encoding is very ad-hoc, and it is not immediately clear how to generalize it to other optics.

Van Laarhoven encoding

In 2009 Twan Van Laarhoven came up with a new encoding for lenses which is commonly used, for example by the lens library.

type Lens s a
  =  forall f. Functor f
  => (a -> f a) -> s -> f s

This says that a Lens s a allows us to lift a function a -> f a to a function s -> f s for any possible functor f. For a more in-depth explanation of the Van Laarhoven encoding, please refer to this talk by Simon Peyton Jones.

I would argue that it is harder to understand what the encoding is describing. The functionalities provided by the explicit encoding could be recovered with a wise choice of f. For example, when f = Identity we get a function (a -> a) -> (s -> s) which allows us to edit the content. Similarly, if we choose f = Const a, we get a function (a -> a) -> s -> a; applying this to the identity function, we get back our get :: s -> a function.

What we gain, though, is a massive improvement with respect to composability. Now, we can use just function composition, i.e. ., to compose lenses.

It also generalizes quite well to traversals, but not so well to prisms; see for example how the definition of Prism in the lens library differs.

Profunctor encoding

An encoding which is commonly used for new optics libraries is the so-called profunctor encoding. The main idea is to quantify the encoding, not over functors, but profunctors instead.

type Lens s a
  =  forall p. Strong p
  => p a a -> p s s

In these terms, a Lens is a way to lift a value of type p a a to a value of type p s s for any Strong profunctor p (i.e. a profunctor which allows lifting values with (,)).

I would argue that this encoding is even less immediate to understand than Van Laarhoven’s one. On the other hand, since we are still dealing with simple functions, we are still able to compose optics just with function composition.

It also becomes extremely easy to generalize this encoding to other types of optics. The type of optic is determined by the constraint we have on the p type variable. In the case of Lens, we have Strong, but if we use just Profunctor, we get Isos, another type of optic which describes isomorphisms. If we use Choice, a typeclass which allows lifting values with Either, we get Prisms.

Now when we want to compose two optics of a different type, we just need to collect all the relevant constraints. For example, if we compose a Lens, which is constrained by Strong p, with a Prism, which is constrained by Choice p, we will get an optic constrained by (Strong p, Choice p).

In short, the profunctor encoding works extremely well with regard to compositionality, but it constrains us with an encoding that is not easy to understand. So the question now is: can we encode optics in another way, that is more expressive and easy to manipulate, possibly giving up a little bit of composability?

Existential encoding

Another equivalent way of expressing what a Lens is, uses the so-called existential encoding, described by Van Laarhoven himself.

data Lens s a
  = forall c. Lens (s -> (c, a)) ((c, a) -> s)

This says that a Lens s a is comprised of two functions: one from s to (c, a) and one back, where we can choose c arbitrarily. Since c appears only in the constructor and not as a parameter of the Lens type constructor, it is called existential.

Coming back to the example used above, with the existential encoding we can implement streetLens as follows:

streetLens :: Lens Address Street
streetlens = Lens f g
  where
    f :: Address -> (Number, Street)
    f address = (number address, street address)

    g :: (Number, Street) -> Address
    g (street, number) = Address street number

Generally, when we know s and we know a, we can identify c as whatever is left over after removing an a from s, broadly speaking.

Easy to grasp

Another way to read this definition is:

A Lens s a is a proof that there exists a c such that s is isomorphic to (c, a).

This is an extremely explicit way to think about a Lens; it says that whenever we have a Lens, we could actually think about a tuple.

Easy to use

Thanks to the fact that we can easily understand what a Lens is with the existential encoding, it is also easy to understand how to define combinators for it. The idea is that we can deconstruct s into a pair (c, a) and then build it back.

For example, if we want to extract a from s, we simply deconstruct s into the pair (c, a), and then we project it into the second component.

view :: Lens s a -> s -> a
view (Lens f _) = snd . f

Similarly, if we want to lift a function h :: a -> a to a function s -> s, we can decompose s into (c, a), map h over the second component of the pair and then construct a new s from the old c and the new a.

over :: Lens s a -> (a -> a) -> s -> s
over (Lens f g) h = g . fmap h . f

Easy to generalize to other optics

When it comes to generalizing the existential encoding to other optics, it turns out that it is enough to switch the (,) data type with another type constructor of the same kind.

Prisms

For example, if we use Either instead of (,) that we had in the definition of a Lens, we get a Prism:

data Prism s a
  = forall c. Prism (s -> Either c a) (Either c a -> s)

This definition tells us that a Prism s a is just a proof that there exists a c such that s is isomorphic to Either c a.

With this definition it is easy to define the common operations used on a Prism. preview allows to retrieve the focus if we are on the correct branch of the sum type; review instead allows to construct s from a.

preview :: Prism s a -> s -> Maybe a
preview (Prism f _) = rightToMaybe . f

review :: Prism s a -> a -> s
review (Prism _ g) = g . Right

General optics

Generally, an optic has the following shape:

data Optic f s a
  = forall c. Optic (s -> f c a) (f c a -> s)

This amounts to saying that Optic f s a is a proof that there exists a c such that s is isomorphic to f c a. I find this a really clear explanation of what an optic is and how to think about it. It is enough then to plug a concrete data type instead of f to get a concrete family of optics. For example:

type Lens = Optic (,)

type Prism = Optic Either

type Iso = Optic Tagged

where Tagged is the identity functor with an added phantom type.

We could also use other data types with the correct kind, like (->), Affine and PowerSeries, to obtain other optics like Grates, AffineTraversals and Traversals.

type Grate = Optic (->)

type AffineTraversal = Optic Affine

type Traversal = Optic PowerSeries

Composing existential optics

Lenses and optics are well known for how well they compose. Let’s see how the existential encoding behaves with respect to composition.

We can immediately observe that function composition does not work with the existential encoding, since we are not dealing with functions anymore.

Let’s consider first the case where we are composing two optics of the same type

compose :: Optic f s u -> Optic f u a -> Optic f s a

If we try to implement compose just following the types, we will probably arrive at

compose
  :: (forall x. Functor (f x))
  => Optic f s u -> Optic f u a -> Optic f s a
compose (Optic f g) (Optic h l)
  = Optic (_a . fmap h . f) (g . fmap l . _b)

We are first deconstructing s into f c u and then u into f c1 a and we are left with two typed holes _a and _b.

_a :: f c (f c1 a) -> f c0 a
_b :: f c0 a -> f c (f c1 a)

Existential associativity

To fill the holes we left, we introduce a type class. Note that c0 in _a and _b is existentially quantified, so we have the freedom to instantiate it however we like.

class ExistentiallyAssociative f where

  type E f a b

  existentialAssociateL :: f a (f b c) -> f (E f a b) c
  existentialAssociateR :: f (E f a b) c -> f a (f b c)

We use an associated type family E to be able to choose what c0 should be for the given f. Notice also how, when E f = f, this type class is saying that f is associative. And this is in fact what happens with data types as (,) and Either. You can find instances for other data types here.

Now, thanks to this new type class, we can fill the holes we left and conclude the definition of compose

compose
  :: ( forall x. Functor (f x)
     , ExistentiallyAssociative f )
  => Optic f s u -> Optic f u a -> Optic f s a

Changing optic type

To compose optics of different types (i.e. defined for different fs), we need first to be able to change the type of an optic. This makes sense because, for example, an Iso can always be seen both as a Lens and as a Prism, and Lenses and Prisms can be seen as AffineTraversals.

What we would like to do is convert an Optic f s a into an Optic g s a. If we try to follow the types, we will probably end up with something like the following:

morph :: Optic f s a -> Optic g s a
morph (Optic h l) = Optic (_a . h) (l . _b)

_a :: f c a -> g c0 a
_b :: g c0 a -> f c a

where _a and _b are typed holes and c0 is existential, meaning that we can choose what it is.

Embedding

As we did for ExistentiallyAssociative, we are going to fill the holes by introducing a type class that provides exactly what we need. Similar to the previous case, we will use an associated type family M to be able to choose c0.

class Morph f g where

  type M f g c

  f2g :: f c a -> g (M f g c) a
  g2f :: g (M f g c) a -> f c a

This class describes how we can embed f into g choosing c0 appropriately.

For example, we can see the identity functor Id as a pair (,) choosing the first component of the pair to be ().

instance Morph Tagged (,) where
  type M Tagged (,) c = ()

  f2g :: Tagged c a -> ((), a)
  f2g (Tagged a) = ((), a)

  g2f :: ((), a) -> Tagged c a
  g2f ((), a) = Tagged a

Similarly, we can see Id as an Either choosing the left component to be Void. For more instances, take a look here.

This new type class allows us to complete the definition of morph we started above.

Composing optics of different type

To compose existential optics of different types, we now need to connect all the pieces we have. To compose an Optic f s u with an Optic g u a we first need to morph them both to a common optic type where we can compose them.

compose'
  :: ( ExistentiallyAssociative h
     , forall x. Functor (h x)
     , Morph f h
     , Morph g h )
  => Optic f s u
  -> Optic g u a
  -> Optic h s a
compose' opticF opticG
  = compose (morph opticF) (morph opticG)

Conclusion

The existential encoding for optics can not compete with profunctor optics in terms of composability. On the other hand, it scores better on other aspects. In particular:

• the definition of optics is easy to understand. This is a two-fold perk. On one side, it makes teaching and learning optics easier. On the other hand, it makes the implementation of combinators and consuming the library easier, since the implementer is left to use simple data types.
• it clarifies what an optic is. Being able to express an optic as proof of the existence of an isomorphism, allows having a clear picture in mind about what an optic is. This helps discriminate optics from other constructs and possibly also to discover new optics.
• the hierarchy between optics is explicit. It is completely described by the Morph instances we described above, which can be understood in terms of embedding one data type into another.

This blog post would not exist without the precious work of many other programmers and category theorists. Reading Bartosz Milewski’s optics-related work was a particular inspiration.

If you want to dive deeper into the code, you can find a sketch of the ideas explained in this post in this repository.