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 Lens
es generalize the notion of a field, Prism
s generalize the notion of a constructor and Traversal
s 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 Iso
s, another type of optic which describes isomorphisms.
If we use Choice
, a typeclass which allows lifting values with Either
, we get Prism
s.
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 ac
such thats
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 Grate
s, AffineTraversal
s and Traversal
s.
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 f
s), 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 Lens
es and Prism
s 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.
About the author
If you enjoyed this article, you might be interested in joining the Tweag team.