A "lens" and a "partial lens" seem rather similar in name and in concept. How do they differ? In what circumstances do I need to use one or the other?
Tagging Scala and Haskell, but I'd welcome explanations related to any functional language that has a lens library.
To describe partial lenses—which I will henceforth call, according to the Haskell
lensnomenclature, prisms (excepting that they're not! See the comment by Ørjan)—I'd like to begin by taking a different look at lenses themselves.A lens
Lens s aindicates that given answe can "focus" on a subcomponent ofsat typea, viewing it, replacing it, and (if we use the lens family variationLens s t a b) even changing its type.One way to look at this is that
Lens s awitnesses an isomorphism, an equivalence, betweensand the tuple type(r, a)for some unknown typer.This gives us what we need since we can pull the
aout, replace it, and then run things back through the equivalence backward to get a newswith out updateda.Now let's take a minute to refresh our high school algebra via algebraic data types. Two key operations in ADTs are multiplication and summation. We write the type
a * bwhen we have a type consisting of items which have both anaand aband we writea + bwhen we have a type consisting of items which are eitheraorb.In Haskell we write
a * bas(a, b), the tuple type. We writea + basEither a b, the either type.Products represent bundling data together, sums represent bundling options together. Products can represent the idea of having many things only one of which you'd like to choose (at a time) whereas sums represent the idea of failure because you were hoping to take one option (on the left side, say) but instead had to settle for the other one (along the right).
Finally, sums and products are categorical duals. They fit together and having one without the other, as most PLs do, puts you in an awkward place.
So let's take a look at what happens when we dualize (part of) our lens formulation above.
This is a declaration that
sis either a typeaor some other thingr. We've got alens-like thing that embodies the notion of option (and of failure) deep at it's core.This is exactly a prism (or partial lens)
So how does this work concerning some simple examples?
Well, consider the prism which "unconses" a list:
it's equivalent to this
and it's relatively obvious what
rentails here: total failure since we have an empty list!To substantiate the type
a ~ bwe need to write a way to transform anainto aband abinto anasuch that they invert one another. Let's write that in order to describe our prism via the mythological functionThis demonstrates how to use this equivalence (at least in principle) to create prisms and also suggests that they ought to feel really natural whenever we're working with sum-like types such as lists.