In many functional programming languages, lenses are an increasingly popular, highly composable, way of structuring bidirectional data access, i.e., operations to both read and functionally update parts of a composite object. There are many introductory tutorials about lenses on the web: one that I found to be particularly gentle is by Gabriel Gonzalez. I’ll borrow some of his ideas to introduce lenses briefly here, although, of course, I’ll work in F* rather than Haskell.

Doing it in F* raises a couple of interesting challenges. First, programming with mutable references and destructive updates is common in F*: so, unlike some other lens libraries, ours must support mutation. Second, like everything else in F*, our lens library focuses on verification: we need a way to specify and prove properties about lenses in a way that does not compromise the inherent composability of lenses—composability being their primary appeal. My solution, the lens-indexed lens, is analogous to the monad-indexed monad, a structure at the core of the design of F* itself.

Updating nested records: Clumsy, even with primitive syntax

Consider the following simple representation of a circle:

// A simple 2d point defined as a pair of integers
type point = {
  x:int;
  y:int;
}

// A circle is a point and a radius
type circle = {
  center: point;
  radius: nat
}

Using the record notation to define our types gives us some primitive syntax to access the fields of a circle and point. But, despite the primitive support, it’s not very convenient to use. Here’s some code to move the circle in the x-direction:

let move_x (delta:int) (c:circle) = 
    { c with center = {c.center with x = c.center.x + delta} }

Not pretty. But, by default, that’s basically what it looks like in most ML-like languages, including OCaml, Haskell etc. We’d much prefer to write something like c.center.x <- c.center.x + delta. Lenses are a clever way of designing a library of abstract “getters” and “setters” that allow you to do just that.

Pure lenses for composable, bidirectional access to data structures

A lens a b is pair of a getter and a setter: given an a-typed value v, a lens a b allows you to

  1. get a b-typed component out of v

  2. create another a-typed value by updating the same b-typed component in v

// A `lens a b` focuses on the `b` component of `a`
// It provides a `get` to access the component
// And a `put` to update and `a` by updating its `b` component
type lens a b = {
  get: a -> b;
  put: b -> a -> a
}

For instance, given a point, we can define two lenses, x and y, to read and write each of its fields, and lenses center and radius to focus on each of the fields of a circle.

let x : lens point int = {
    get = (fun p -> p.x);
    put = (fun x' p -> {p with x=x'})
}
let y : lens point int = {
    get = (fun p -> p.y);
    put = (fun y' p -> {p with y=y'})
}
let center : lens circle point = {
    get = (fun c -> c.center);
    put = (fun p c -> {c with center=p}}
}
let radius : lens circle int = {
    get = (fun c -> c.radius);
    put = (fun r c -> {c with radius=r}}
}

This four definitions are rather boring: one could imagine automatically generating them with a bit of meta-programming (maybe we’ll have a future post about that).

But, now comes the fun part. Lenses are easily composable: l |. m: composes lenses, building an “access path” that extends the focus of l with m. (Note #a, #b and #c below bind implicit type arguments.)

let ( |. ) #a #b #c (m:lens a b) (l:lens b c) : lens a c = {
  get = (fun x -> l.get (m.get x));
  put = (fun x y -> m.put (l.put x (m.get y)) y)
}

We can now define:

let move_x (delta:int) (c:circle) = 
    (center |. x).put ((center |. x).get c + delta) c

That may not look like much of an improvement, but even with F*’s poor support for custom operators, it’s easy to re-define a couple of common infix operators to make it better.

// `x.(|l|)`: accesses the l-focused component
let ( .(||) ) #a #b (x:a) (l:lens a b) : b = l.get x

// `x.(|l|) <- v`: updates the l-focused component of x with v
let ( .(||)<- ) #a #b (x:a) (l:lens a b) (v:b) : a = l.put v x

This lets us write:

let move_x (delta:int) (c:circle) = 
    c.(| center |. x |) <- c.(| center |. x |) + delta

which is pretty close to what we were aiming for.

Lenses on mutable data

Just to be clear, despite appearances, c.(| center |. x |) <- c.(| center |. x |) + delta does not actually mutate c. It creates a new circle that differs from c in the x field of its center, leaving the original c unchanged.

That’s nice, but we would also like a way to access and update in place the mutable fields of a record. In a language like OCaml, an object’s fields may contains mutable references to heap-allocated values. In such a setting, it’s easy to define a lens like:

let deref : lens (ref a) a = {
    get = (fun r -> !r);
    put = (fun v r -> r := v)
}

But, this won’t do in F*: for starters, the get and put fields of a lens are expected to be pure, total functions and the fields of deref are certainly not pure: they read or write to the heap. F*, like Haskell, forces us to confess to our impurities.

If we were in Haskell, we could define the type of a stateful lens (in F* pseudo-syntax) like so:

type st_lens a b = {
     st_get : a -> ST b;
     st_put:  b -> a -> ST a
}

And we could give deref the type st_lens (ref a) a. But, this still won’t do in F*. With verification in mind, stateful computations must

  1. be accompanied by a precise specification, and

  2. whatever specification we give a stateful lens, it needs to be stable under composition: the composition of stateful lenses needs to also be a stateful lens (e.g., we should be able to define a double dereference to read an write an a from/to a ref (ref a), by composing lens from ref (ref a) to a ref a and again from a ref a to an a).

A precise specification for the deref lens

Let’s look again at the get and put of the deref lens.

let get (r:ref a) = !r
let put (v:a) (r:ref a) = r := v

These two functions are the most primitive operations available on references and, of course, we can give them precise specifications in F*.

val get (r:ref a) 
    : ST a
    (requires (fun h -> True))
    (ensures  (fun h0 x h1 -> h0==h1 /\ x == sel h0 r))

val put (v:a) (r:ref a)
    : ST unit 
    (requires (fun h -> True))
    (ensures  (fun h0 () h1 -> h1 == upd h0 r v))

Here ST a (requires pre) (ensures post) is the type of a stateful computation whose pre-condition on the input heap is pre, and whose post-condition post relates the initial heap h0 to the result and the final heap h1.

Viewing the spec of a stateful lens as a pure lens

The specification of get describes the return value by getting it from the initial heap h0 and the reference r; the spec of put describes the final heap h1 by putting a new value into the initial heap h0. Viewed differently, the specification of get and put is itself a lens, a lens between a pair of heap * ref a and an a. Let’s call such a lens an hlens.

let hlens a b = lens (heap * a) b
let ref_hlens #a : hlens (ref a) a = {
    get = (fun (h,r) -> sel h r);
    put = (fun v (h, r) -> upd h r v)
}

We can then specify stateful lenses that perform destructive updates based on their underlying hlenses.

// st_lens l: a stateful lens between a and b
type st_lens #a #b (l:hlens a b) = {
   st_get : (x:a
         -> ST b
            (requires (fun h -> True))
            (ensures  (fun h0 x h1 -> h0==h1 /\ y == l.get (h0, x))));

   st_put : (y:b 
         -> x:a 
         -> ST a
            (requires (fun h -> True))
            (ensures  (fun h0 x' h1 -> h1, x' == l.put y (h0, x)))
}

Given an l:hlens a b, an st_lens l is a stateful lens between a and b that can perform destructive updates and whose behavior is fully specified by l.

And we can finally specify the deref stateful lens:

let deref : st_lens ref_hlens = {
    st_get = (fun r -> !r);
    st_put = (fun v r -> r := v)
}

Composing stateful lenses

Happily, stateful lenses compose nicely: the composition of an st_lens l and an st_lens m is fully specified by l |. m, the composition of l and m.

let ( |.. ) #a #b #c (#l:hlens a b) (#m:hlens b c)
                     (sl:st_lens l) (sm:st_lens m)
    : st_lens (l |. m) = {
      st_get = (fun (x:a) -> sm.st_get (sl.st_get x));
      st_put = (fun (z:c) (x:a) -> sl.st_put (sm.st_put z (sl.st_get x)) x)
}

And any pure lens l is easily lifted to a stateful lens whose specification is the trivial lifting of l itself to an hlens.

let as_hlens #a #b (l:lens a b) : hlens a b = {
    get = (fun (h, x) -> x.(|l|));
    put = (fun y (h, x) -> h, (x.(|l|) <- y));
}

let as_stlens #a #b (l:lens a b) : stlens (as_hlens l) = {
    st_get = (fun (x:a) -> x.(|l|));
    st_put = (fun (y:b) (x:a) -> x.(|l|) <- y)
}

These liftings of pure lenses to stateful lenses are convenient to fold in as part of the lens composition, lifting pure lenses as they are composed with stateful lenses, either on the left or the right.

let ( |^. ) #a #b #c (m:lens a b) (#l:hlens b c) (sl:stlens l) =
    (as_stlens m) |.. sl

let ( |.^ ) #a #b #c (#l:hlens a b) (sl:stlens l) (m:lens b c) =
    sl |.. as_stlens m

We can also define some shorthands, x.[sl] and x.[sl] <- v, to apply a stateful lens sl to access or mutate an object x.

let ( .[]   ) #a #b (#l:hlens a b) (x:a) (sl:stlens l) =
    sl.st_get x
let ( .[]<- ) #a #b (#l:hlens a b) (x:a) (sl:stlens l) (y:b) = 
    let _ = sl.st_put y x in ()

Stateful lenses at work

We can now revisit our original example of circles and points, this time defining them to support destructive updates.

type point = {
  x:ref int;
  y:ref int;
}
type circle = {
  center: ref point;
  radius: ref nat
}

These are just the types we had before, but now with mutable references in each field. Pure lenses to access and mutate each field are easy to define, as before.

let center : lens circle (ref point) = {
  get = (fun c -> c.center);
  put = (fun p c -> {c with center = p})
}
let x : lens point (ref int) = {
  get = (fun p -> p.x);
  put = (fun x p -> {p with x = x})
}
...

Using a combination of pure and stateful lenses, we can mutate the x field of a circle’s center easily.

let move_x delta c
   = let l = center |^. deref |.^ x |.. deref in
     c.[l] <- c.[l] + delta

Notice that since a lens is a first-class value, the access path from a circle to the contents of the x-field of its center is a value that can be constructed once, bound to a variable (l) and re-used as needed.

Of course, we also want to be able to specify move_x. But, since every stateful lens is fully specified by a pure lens, specifying move_x is now pretty easy in terms of its action on the heap. Here’s the type of move_x:

val move_x (delta:int) (c:circle) : ST unit
  (requires (fun _ -> True))
  (ensures  (fun h0 _ h1 ->
             let l = center |^. deref |.^ x |.. deref in
             (h1, c) == (c.(h0, l) <- c.(h0, l) + delta)))

We can specify it using just the same lens that we used in its implementation, except using the hlens that’s the pure counterpart of the stateful lens l. Since the type of a stateful lens always mentions its corresponding hlens, we can easily define functions to to specify a stateful lenses effect.

let ( .() )   #a #b (#l:hlens a b) (x:a) (hs:(heap * stlens l)) = l.get (fst hs, x)
let ( .()<- ) #a #b (#l:hlens a b) (x:a) (hs:(heap * stlens l)) (y:b) = l.put y (fst hs, x)

Without these lenses, here’s the mouthful we’d have had to write instead.

let move_x2 (delta:int) (c:circle) : ST unit
  (requires (fun _ -> True))
  (ensures  (fun h _ h' ->
             let rp = c.center in
             let p = sel h rp in
             let rx = p.x in
             let h1 = upd h rx (sel h rx + delta) in
             let p = sel h1 rp in
             let h2 = upd h1 rp ({p with x = rx}) in
             h' == h2))
   = c.[center |^. v |.^ x |.. v] <- (c.[center |^. v |.^ x |.. v] + delta)

Worse than the verbosity, it actually took me nearly half an hour to write this specification, requiring peeling back the layers of abstraction to figure out the exact order in which the reads and writes were occurring!

Takeaways

Lenses are a powerful way to structure data access and mutation. With stateful lens-indexed lenses, we can use them to implement and specify destructive updates of nested data structures in a compact and composable manner.

You can see a fully detailed code listing for this blog post here.

Lens libraries in other languages are much more extensive—I’ve merely scratched the surface ground out the most basic lens combinators.