203 Advanced

Lens Laws

Functional Programming

Tutorial

The Problem

A "lens" that violates basic consistency properties is useless — if set does not set or get does not get what was set, compositions break silently. Three laws define what it means for a lens to be "lawful": GetSet (setting then getting gives back what you set), SetGet (getting then setting the same value is a no-op), and SetSet (setting twice is the same as setting once). Law-checking tests catch implementation bugs early.

🎯 Learning Outcomes

• Understand the three lens laws: GetSet, SetGet, and SetSet

• Learn how to write property-based tests that verify lens law compliance

• See examples of lawful and unlawful lenses

• Appreciate why laws matter: lawless lenses break when composed

Code Example

fn check_get_set<S: PartialEq + Clone, A: Clone>(lens: &Lens<S, A>, s: &S) -> bool {
    let a = (lens.get)(s);
    (lens.set)(a, s) == *s
}

fn check_set_get<S: Clone, A: PartialEq + Clone>(lens: &Lens<S, A>, a: A, s: &S) -> bool {
    (lens.get)(&(lens.set)(a.clone(), s)) == a
}

fn check_set_set<S: PartialEq + Clone, A: Clone>(lens: &Lens<S, A>, a: A, b: A, s: &S) -> bool {
    (lens.set)(b.clone(), &(lens.set)(a, s)) == (lens.set)(b, s)
}

(* GetSet: set (get s) s = s *)
let check_get_set lens s =
  lens.set (lens.get s) s = s

(* SetGet: get (set a s) = a *)
let check_set_get lens a s =
  lens.get (lens.set a s) = a

(* SetSet: set b (set a s) = set b s *)
let check_set_set lens a b s =
  lens.set b (lens.set a s) = lens.set b s

Key Differences

Law testing: Both languages use property-based testing (Rust: proptest/quickcheck, OCaml: QCheck) to verify lens laws over many random inputs.

Derived lenses: Lenses derived from direct field access always satisfy all three laws; manually constructed lenses (with transformations) may violate them.

Unlawful lenses: "Lenses" that fail the laws are sometimes useful (e.g., a lens with normalization) but must not be composed with other lenses.

Weaker optics: Prisms and affine traversals have analogous laws (PreviewReview, ReviewPreview) that all lawful instances must satisfy.

OCaml Approach

OCaml's optics libraries ship with property-based tests using QCheck. The laws are phrased identically — they are mathematical properties independent of the programming language. OCaml's ppx_lens-generated lenses are always lawful by construction (they directly access record fields). Hand-written lenses require manual law verification.

Full Source

#![allow(clippy::all)]
// Example 203: Lens Laws — GetSet, SetGet, SetSet

#[derive(Debug, Clone, PartialEq)]
struct Point {
    x: f64,
    y: f64,
}

struct Lens<S, A> {
    get: Box<dyn Fn(&S) -> A>,
    set: Box<dyn Fn(A, &S) -> S>,
}

impl<S, A> Lens<S, A> {
    fn new(get: impl Fn(&S) -> A + 'static, set: impl Fn(A, &S) -> S + 'static) -> Self {
        Lens {
            get: Box::new(get),
            set: Box::new(set),
        }
    }
}

// Approach 1: Lawful lenses
fn x_lens() -> Lens<Point, f64> {
    Lens::new(
        |p: &Point| p.x,
        |x: f64, p: &Point| Point { x, ..p.clone() },
    )
}

fn y_lens() -> Lens<Point, f64> {
    Lens::new(
        |p: &Point| p.y,
        |y: f64, p: &Point| Point { y, ..p.clone() },
    )
}

// Approach 2: An UNLAWFUL lens — set has a side effect
fn bad_lens() -> Lens<Point, f64> {
    Lens::new(
        |p: &Point| p.x,
        |x: f64, p: &Point| Point { x, y: p.y + 1.0 }, // mutates y!
    )
}

// Approach 3: Law verification
fn check_get_set<S: PartialEq + Clone, A: Clone>(lens: &Lens<S, A>, s: &S) -> bool {
    let a = (lens.get)(s);
    let result = (lens.set)(a, s);
    result == *s
}

fn check_set_get<S: Clone, A: PartialEq + Clone>(lens: &Lens<S, A>, a: A, s: &S) -> bool {
    let result = (lens.get)(&(lens.set)(a.clone(), s));
    result == a
}

fn check_set_set<S: PartialEq + Clone, A: Clone>(lens: &Lens<S, A>, a: A, b: A, s: &S) -> bool {
    let r1 = (lens.set)(b.clone(), &(lens.set)(a, s));
    let r2 = (lens.set)(b, s);
    r1 == r2
}

fn verify_laws<S: PartialEq + Clone, A: PartialEq + Clone>(
    name: &str,
    lens: &Lens<S, A>,
    s: &S,
    a: A,
    b: A,
) -> (bool, bool, bool) {
    let gs = check_get_set(lens, s);
    let sg = check_set_get(lens, a.clone(), s);
    let ss = check_set_set(lens, a, b, s);
    println!("{}: GetSet={} SetGet={} SetSet={}", name, gs, sg, ss);
    (gs, sg, ss)
}

#[cfg(test)]
mod tests {
    use super::*;

    #[test]
    fn test_x_lens_lawful() {
        let p = Point { x: 1.0, y: 2.0 };
        let l = x_lens();
        assert!(check_get_set(&l, &p));
        assert!(check_set_get(&l, 99.0, &p));
        assert!(check_set_set(&l, 5.0, 10.0, &p));
    }

    #[test]
    fn test_bad_lens_unlawful() {
        let p = Point { x: 1.0, y: 2.0 };
        let l = bad_lens();
        assert!(!check_get_set(&l, &p));
    }

    #[test]
    fn test_set_get_law() {
        let p = Point { x: 0.0, y: 0.0 };
        let l = y_lens();
        let result = (l.get)(&(l.set)(42.0, &p));
        assert_eq!(result, 42.0);
    }

    #[test]
    fn test_set_set_law() {
        let p = Point { x: 1.0, y: 2.0 };
        let l = x_lens();
        let r1 = (l.set)(99.0, &(l.set)(50.0, &p));
        let r2 = (l.set)(99.0, &p);
        assert_eq!(r1, r2);
    }
}

(* Example 203: Lens Laws — GetSet, SetGet, SetSet *)

type ('s, 'a) lens = {
  get : 's -> 'a;
  set : 'a -> 's -> 's;
}

(* The three lens laws:
   1. GetSet: set (get s) s = s        — setting what you got changes nothing
   2. SetGet: get (set a s) = a        — you get back what you set
   3. SetSet: set b (set a s) = set b s — setting twice = setting last value *)

type point = { x : float; y : float }

(* Approach 1: A lawful lens *)
let x_lens : (point, float) lens = {
  get = (fun p -> p.x);
  set = (fun x p -> { p with x });
}

let y_lens : (point, float) lens = {
  get = (fun p -> p.y);
  set = (fun y p -> { p with y });
}

(* Approach 2: An UNLAWFUL lens — to show what goes wrong *)
let bad_lens : (point, float) lens = {
  get = (fun p -> p.x);
  set = (fun x p -> { x; y = p.y +. 1.0 }); (* side effect! mutates y *)
}

(* Approach 3: Law verification functions *)
let check_get_set lens s =
  let result = lens.set (lens.get s) s in
  result = s

let check_set_get lens a s =
  let result = lens.get (lens.set a s) in
  result = a

let check_set_set lens a b s =
  let r1 = lens.set b (lens.set a s) in
  let r2 = lens.set b s in
  r1 = r2

let verify_laws name lens s a b =
  let gs = check_get_set lens s in
  let sg = check_set_get lens a s in
  let ss = check_set_set lens a b s in
  Printf.printf "%s: GetSet=%b SetGet=%b SetSet=%b\n" name gs sg ss;
  (gs, sg, ss)

(* === Tests === *)
let () =
  let p = { x = 3.0; y = 4.0 } in

  (* x_lens is lawful *)
  let (gs, sg, ss) = verify_laws "x_lens" x_lens p 10.0 20.0 in
  assert gs; assert sg; assert ss;

  (* y_lens is lawful *)
  let (gs, sg, ss) = verify_laws "y_lens" y_lens p 10.0 20.0 in
  assert gs; assert sg; assert ss;

  (* bad_lens violates GetSet *)
  let (gs, _sg, _ss) = verify_laws "bad_lens" bad_lens p 10.0 20.0 in
  assert (not gs); (* GetSet fails: set changes y! *)

  (* Verify the specific violations *)
  let p2 = bad_lens.set (bad_lens.get p) p in
  assert (p2.y = 5.0); (* y was mutated! *)
  assert (p2 <> p);

  print_endline "✓ All tests passed"

✓ Tests Rust test suite

#[cfg(test)]
mod tests {
    use super::*;

    #[test]
    fn test_x_lens_lawful() {
        let p = Point { x: 1.0, y: 2.0 };
        let l = x_lens();
        assert!(check_get_set(&l, &p));
        assert!(check_set_get(&l, 99.0, &p));
        assert!(check_set_set(&l, 5.0, 10.0, &p));
    }

    #[test]
    fn test_bad_lens_unlawful() {
        let p = Point { x: 1.0, y: 2.0 };
        let l = bad_lens();
        assert!(!check_get_set(&l, &p));
    }

    #[test]
    fn test_set_get_law() {
        let p = Point { x: 0.0, y: 0.0 };
        let l = y_lens();
        let result = (l.get)(&(l.set)(42.0, &p));
        assert_eq!(result, 42.0);
    }

    #[test]
    fn test_set_set_law() {
        let p = Point { x: 1.0, y: 2.0 };
        let l = x_lens();
        let r1 = (l.set)(99.0, &(l.set)(50.0, &p));
        let r2 = (l.set)(99.0, &p);
        assert_eq!(r1, r2);
    }
}

Deep Comparison

Comparison: Example 203 — Lens Laws

Law Definitions

OCaml

(* GetSet: set (get s) s = s *)
let check_get_set lens s =
  lens.set (lens.get s) s = s

(* SetGet: get (set a s) = a *)
let check_set_get lens a s =
  lens.get (lens.set a s) = a

(* SetSet: set b (set a s) = set b s *)
let check_set_set lens a b s =
  lens.set b (lens.set a s) = lens.set b s

Rust

fn check_get_set<S: PartialEq + Clone, A: Clone>(lens: &Lens<S, A>, s: &S) -> bool {
    let a = (lens.get)(s);
    (lens.set)(a, s) == *s
}

fn check_set_get<S: Clone, A: PartialEq + Clone>(lens: &Lens<S, A>, a: A, s: &S) -> bool {
    (lens.get)(&(lens.set)(a.clone(), s)) == a
}

fn check_set_set<S: PartialEq + Clone, A: Clone>(lens: &Lens<S, A>, a: A, b: A, s: &S) -> bool {
    (lens.set)(b.clone(), &(lens.set)(a, s)) == (lens.set)(b, s)
}

Unlawful Lens

OCaml

let bad_lens = {
  get = (fun p -> p.x);
  set = (fun x p -> { x; y = p.y +. 1.0 }); (* side effect! *)
}

Rust

fn bad_lens() -> Lens<Point, f64> {
    Lens::new(|p| p.x, |x, p| Point { x, y: p.y + 1.0 }) // side effect!
}

Exercises

Construct an unlawful lens that normalizes a string to lowercase on get, and show which law it violates.

Add #[cfg(test)] property-based tests using quickcheck that verify all three laws for the Point.x lens.

Verify that the composition of two lawful lenses is also lawful by testing the composed lens against all three laws.

Open Source Repos

functional-rust

View the source for this example on GitHub — OCaml and Rust side by side in the repo.

Rust