Lenses can be composed like any ordinary function. We have:
Lens' a b = forall f . Functor f => (b -> f b) -> a -> f a
Now consider this example:
(.) :: Lens' Config Foo -> Lens' Foo String -> Lens' Config String
Expanding we get:
(.) :: (forall f. Functor f => (Foo -> f Foo) -> Config -> f Config)
-> (forall f. Functor f => (String -> f String) -> Foo -> f Foo)
-> (forall f. Functor f => (String -> f String) -> Config -> f Config)
And the type of function composition is:
(.) :: (b -> c) -> (a -> b) -> (a -> c)
Which lacks any universal quantification and typeclass constraints. Now my question is, how are these two features treated by the compiler/type-checker so that the function composition operator can be used for composing lenses?
My guess is that it is OK to have functions universally quantified and typeclass constraints, as long as these match for the two functions being composed.
Why don't we see what happens? Consider the following values:
(.) :: (b -> c) -> (a -> b) -> a -> c
foo :: Lens' A B
bar :: Lens' B C
The type of foo
and bar
will be expanded to:
foo :: Functor f => (B -> f B) -> A -> f A
bar :: Functor g => (C -> g C) -> B -> g B
Note that I left out the forall f.
part because it's implicit. Also, I changed the name of f
to g
for bar
to show that it's different from the f
for foo
.
Anyway, we'll first apply (.)
to foo
:
(.) :: (b -> c) -> (a -> b) -> a -> c
| | | | | |
-------- -------- | | | |
| | | | | | | |
foo :: Functor f => (B -> f B) -> A -> f A | -------- | --------
| | | | | |
(.) foo :: Functor f => (a -> B -> f B) -> a -> A -> f A
Thus, (.) foo
has the type Functor f => (a -> B -> f B) -> a -> A -> f A
. As you can see, the Functor
constraint is simply copied as is.
Now, we apply (.) foo
to bar
:
(.) foo :: Functor f => (a -> B -> f B) -> a -> A -> f A
| | | | | | | | |
| -------- | | | | | | |
| | | | | | | | | |
bar :: Functor g => (C -> g C) -> B -> g B -------- | | |
| | | | |
(.) foo bar :: Functor g => (C -> g C) -> A -> g A
Thus, (.) foo bar
has the type Functor g => (C -> g C) -> A -> g A
which means that it's a Lens' A C
. As you can see Functor f
is the same as Functor g
which is why everything works out.