Lens gets a lot of flack for having crazy type signatures. This is a whirlwind derivation of the craziest of signatures from the ground up. It might be useful as a starting point for exploring more of the lens code and seeing "through" the sophisticated types.
Getting and Setting
At the simplest, a Lens is a getter and a setter much like the getters and setters in an OO language. If you've not seen them before you might wonder what "getting" and "setting" even means in a pure language.
In Haskell, getting and setting refers to the relationship between a "large" structure and some "smaller" part of it. For instance, given a tuple you might want to get and set the left side of it.
get :: (a, b) -> a
get (part, _) = part
set :: a' -> (a, b) -> (a', b)
set part (_, b) = (part, b)so get is an extraction function and set x is a transformation on the "larger" structure parameterized by the "smaller" structure.
Early lenses
A Lens is always just a "getter" and a "setter" together. The most obvious implementation would be to tuple them.
data Lens a b
= Lens { get :: a -> b
, set :: b -> a -> a
}and indeed this is a perfectly valid Lens that has most of the common properties of the more clever derivations to come. We'll build our lens l that focus on the "smaller" part of some "larger" thing and then use the field selectors get l and set l just like before.
-- | A *Lens* that focuses on the first element in a tuple.
_1 :: Lens (a, b) a
_1 = Lens (\(part, _) -> part) (\part (_, b) -> (part, b))
> :t get _1
get _1 :: (a, b) -> a
> :t set _1
set _1 :: a -> (a, b) -> (a, b)If you're really paying attention you'll notice that the "setter" on this lens is actually slightly less powerful than the one we wrote in the first section. We'll revisit that later and rectify it.
Composition
If this were all that Lenses offered there might not be much of a point, but they can also be chained letting us build lenses which focus deep inside of the "larger" object from many simpler lenses together.
-- | Lens composition
(>-) :: Lens a b -> Lens b c -> Lens a c
la >- lb = Lens (get lb . get la) $ \part whole ->
set la (set lb part (get la whole)) wholethe setter is a little messy, but if you think of there being big (a), middle (b), and little (c) pieces then it's this process, given an original big part and a new little part
- Get the original middle part from the original big part
- Update the middle part with the new little part
- Update the bit part with the new middle part
which isn't too challenging, though it is tedious. Part of the magic of lens composition is that it completely dispatches with all of this tedious boilerplate.
> :t _1 >- _1 >- _1 >- _1 >- _1 -- useless, but if you didn't have pattern matching
-- this would be very challenging to code
-- ... we don't always have pattern matching,
-- but can always have lenses
_1 >- _1 >- _1 >- _1 >- _1 :: Lens (((((c, b4), b3), b2), b1), b) cGeneralizing to Store
The lenses up to this point are fully functional, but there's a lot more structure to them that we haven't expoloited. For instance, both the "getter" and the "setter" take the larger piece as an argument. We can thus combine those applications and "extract an argument from our tuple".
type Lens a b = (a -> b, b -> a -> a) -- same as before
type Lens a b = (a -> b, a -> b -> a) -- flip the setter
type Lens a b = a -> (b, b -> a) -- pull the parameter outThe intuition to guide this change is that now a Lens is a function that takes a large structure and returns to us two things, (1) a small piece from inside that large structure, and (2) a "holey" version of our original structure---it demands a small piece like the one it gave us in order to restore the original large structure. In fact, if we just put these pieces back together we'll get back our original object.
lensToId :: Lens a b -> (a -> a)
lensToId f = \a -> let (piece, hole) = f a in hole pieceThis intuition is already important---the idea of separating structures into parts and the holes that those parts fit into shows up repeatedly---but the process of doing that separation a -> (b, b -> a), and the result (b, b -> a) itself, both have surprisingly rich structure.
Without going into any details about what that structure "means", I'll describe it. To begin, that pair is often called Store...
data Store b a = Store b (b -> a)Functors
Almost too obvious to mention, but (b, b -> a) forms a Functor in exactly the same way that (->) e, the Reader Monad, does.
instance Functor (Store b) where
fmap f (Store piece hole) = Store piece (f . hole)Comonads
Without any elaboration, you can think of a Comonad as the inversion of a Monad. Monads m are defined by their operations join :: m (m a) -> m a and return :: a -> m a. Comonads (often denoted w as a visual pun) are defined by their operations extract :: w a -> a and duplicate :: w a -> w (w a). Or, to drive home the correspondance even more
| Monad a -> m a m (m a) -> m a
| Comonad w a -> a w a -> w (w a)
It turns out that Store b forms a Comonad.
instance Comonad (Store b) where
extract (Store piece hole) = hole piece -- this is the second part of lensToId!
duplicate (Store piece hole) =
Store piece (\newPiece -> Store newPiece hole)Coalgebras
The final interesting structure is the Coalgebra. This is a generalization of unfoldr for turning a "seed" into something with more structure. For instance, you can use unfoldr to create a list counting down from an integer.
> unfoldr (\n -> if (n == 0) then Nothing else Just (n, n-1)) 10
[10,9,8,7,6,5,4,3,2,1]If we just look at unfoldr go we see it has a type like a -> [a], an "injection" function. Things like unfoldr go transform seed values into lists of values and are exactly what Coalgebras are. These are tightly related to recursion because so long as the larger result structure is a Functor (and this is actually a requirement to calling a -> f a a Coalgebra) then we can repeatedly apply our coalgebra.
> unfoldr go :: a -> [a]
> fmap (unfoldr go) . unfoldr go :: a -> [[a]] -- this is like "duplicate"
> fmap (fmap (unfoldr go)) . fmap (unfoldr go) . unfoldr go :: a -> [[[a]]] -- and duplicate again!So, at this point since we're calling our Lens a b = a -> Store b a and Store b is a Functor we're allowed to call our Lens a Coalgebra.
type Coalg f a = a -> f a
type Lens a b = Coalg (Store b) a -- (thanks to Austin Seipp for pointing this out)Which, all together, leads to the fascinating or oblique notion that "Lenses are Costate Comonad Coalgebras". [1]
What did we gain?
Alright, so now that we've seen that this rather tiny trick, pulling just one argument out of our trivial "pair of a getter and a setter" structure, has exposed a great deal of hidden structure in lenses does it make our lenses any more powerful? Our intuition any more clear?
Well, hopefully thinking about the Store Comonad as holding a "piece" and its "hole" as two parts of the "whole" as given new insight, but is it really worth all that jargon?
One way we get a lot of improvement is in writing the composition operator (>-). Previously it wasn't exactly difficult to write, but demanded a small amount of mental gymnastics to write the combined "setter". What does it look like using the Store Comonad?
(>-) :: Lens a b -> Lens b c -> Lens a c
(la >- lb) a = let Store partB holeBA = la a
Store partC holeCB = lb partB
holeCA = holeBA . holeCB
in Store partC holeCAReally, given the types available, this function almost writes itself. It also more clearly demonstrates the idea of splitting our a type into the two underlying pieces and their holes---the two layers of Stores---and then sewing them back together to form the resulting, composed Store.
Furthermore, if you read the blog post by Russell O'Connor I linked earlier, you'll might have noticed there's something genuinely beautiful going on here.
Laws
Our inutitions so far are built upon our beliefs about how Lenses "should" behave, but we can be more specific. The notion of a lens has been studied for a long time by computer scientists and a set of formal laws which outline everyone's intution have been established. These are Pierce's Laws of a "Very Well Behaved Lens":
Setting something back that you just got out is a no-op
set s (get s) == s
Getting something that you just set is exactly that thing
get (set s v) == v
If you put something repeatedly, the last put wins
get (set (set s v1) v2) == v2
Hopefully you'll find that your inutition about what "getting" and "setting" might mean is completely aligned with these laws. They're carefully designed to capture the entire behavior of getting and setting and nothing more.
What O'Connor discovered was that these laws, things thought to be the essence of a particularly practical notion of computer science, can be derived as a specific instance of much more general laws known to hold for any "Comonad Coalgebra". In particular, given some l :: Lens b a = a -> Store b a they are completely equivalent to
extract . l == id -- injecting with the coalgebra then extracting the comonad is `id`
-- (this is just breaking our whole into the "piece" and "hole"
-- then jamming them back together)
fmap l . l == duplicate l -- duplicate is the same as "repeated coalgebra injection"
-- (see the comments in the Coalgebra section)Clearly these laws are less inuitive than the "Well Behaved Lens Laws", but they also are not much more than a very formal was of saying that Comonad Coalgebras are as boring as possible---they behave exactly the way you would expect them to.
And "Costate" Comonad Coalgebras [1] behave as boringly as possible, exactly as getters and setters.
Can we go further?
This is already a lot of generality, but we haven't yet reached the representation that lens uses today. There's one last step.
Right now, if someone were to use our "Comonad Coalgebra" lenses they would need an instance of the Store datatype. That means dragging around all of our lens library as a dependency to every library which offers a lenslike interface. Not the worst result, but it'd be nice if we could offer a "minimal" interface for this dependency. Something that eliminates the datatype Store while keeping all of its power around.
If you read Edward Kmett's discussion of Store Comonadic Cellular Automata or my followup exploration you will have seen a very particular and interesting operation on Stores called experiment
experiment :: Functor f => Store b a -> (b -> f b) -> f a
experiment (Store part hole) inj = hole <$> inj partAs Edward hinted and I tried to explore in much greater depth, experiment converts a Store into its "functional" form. Furthermore, this conversion is an isomorphism.
Store piece hole ~= experiment (Store piece hole)
Store b a ~= (b -> f b) -> f aJust for completeness, I'll write the other isomorphism which I previously called guess
guess :: ( forall f . Functor f => (b -> f b) -> f a ) -> Store b a
guess m = m $ \piece -> Store piece idwhich uses the fact that Store is a Functor.
Since it's an isomorphism, we gain nothing of value by choosing to use Store b a or (forall f. Functor f => (b -> f b) -> f a). With Store we have much simpler looking types, but with the second type (also called a Pretext) we don't need to carry around our Store datatype.
If we expand out what Lens b a is when using Pretexts it looks like this
type Lens a b = Functor f => a -> (b -> f b) -> f awhich, while much more confusing, can be written for any type using only fmap.
_1 :: Lens (a, b) a
_1 (a, b) inj = (,b) <$> inj aComposing Pretexts
Lets revisit the classic example for the power of a Lens, how does it look to compose it? It's somewhat difficult in this format to think about how two lenses compose, but we can do it.
(>-) :: Lens a b -> Lens b c -> Lens a c
(la >- lb) a = ...—wait! Actually, there's a trick. If we rearrange our definition of a Pretext lens.
type Lens a b = Functor f => (b -> f b) -> (a -> f a)and maybe make another type alias
type Coalg f x = x -> f xthen we can see this as a much simpler type
type Lens a b = Functor f => Coalg f b -> Coalg f aand in fact we immediately have composition using basic function composition!
(>-) :: Lens a b -> Lens b c -> Lens a c
la >- lb = la . lbThis finally is exactly the type of a Lens' you might see in the lens library. In this extended form you can compose lenses using only normal function composition (.) and you don't need any external dependencies to write a lens for a type in your code---you need only fmap.
It's worth noting that this formulation was perhaps first discovered by Twan van Laarhoven under the name "CPS Functional Reference" though it arose from a somewhat different direction.
But wait, what about s-t-a-b?
If you've used lens a lot you probably caught a slight trick I played a moment ago—I only bothered to define what Lens', a.k.a. Simple Lens, is. This whole article has focused entirely on two-parameter lenses while the ones in the library are four parameter lenses! Where does this extra complexity come from?
Well, let's try writing one of these lenses. I'll pick the same example I've carried throughout.
_1 :: Lens (a,b) a
_1 inj (a, b) = (,b) <$> inj aThat's a pretty tight definition that seems to make sense with just two parameters. Watch what happens if we forget the type line and let GHCi infer things, though.
> :t \inj (a, b) -> (,b) <$> inj a
\inj (a, b) -> (,b) <$> inj a
:: Functor f => (a -> f b) -> (a, t) -> f (b, t)We can "sort of" interpret that type as a Pretext lens, except that we need a ~ b and (a, t) ~ (b, t), each implying the other. This extra freedom indicates something very powerful about getters and setters---setting has the ability to change the type of the whole! Not completely, and not always, but the type of Lens we defined earlier completely wipes that possibility off the table.
This possibility is, in fact, the exact thing we enountered way back at the beginning of this article, write before the first "Composition" section.
We can fix it, though, by generalizing the type of our Lens to its final form that we know and love.
type Lens s t a b = Functor f => (a -> f b) -> (s -> f t)Quite obvious now isn't it? ;)
If this was an interesting read, I highly recommend Russell O'Connor's Functor is to Lens as Applicative is to Biplate which carries out this argument with much more elegance and generality while also making many more connections to related topics. He also proves the important steps which I'm simply omitting.
(Thanks to aseipp, drb226, alen_ribic, heisenbug, Jameshfisher, mutjida, and tailbalance for comments and corrections.)
[1] It's a common gag, as evidenced by PL Borat there, to call Store lenses "Costate Comonad Coalgebras". Above I walked through where "Coalgebra" and "Comonad" come from, but left "Costate" alone. It turns out there is a relationship between Store and State though it's not truly "Co-" relationship.
The "Co-" terminology comes from category theory where "Co-X" means "X with all of the arrows turned around". Category theory tends to encode all interesting properties of all things in the arrows, so this is a very important notion. Thus all the more reason to be precise in how State and Store are actually related.
Again in whirlwind fashion, one can think of all Monads as arising from the composition of two Functors which share a special relationship known as "adjunction". For the Store monad, they are as follows
( b , b -> a ) == ( b , _ ) . ( b -> _ ) $ aIf we reverse the order of these functions, we end up with State directly.
( b , b -> a ) == ( b , _ ) . ( b -> _ ) $ a
( b -> _ ) . ( b , _ ) $ a == ( b -> ( b , a ) )and obviously visa versa. I don't know of a good name for "adjunction flipped cousins", which perhaps explains the longevity of the pithy, suggestive, but ultimately incorrect term "Costate Comonad".
