Van Laarhoven lens

A van Laarhoven lens is a lens represented as a single function that is polymorphic over functors: given a way to turn the focus $a$ into an $F a$ , it turns the whole structure $s$ into an $F s$ . Choosing the functor chooses the operation: the constant functor gives the getter and the identity functor the setter^[1]. Lenses in this form compose with ordinary function composition, and weakening the constraint from functors to applicative functors gives traversals, which compose with lenses in the same way^[2]. The representation is named after Twan van Laarhoven, who described it in 2009, and it is the basis of Haskell's lens library^[3].

§ 01

Definition

A lens from a structure $s$ to a part $a$ is usually given as a getter and a setter, $get : s \to a$ and $set : s \to a \to s$ . The van Laarhoven form is

Lens s a = \forall F . Functor F \Rightarrow (a \to F a) \to s \to F s

A lens built from a getter and a setter applies the given function to the focus and maps the setter over the result:

lens get set = λk s . fmap (set s) (k (get s))

The operations are recovered by choosing $F$ . With the constant functor $Const a x = a$ , whose $fmap$ ignores its function, the focus passes through untouched and the rebuilding is discarded, which is $get$ . With the identity functor, whose $fmap$ is application, the result is the updated structure:

view l s = getConst (l Const s) over l f s = runIdentity (l (Identity \circ f) s)

The two representations are equivalent: every function of the polymorphic type arises from a getter and a setter. Jaskelioff and O'Connor proved this as an instance of a general representation theorem, a consequence of the Yoneda lemma^[7].

Type-changing lenses

The general form lets the update change the type of the focus, and with it the type of the structure:

Lens s t a b = \forall F . Functor F \Rightarrow (a \to F b) \to s \to F t

so that a lens onto the first component of a pair can turn an (int, string) pair into a (float, string) pair. The simple $Lens s a$ is $Lens s s a a$ .

§ 02

In OCaml

The definition quantifies over a type constructor $F$ , which OCaml's type system cannot express directly. Yallop and White's lightweight higher-kinded polymorphism represents the application of a type constructor to a type as a type ('a, 'f) app, where 'f is a brand, an ordinary type that stands for the constructor^[4]. Functors become modules over a brand, and a lens is a record with a field polymorphic in the brand:

Van Laarhoven lenses in OCaml with brands, and the same lens used with four functors.

(* Higher-kinded types in OCaml: ('a, 'f) app stands for "'f applied to
   'a", where 'f is a brand, an abstract type naming a type constructor. *)
type ('a, 'f) app = ..
 
module type FUNCTOR = sig
  type f
  val map : ('a -> 'b) -> ('a, f) app -> ('b, f) app
end
 
(* A van Laarhoven lens: for every functor, lift a function on the focus
   to a function on the whole. *)
type ('s, 'a) lens = { run : 'f. (module FUNCTOR with type f = 'f) -> ('a -> ('a, 'f) app) -> 's -> ('s, 'f) app }
 
(* The identity functor gives over and set. *)
type identity
type ('a, 'f) app += Identity : 'a -> ('a, identity) app
module Identity = struct
  type f = identity
  let map f = function Identity x -> Identity (f x) | _ -> assert false
end
 
(* The constant functor gives view: the function's result is carried
   through unchanged and the rebuilding is never done. *)
(* The brand must be injective in 'r, so it is a variant, never built. *)
type 'r const = Const_brand of 'r
type ('a, 'f) app += Const : 'r -> ('a, 'r const) app
module Const (R : sig type t end) = struct
  type f = R.t const
  let map _ = function Const r -> Const r | _ -> assert false
end
 
let view (type s a) (l : (s, a) lens) (s : s) : a =
  let module C = Const (struct type t = a end) in
  match l.run (module C) (fun a -> Const a) s with Const r -> r | _ -> assert false
 
let over (type s a) (l : (s, a) lens) (f : a -> a) (s : s) : s =
  match l.run (module Identity) (fun a -> Identity (f a)) s with Identity s -> s | _ -> assert false
 
let set l a = over l (fun _ -> a)
 
(* A lens from a getter and a setter. *)
let lens get put = { run = (fun (type f) (module F : FUNCTOR with type f = f) k s -> F.map (fun a -> put s a) (k (get s))) }
 
(* Composition is function composition. *)
let ( >> ) l1 l2 = { run = (fun m k -> l1.run m (l2.run m k)) }
 
type address = { street : string; city : string }
type person = { name : string; age : int; address : address }
 
let address = lens (fun p -> p.address) (fun p a -> { p with address = a })
let city = lens (fun a -> a.city) (fun a c -> { a with city = c })
let age = lens (fun p -> p.age) (fun p a -> { p with age = a })
 
(* Any other functor works with the same lens. With option: an update
   that may fail. With lists: every alternative. *)
type ('a, 'f) app += Opt : 'a option -> ('a, [ `opt ]) app
module Opt = struct type f = [ `opt ] let map f = function Opt o -> Opt (Option.map f o) | _ -> assert false end
type ('a, 'f) app += Lst : 'a list -> ('a, [ `lst ]) app
module Lst = struct type f = [ `lst ] let map f = function Lst l -> Lst (List.map f l) | _ -> assert false end

Running it.

view (address >> city)          London
set (address >> city) "Oxford"  { Ada, 36, Oxford }
over age succ                   { Ada, 37, London }
option functor, limit 40        { Ada, 37, London }
option functor, limit 30        None
list functor                    { Ada, 36, London } { Ada, 36, Paris } { Ada, 36, Rome }
original unchanged              { Ada, 36, London }

The brands are constructors of an extensible type, so each functor adds its own constructor and matches on it. The same lens, unchanged, runs with the option functor, giving an update that can fail and leaves nothing changed if it does, and with the list functor, giving one updated record for each alternative. A lens written as a getter and setter pair would need a separate function for each of these.

§ 03

Composition

Lenses in this form are functions that transform functions, so two of them compose with function composition:

l_{1} : Lens s a, l_{2} : Lens a b ⟹ l_{1} \circ l_{2} : Lens s b

A function on the innermost focus is lifted by $l_{2}$ to a function on the middle structure, and by $l_{1}$ to a function on the whole. The order is the order in which the fields are written in a path, outermost first, which is why Haskell code reads address . city as in an object-oriented language. With getter and setter pairs, composition has to be written out and pays for a nested get on every set.

Laws

A lawful lens satisfies get-put, put-get and put-put^[5]^[8]:

set s (get s) = s get (set s a) = a set (set s a) b = set s b

In the van Laarhoven form the same conditions become laws of the kind satisfied by traversals: using the identity functor changes nothing, and running with a composed functor equals running twice. Composition of lawful lenses is lawful.

§ 04

Traversals and the optic hierarchy

Replacing $Functor$ by $Applicative$ gives a traversal, which can focus on any number of parts, since an applicative can combine the effects of many calls to the focus function^[2]:

Traversal s a = \forall F . Applicative F \Rightarrow (a \to F a) \to s \to F s

Every applicative is a functor, so every lens is a traversal, and a lens composed with a traversal is a traversal. In Haskell this subsumption is automatic, because constraints are checked at use; in OCaml an explicit coercion packs an applicative module as a functor module:

Traversals, lenses as traversals, and a composed traversal over the salaries of a company.

(* A traversal asks for an applicative instead of a functor, so it can
   visit any number of foci and combine their effects. *)
module type APPLICATIVE = sig
  include FUNCTOR
  val pure : 'a -> ('a, f) app
  val map2 : ('a -> 'b -> 'c) -> ('a, f) app -> ('b, f) app -> ('c, f) app
end
 
type ('s, 'a) traversal = { trav : 'f. (module APPLICATIVE with type f = 'f) -> ('a -> ('a, 'f) app) -> 's -> ('s, 'f) app }
 
(* Every lens is a traversal: an applicative is in particular a functor. *)
let of_lens l = { trav = (fun (type f) (module A : APPLICATIVE with type f = f) k s -> l.run (module A : FUNCTOR with type f = f) k s) }
let ( >>> ) t1 t2 = { trav = (fun m k -> t1.trav m (t2.trav m k)) }
 
(* All elements of a list. *)
let each = { trav = (fun (type f) (module A : APPLICATIVE with type f = f) k xs ->
  List.fold_right (fun x acc -> A.map2 List.cons (k x) acc) xs (A.pure [])) }
 
module IdA = struct include Identity let pure x = Identity x
  let map2 f a b = match (a, b) with Identity a, Identity b -> Identity (f a b) | _ -> assert false end
 
(* Const into the monoid of lists collects the foci. *)
module ConstList (R : sig type t end) = struct include Const (struct type t = R.t list end)
  let pure _ = Const [] let map2 _ a b = match (a, b) with Const a, Const b -> Const (a @ b) | _ -> assert false end
 
let to_list_of (type s a) (t : (s, a) traversal) (s : s) : a list =
  let module C = ConstList (struct type t = a end) in
  match t.trav (module C) (fun a -> Const [ a ]) s with Const r -> r | _ -> assert false
 
let over_all (type s a) (t : (s, a) traversal) (f : a -> a) (s : s) : s =
  match t.trav (module IdA) (fun a -> Identity (f a)) s with Identity s -> s | _ -> assert false
 
type employee = { ename : string; salary : int }
type company = { cname : string; staff : employee list }
let staff = lens (fun c -> c.staff) (fun c s -> { c with staff = s })
let salary = lens (fun e -> e.salary) (fun e s -> { e with salary = s })
let salaries = of_lens staff >>> each >>> of_lens salary

Running it.

to_list_of salaries        [100; 120; 90]
over_all salaries (+10%)   [110; 132; 99]
names via each             Ada, Charles, Mary

Viewing through a traversal uses the constant functor into a monoid, here lists, which is an applicative and collects all the foci. The standard traverse of a container is itself a traversal. Other constraints give the rest of the hierarchy: a getter asks for functors that are also contravariant, and folds for applicatives that are contravariant, so that no update is possible. Prisms and isomorphisms do not fit the functor form and need profunctors instead^[6].

§ 05

Profunctor optics

The profunctor representation generalizes the van Laarhoven one, quantifying over profunctors $P$ with some structure instead of functors^[6]:

Optic s a = \forall P . C P \Rightarrow P a a \to P s s

where the constraint $C$ determines the kind of optic: strong profunctors give lenses, choice profunctors prisms, and both together affine traversals. A van Laarhoven lens is a profunctor lens at the profunctors $a \to F b$ for functors $F$ . Riley described optics in general as a category built from a monoidal action, of which all of these are instances^[9].

§ 06

History

Lenses as getter and setter pairs came from work on bidirectional transformations and the view-update problem^[5]. Van Laarhoven described the functor-polymorphic form in a blog post in 2009^[1], and O'Connor observed in 2011 that the applicative version gives traversals and that lenses and traversals compose^[2]. Kmett's lens library, released in 2012, built a hierarchy of optics on the representation^[3]. Jaskelioff and O'Connor proved the representation theorem in 2015^[7], and Pickering, Gibbons and Wu presented the profunctor generalization in 2017^[6].