Lensindexed lenses
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 lensindexed lens, is analogous to the monadindexed 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 MLlike 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

get
ab
typed component out ofv

create another
a
typed value by updating the sameb
typed component inv
// 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 metaprogramming (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 redefine a couple of common infix operators to make it better.
// `x.(l)`: accesses the lfocused component
let ( .() ) #a #b (x:a) (l:lens a b) : b = l.get x
// `x.(l) < v`: updates the lfocused 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 heapallocated 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* pseudosyntax) 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

be accompanied by a precise specification, and

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 aref (ref a)
, by composing lens fromref (ref a)
to aref a
and again from aref a
to ana
).
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 precondition on the input heap is pre
, and whose
postcondition 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 firstclass 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 reused 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 lensindexed 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.