Logo Questions Linux Laravel Mysql Ubuntu Git Menu
 

Isn't it redundant for Control.Lens.Setter to wrap types in functors?

Tags:

I'm watching the Control.Lens introduction video.
It makes me wonder why is it needed for the Setter type to wrap things in functors.
It's (roughly) defined like this:

type Control.Lens.Setter s t a b = (Functor f) => (a -> f a) -> s -> f t

Let's say I have a data called Point that's defined like this:

data Point = Point { _x :: Int, _y :: Int } deriving Show

Then I can write my own xlens like this:

type MySetter s t a b = (a -> b) -> s -> t
xlens :: MySetter Point Point Int Int
xlens f p = p { _x = f (_x p) }

And I can use it like this:

p = Point 100 200
xlens (+1) p -- Results in Point { _x = 101, _y = 200 }

By using Control.Lens, the same effect is achieved by:

over x (+1) p

where the following stands:

x :: Functor f => (Int -> f Int) -> Point -> f Point
over :: Setter Point Point Int Int -> (Int -> Int) -> Point -> Point

So my question is, since the same effect can be achieved in a simpler manner, why Control.Lens wraps things in functors? It looks redundant to me, since my xlens does the same as Control.Lens's over x.

Just for the record, I can also chain my lenses in the same manner:

data Atom = Atom { _element :: String, _pos :: Point } deriving Show
poslens :: MySetter Atom Atom Point Point
poslens f a = a { _pos = f (_pos a) }

a = Atom "Oxygen" p
(poslens . xlens) :: (Int -> Int) -> Atom -> Atom
(poslens . xlens) (+1) a -- Results in Atom "Oxygen" (Point 101 200)
like image 554
qwe Avatar asked Jun 06 '16 20:06

qwe


1 Answers

This is a wonderful question and will require a little bit of unpacking.

I want to gently correct you on one point right off the bat: the type of Setter in the lens package as of recent versions is

type Setter s t a b = (a -> Identity b) -> s -> Identity t

No Functor in sight ... yet.

That does not invalidate your question however. Why isn't the type simply

type Setter s t a b = (a -> b) -> s -> t

For that we first have to talk about Lens.

Lens

A Lens is a type that allows us to perform both a getter and a setter operation. These two combined form one beautiful functional reference.

A simple pick for Lens type is:

type Getter s a = s -> a
type Setter s t a b = (a -> b) -> s -> t
type Lens s t a b = (Getter s a, Setter s t a b)

This type however is deeply unsatisfying.

  • It fails to compose with ., which is perhaps the single best selling point of the lens package.
  • It is rather memory inefficient to build lots of tuples, only to rip them apart later.
  • The big one: functions that take getters (like view) and setters (like over) cannot take lenses because their types are so different.

Without that last problem solved why even bother writing a library? We would hate for users to have to constantly think about where they are in the UML hierarchy of optics, adjusting their function calls each time they move up or down.

The question of the moment is then: is there a type we can write down for Lens such that it is automatically both a Getter and a Setter? And for that we have to transform the types of Getter and Setter.

Getter

  • First note that s -> a is equivalent to forall r. (a -> r) -> s -> r. This transformation into continuation passing style is far from obvious. You might be able to intuit this transformation as this: "A function of type s -> a is a promise that given any s you can hand me an a. But that should be equivalent to the promise that given a function that maps a to r you can hand me a function that maps s to r also." Maybe? Maybe not. There might be a leap of faith involved here.

  • Now define newtype Const r a = Const r deriving Functor. Note that Const r a is the same as r, mathematically and at runtime.

  • Now note that type Getter s a = forall r. (a -> r) -> s -> r can be rewritten as type Getter s t a b = forall r. (a -> Const r b) -> s -> Const r t. Though we introduced new type variables and mental anguish for ourselves this type is still mathematically identical to what we started out with (s -> a).

Setter

  • Define newtype Identity a = Identity a. Note that Identity a is the same as a, mathematically and at runtime.

  • Now note that type Setter s t a b = (a -> Identity b) -> s -> Identity t is still identical to the type that we started out with.

All together

With this paperwork out of the way, can we unify setters and getters into one single Lens type?

type Setter s t a b = (a -> Identity b) -> s -> Identity t
type Getter s t a b = forall r. (a -> Const r b) -> s -> Const r t

Well this is Haskell and we can abstract out the choice of Identity or Const to a quantified variable. As the lens wiki says, all that Const and Identity have in common is that each is a Functor. We then choose that as a sort of point of unification for these types:

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

(There are other reasons to choose Functor too, such as to prove the laws of functional references by using free theorems. But we will handwave a little bit here for time.) That forall f is like the forall r. above – it lets consumers of the type choose how to fill the variable in. Fill in an Identity and you get a setter. Fill in a Const a and you get a getter. It was by choosing small and careful transformations along the way that we were able to arrive at this point.

Caveats

It might be important to note that this derivation is not the original motivation for the lens package. As the Derivation wiki page states explains, you can start from the interesting behavior of (.) with certain functions and tease out optics from there. But I think this path we carved out is a little better at explaining the question you posed, which was a big question I had starting out too. I also want to refer you to lens over tea, which provides yet another derivation.

I think these multiple derivations are a good thing and a kind of dipstick for the healthiness of the lens design. That we are able to arrive at the same elegant solution from different angles means that this abstraction is robust and well-supported by different intuitions and mathematics.

I also lied a little bit about the type of Setter in recent lens. It's actually

type Setter s t a b = forall f. Settable f => (a -> f b) -> s -> t b

This is another example of abstracting the higher-order type in optical types to provide the library user a better experience. Almost always f will be instantiated to Identity, as there is an instance Settable Identity. However every now and then you might want to pass setters to the backwards function, which fixes f to be Backwards Identity. We can probably categorize this paragraph as "more information about lens than you probably wanted to know."

like image 54
hao Avatar answered Oct 20 '22 05:10

hao