Free Lenses for Higher-Kinded Data

In the previous blog post, we discussed higher-kinded data (HKD), the technique of parameterizing your data types by something of kind * -> *, and subsequently wrapping each of its fields by this parameter. The example we used previously was transforming this type:

data Person = Person
  { pName :: String
  , pAge  :: Int
  } deriving (Generic)

into its HKD representation:

data Person' f = Person
  { pName :: HKD f String
  , pAge  :: HKD f Int
  } deriving (Generic)

Recall that HKD is a type family given by

type family HKD f a where
  HKD Identity a = a
  HKD f        a = f a

which is responsible for stripping out an Identity wrapper. This means we can recreate our original Person type via type Person = Person' Identity, and use it in all the same places we used to be able to.

Our previous exploration of the topic unearthed some rather trivial applications of this approach; we generated a function validate :: f Maybe -> Maybe (f Identity) which can roughly be described as a “type-level sequence.” In fact, in the comments, Syrak pointed out we can implement this function in a less-round-about way via gtraverse id.

So, how about we do something a little more interesting today? Let’s generate lenses for arbitrary product types.

In my opinion, one of the biggest advantages of the HKD approach is it answers the question “where can we put this stuff we’ve generated?” Generating lenses generically is pretty trivial (once you have wrapped your head around the mind-boggling types), but the harder part is where to put it. The lens package uses TemplateHaskell to generate new top-level bindings so it has somewhere to put the lenses. But we have HKD.

Recall, our Person' type:

data Person' f = Person
  { pName :: HKD f String
  , pAge  :: HKD f Int
  } deriving (Generic)

By substituting f ~ Lens' (Person' Identity), we’ll have pName :: Lens' (Person' Identity) String, which is exactly the type we need. All of a sudden it looks like we have an answer to “where should we put it”: inside our original structure itself. If we can generate a record of type Person' (Lens' (Person' Identity), destructuring such a thing will give us the lenses we want, allowing us to name them when we do the destructuring. Cool!

Unfortunately, we’re unable to partially apply type-synonyms, so we’ll need to introduce a new type constructor that we can partially apply. Enter LensesFor:

data LensFor s a = LensFor
  { getLensFor :: Lens' s a
  }

The next step is to think really hard about what our lens-providing type-class should look like. At the risk of sounding like a scratched CD in a walkman, I consider the design of the typeclass to be by far the hardest part of this approach. So we’ll work through the derivation together:

I always begin with my “template” generic-deriving class:

class GLenses i o where
  glenses :: i p -> o p

where p is a mysterious existentialized type parameter “reserved for future use” by the GHC.Generics interface. Recall that i is the incoming type for the transformation (not the original Person' type), and o is correspondingly the output type of the transformation.

Since lenses don’t depend on a particular “input” record – they should be able to be generated ex nihilo – we can drop the i p parameter from glenses. Furthermore, since eventually our lenses are going to depend on our “original” type (the Person' in our desired LensesFor (Person' Identity)), we’ll need another parameter in our typeclass to track that. Let’s call it z.

class GLenses z i o where
  glenses :: o p

As far as methods go, glenses is pretty unsatisfactory right now; it leaves most of its type parameters ambiguous. No good. We can resolve this issue by realizing that we’re going to need to actually provide lenses at the end of the day, and because GHC.Generics doesn’t give us any such functionality, we’ll need to write it ourselves. Which implies we’re going to need to do structural induction as we traverse our generic Representation.

The trick here is that in order to provide a lens, we’re going to need to have a lens to give. So we’ll add a Lens' to our glenses signature – but what type should it have? At the end of the day, we want to provide a Lens' (z Identity) a where a is the type of the field we’re trying to get. Since we always want a lens starting from z Identity, that pins down one side of our lens parameter.

class GLenses z i o where
  glenses :: Lens' (z Identity) _ -> o p

We still have the notion of an input to our glenses, which we want to transform into our output. And that’s what tears it; if we have a lens from our original type where we currently are in our Generic traversal, we can transform that into a Generic structure which contains the lenses we want.

class GLenses z i o where
  glenses :: Lens' (z Identity) (i p) -> o p

Don’t worry if you’re not entirely sure about the reasoning here; I wasn’t either until I worked through the actual implementation. It took a few iterations to get right. Like I said, figuring out what this method should look like is by far the hardest part. Hopefully going through the rest of the exercise will help convince us that we got our interface correct.

With our typeclass pinned down, we’re ready to begin our implementation. We start, as always, with the base case, which here is “what should happen if we have a K1 type?” Recall a K1 corresponds to the end of our generic structural induction, which is to say, this is a type that isn’t ours. It’s the HKD f String in pName :: HKD f String from our example.

So, if we have an a wrapped in a K1, we want to instead produce a LensFor (z Identity) a wrapped in the same.

instance GLenses z (K1 _x a)
                   (K1 _x (LensFor (z Identity) a)) where
  glenses l = K1                            -- [3]
            $ LensFor                       -- [2]
            $ \f -> l $ fmap K1 . f . unK1  -- [1]
  {-# INLINE glenses #-}

Egads there’s a lot going on here. Let’s work through it together. In [1], we transform the lens we were given (l) so that it will burrow through a K1 constructor – essentially turning it from a Lens' (z Identity) (K1 _x a) into a Lens' (z Identity) a. At [2], we wrap our generated lens in the LensFor constructor, and then in [3] we wrap our generated lens back in the GHC.Generics machinery so we can transform it back into our HKD representation later.

And now for our induction. The general idea here is that we’re going to need to transform the lens we got into a new lens that focuses down through our generic structure as we traverse it. We can look at the M1 case because it’s babby’s first instance when compared to K1:

instance (GLenses z i o)
    => GLenses z (M1 _a _b i) (M1 _a _b o) where
  glenses l = M1 $ glenses $ \f -> l $ fmap M1 . f . unM1
  {-# INLINE glenses #-}

Here we’re saying we can lift a GLenses z i o over an M1 constructor by calling glenses with an updated lens that will burrow through the M1-ness. This transformation is completely analogous to the one we did for K1. Once we have our generated lenses, we need to re-wrap the structure in an M1 constructor so we can transform it back into our HKD representation.

The product case looks a little trickier, but it’s only because GHC.Generics doesn’t provide us with any useful un/wrapping combinators for the (:*:) constructor.

instance (GLenses z i o, GLenses z i' o')
    => GLenses z (i :*: i') (o :*: o') where
  glenses l = glenses (\f -> l (\(a :*: b) -> fmap (:*: b) $ f a))
          :*: glenses (\f -> l (\(a :*: b) -> fmap (a :*:) $ f b))
  {-# INLINE glenses #-}

We finish it off with the trivial instances for V1 and U1:

instance GLenses z V1 V1 where
  glenses l = undefined

instance GLenses z U1 U1 where
  glenses l = U1

And voila! Our induction is complete. Notice that we did not write an instance for (:+:) (coproducts), because lenses are not defined for coproduct types. This is fine for our Person' case, which has no coproducts, but types that do will simply be unable to find a GLenses instance, and will fail to compile. No harm, no foul.

With this out of the way, we need to write our final interface that will use all of the generic machinery and provide nice access to all of this machinery. We’re going to need to call glenses (obviously), and pass in a Lens' (z Identity) (Rep (z Identity)) in order to get the whole thing running. Then, once everything is build, we’ll need to call to to turn our generic representation back into the HKD representation.

But how can we get a Lens'(z Identity) (Rep (z Identity))? Well, we know that GHC.Generics gives us an isomorphism between a type and its Rep, as witnessed by to and from. We further know that every Iso is indeed a Lens, and so the lens we want is just iso from to. Our function, then, is “simply”:

{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications    #-}

getLenses
    :: forall z
     . ( Generic (z Identity)
       , Generic (z (LensFor (z Identity)))
       , GLenses z (Rep (z Identity))
                   (Rep (z (LensFor (z Identity))))
       )
    => z (LensFor (z Identity))
getLenses = to $ glenses @z $ iso from to

where I just wrote the z (LensFor (z Identity)) part of the type signature, and copy-pasted constraints from the error messages until the compiler was happy.

OK, so let’s take it for a spin, shall we? We can get our lenses thusly:

Person (LensFor lName) (LensFor lAge) = getLenses

Yay! Finally we can ask GHCi for their types, which is a surprisingly satisfying experience:

> :t lName
lName :: Lens' (Person' Identity) String

Pretty sweet, ne? Now that getLenses has been implemented generically, it can become library code that will work for any product-type we can throw at it. Which means free lenses without TemplateHaskell for any types we define in the HKD form.

This HKD pattern is useful enough that I’ve begun implement literally all of my “data” (as opposed to “control”) types as higher-kinded data. With an extra type synonym type X = X' Identity, and {-# LANGUAGE TypeSynonymInstances #-}, nobody will ever know the difference, except that it affords me the ability to use all of this stuff in the future should I want to.

As Conal says, all of this stuff might not necessarily be “for free” but at the very least, it’s “already paid for.”

More shoutouts to Travis Athougies, whose sweet library beam uses this approach to generate lenses for working with SQL tables. I consulted the beam source more than a couple times in writing this post. Thanks again, Travis!