Matthew Chan

← back

yoctolens: lenses from first principles

28 October 2017

Yesterday I whipped up a small twenty-line lens module while working on a zero-dependency library and realising that I needed lenses. I later extracted it to the yoctolens library as a joke (seriously, you should use microlens instead). While writing the module, I realised that it would serve as a pretty neat tutorial introduction to the lens library, so here it is.

To begin, let’s examine the core Lens abstraction:

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

This says, if you can convert a a to a b, then you can convert an s (containing an a ) to a t (containing a b).

To understand why the domains b and t must be in some functor f, consider the following alternative definition, in which we split the two basic lens operations apart and put them in a product:

data LensP s t a b = LensP
  { view :: s -> a
  , set :: s -> b -> t

The morphism lens takes a LensP to Lens

lens :: (s -> a)
     -- ^ Get an a from an s
     -> (s -> b -> t)
     -- ^ Set the component 'a' to a 'b', changing the outer record type
     --   to 't'
     -> Lens s t a b
     -- ^ A lens into component 'a' of record 's'.
     --   If you change 'a' to 'b', it would change the
     --   record from 's' to 't'

-- In order to produce an 'f t',
lens getter setter = \afb s ->
  fmap                -- 2. Next, we want to put the 'b' back into the record 's'.
    (setter s)        --    Lift the pure setter 'b -> t' to a setter inside the
                      --    'f' context, 'f b -> f t'
    (afb              -- 1. Run the setter on the desired field.
      (getter s)      --    The input is the field 'a' in the record 's'
    )                 --    This produces a 'b' inside the 'f' context

I like to think of the functor as a “data context” in which results are computed — a weaker notion of the “effect contexts” defined by Applicatives and Monads. By varying the specific Functor used, we can coerce the general lens type into the types of the components of LensP. That is, we can construct (partial) inverses of the lens morphism from Lens to LensP, or rather, morphisms from Lens to the dual of LensP, LensS1:

data LensS s t a b
  = View (s -> a)
  | Set  (s -> b -> t)

The basic idea is this: in order to operate on a record s, we extract the relevant field a into a context f a, perform an operation a -> b in the context functorially, then extract the result using the appropriate projection from the context.

For example, to view a component a, we need a functor f, such that evaluating f t will always produce data of type a, regardless of what t is. So we use the Const functor, which is just a box containing a value, but with a phantom type parameter to keep fmaps from actually touching the value inside.

-- Data.Functor.Const
newtype Const c a = Const { getConst :: c }
instance Functor (Const c) where
  fmap _ (Const c) = Const c
view :: Lens s t a b -> (s -> a)
view l = runConst . l Const

And to show that it does what you think it does, we calculate:

view l

{- definition of 'view l' -}
= runConst . l Const

{- definition of 'l' -}
= runConst . (\afb s -> fmap (setter s) (afb (getter s))) Const

{- beta reduction -}
= runConst . (\s -> fmap (setter s) (Const (getter s)))

{- definition of fmap for Const -}
= runConst . (\s -> (\_ (Const c) -> c) (setter s) (Const (getter s)))

{- beta reduction -}
= runConst . (\s -> (\(Const c) -> Const c) (Const (getter s)))

{- beta reduction -}
= runConst . (\s -> (Const (getter s)))

{- and if you provide input 'record' -}
= getter record

In order to set a component of type a to a new value of type b, we require a context which will let us modify the extracted data it contains, i.e. the Identity functor, which is simply a box containing a value.

-- Data.Functor.Identity
newtype Identity a = Identity { getIdentity :: a }
instance Functor Identity where
  fmap f (Identity a) = Identity (f a)

After you extract the a value into Identity a, an fmap (const b) over it will change the context to contain an Identity b. Another fmap with a concrete setter b -> t will pack the new field back into the larger record, returning a t.

set :: Lens s t a b -> (b -> s -> t)
set l b = runIdentity . l (const (Identity b))

Again, by calculation:

set l b

{- definition of 'set l b' -}
= runIdentity . l (const (Identity b))

{- definition of 'l' -}
= runIdentity . (\afb s -> fmap (setter s) (afb (getter s))) (const (Identity b))

{- beta reduction -}
= runIdentity . (\s -> fmap (setter s) ((const (Identity b)) (getter s)))

{- beta reduction -}
= runIdentity . (\s -> fmap (setter s) (Identity b))

{- definition of fmap for Identity -}
= runIdentity . (\s -> (\f (Identity a) -> Identity (f a)) (setter s) (Identity b))

{- beta reduction -}
= runIdentity . (\s -> (\(Identity a) -> Identity ((setter s) a)) (Identity b))

{- beta reduction -}
= runIdentity . (\s -> Identity ((setter s) b))

{- with input 'record' -}
= setter record b

  1. I have not explored this, but it seems to have some relation to derivatives of data types.