Data.Optic

Lenses: a getter and a setter carried together as one first-class value.

A Lens(s, a) names one a sitting inside an s, so reading it, writing it and modifying it are three calls against one value instead of three separate spellings of the same route. The usual constructor is the path literal: #path pos.x expands to exactly the lens call below, and the anchored form #path Player.pos.x names its root type so it sits inline with no surrounding annotation, a route of any depth in one spelling. deriving (Lens) also synthesizes a getter f_of and a functional setter with_f for every record field, and that pair is exactly what this type holds, so a field lens is also lens(hp_of, with_hp); where this module is imported the derivation goes one step further and pairs them itself, giving one lens value per field named for its type and field (Player.hp gives player_hp).

What paying for the value buys is composition and abstraction: compose_lens glues a lens into the whole to a lens into the part, and the result is an ordinary lens that a caller reads and writes without knowing how deep it reaches or which fields it crosses. A function that takes a Lens(s, a) works against any state that has an a somewhere in it.

Both halves are pure, so a lens hides no effects and every operation here is a direct call with a known shape. The Control.State bridge (gets_at, set_at, modify_at) is where that pays off for threaded state: a rule reaches one field of the state without spelling a get, a put and a record update at every step.

A well-behaved lens satisfies three laws, which the ones built here do and which a hand-written pair should be checked against: reading back what was just written returns it (view(l, lens_set(l, x, v)) == v), writing what was just read changes nothing (lens_set(l, x, view(l, x)) == x), and the last write wins (lens_set(l, lens_set(l, x, u), v) == lens_set(l, x, v)).

A Traversal(s, a) is the same idea with many foci instead of one: it reads every a in an s and rebuilds the s from replacements. Lenses and traversals compose in either order, and the result is a traversal, so a route that crosses a list stays one value. over_eff and traverse_of_eff take a modifying function carrying an open effect row, which is what a rewriting pass needs: the rule reads and writes state while the optic decides where it lands.

type Point = Point { x : Int, y : Int }
type Box = Box { at : Point, w : Int }

let box_x : Lens(Box, Int) = #path Box.at.x

fn main() =
  let b = Box { at = Point { x = 1, y = 2 }, w = 10 }
  println(view(box_x, b))
  println(view(box_x, lens_set(box_x, b, 9)))
  let bumped = exec_state(b, \() -> modify_at(#path Box.at.x, \(n) -> n + 41))
  println(bumped.at.x)

1
9
42

Opt-in: not in Base.

Types

Lens

type Lens(whole, part) = MkLens((whole) -> part, (whole, part) -> whole)

A getter and a setter for one part inside one whole, paired.

The constructor is spelled MkLens rather than Lens on purpose: constructors share one flat namespace with every module in the program, so a constructor named for its type is a name every other module has to avoid. Build one through lens, which is the door this module documents.

Traversal

type Traversal(whole, part) = MkTraversal(
  (whole) -> List(part),
  (whole, List(part)) -> whole
)

Many foci instead of one: a read of every part inside a whole, and a rebuild of the whole from replacements for exactly those parts.

The pair is the same children-and-rebuild shape a generic walk runs on, which is what keeps a traversal first-order: nothing here is a higher-rank function and no effect hides inside the value. Effects enter at the call, not in the optic, which is why traverse_of_eff can carry an open row while the traversal it runs stays a plain pair of pure functions.

The obligation on a hand-written pair: write_all is only ever handed a list as long as the one read_all returned, in the same order, and rebuilding with the parts just read has to give the original back (set_all(t, x, collect_of(t, x)) == x). Every traversal built here holds to that, and composition preserves it.

Functions and Values

lens

lens : forall a b. ((a) -> b, (a, b) -> a) -> Data.Optic.Lens(a, b)

Pair a getter with a setter. read(x) extracts the focus; write(x, v) returns x with the focus replaced by v and everything else untouched.

The two arguments have the shapes deriving (Lens) synthesizes, so a lens on a record field is the getter and the setter handed straight over.

view(lens(fst, \(p, v) -> (v, snd(p))), (1, 2))

1

view

view : forall a b. (Data.Optic.Lens(a, b), a) -> b

Read the focus of l out of x.

view(lens_snd, (1, 2))

2

lens_set

lens_set : forall a b. (Data.Optic.Lens(a, b), a, b) -> a

Replace the focus of l in x with v, leaving the rest of x alone.

Named lens_set rather than set, which Incr already exports: a program importing both would have to qualify every use of the shorter name.

lens_set(lens_fst, (1, 2), 9)

(9, 2)

over

over : forall a b. (Data.Optic.Lens(a, b), (b) -> b, a) -> a

Apply f to the focus of l in x. One read and one write, so a lens whose setter reuses a uniquely owned value updates in place.

over(lens_snd, \(n) -> n * 10, (1, 2))

(1, 20)

over_eff

over_eff : forall e0 a b. (Data.Optic.Lens(a, b), (b) -> b ! {e0}, a) -> a ! {e0}

over for a modifying function that carries effects. The row is open, so the rewrite inherits whatever the function does and nothing else: handing it a pure function gives back a pure result.

This is the shape a rewriting pass wants. A rule that reads and writes solver state while it rebuilds a term is a (a) -> a ! {State(m)}, and putting it through a lens leaves it a rule about the part, never about the whole.

fn ticked(n : Int) : Int ! {State(Int)} =
  modify(\(c) -> c + 1)
  n * 10

fn main() =
  println(run_state(0, \() -> over_eff(lens_snd, ticked, (1, 2))))

((1, 20), 1)

compose_lens

compose_lens : forall a b c. (Data.Optic.Lens(a, b), Data.Optic.Lens(b, c)) -> Data.Optic.Lens(a, c)

Focus through outer and then through inner, giving one lens that reaches the inner part of the outer whole. Composition is associative and preserves the three laws, so a route of any depth stays one ordinary lens.

let deep = compose_lens(lens_snd, lens_fst)
(view(deep, (1, (2, 3))), lens_set(deep, (1, (2, 3)), 9))

(2, (1, (9, 3)))

lens_id

lens_id : forall a. Data.Optic.Lens(a, a)

The lens that focuses the whole value: composing with it changes nothing.

lens_set(lens_id, 1, 2)

2

lens_fst

lens_fst : forall a b. Data.Optic.Lens((a, b), a)

The first component of a pair.

over(lens_fst, \(n) -> n + 1, (1, 2))

(2, 2)

lens_snd

lens_snd : forall a b. Data.Optic.Lens((a, b), b)

The second component of a pair.

over(lens_snd, \(n) -> n + 1, (1, 2))

(1, 3)

gets_at

gets_at : forall a b. (Data.Optic.Lens(a, b)) -> b ! {Control.State.State(a)}

Read the part of the threaded state that l focuses.

eval_state((1, 2), \() -> gets_at(lens_snd))

2

set_at

set_at : forall a b. (Data.Optic.Lens(a, b), b) -> Unit ! {Control.State.State(a)}

Overwrite the part of the threaded state that l focuses, leaving the rest of the state as it was.

exec_state((1, 2), \() -> set_at(lens_fst, 9))

(9, 2)

modify_at

modify_at : forall a b. (Data.Optic.Lens(a, b), (b) -> b) -> Unit ! {Control.State.State(a)}

Apply f to the part of the threaded state that l focuses. This is the one-line form of a get, a modify of one field and a put.

let deep = compose_lens(lens_snd, lens_fst)
exec_state((1, (2, 3)), \() -> modify_at(deep, \(n) -> n * 10))

(1, (20, 3))

traversal

traversal : forall a b. ((a) -> List(b), (a, List(b)) -> a) -> Data.Optic.Traversal(a, b)

Pair a reader of every focus with a rebuilder, in that order.

fn pair_kids(p : (Int, Int)) : List(Int) = [fst(p), snd(p)]

fn pair_fill(p : (Int, Int), vs : List(Int)) : (Int, Int) =
  match vs of
    Cons(a, Cons(b, _)) => (a, b)
    _ => p

fn main() =
  println(over_all(traversal(pair_kids, pair_fill), \(n) -> n + 1, (1, 2)))

(2, 3)

collect_of

collect_of : forall a b. (Data.Optic.Traversal(a, b), a) -> List(b)

Every focus of t in x, in traversal order. The view of many foci.

collect_of(each_of_list, [1, 2, 3])

[1, 2, 3]

set_all

set_all : forall a b. (Data.Optic.Traversal(a, b), a, List(b)) -> a

Rebuild x with vs standing in for its foci. The list has to be the one collect_of returned, modified elementwise: a shorter or reordered list is outside what a traversal promises.

set_all(compose_lens_traversal(lens_snd, each_of_list), (1, [2, 3]), [8, 9])

(1, [8, 9])

over_all

over_all : forall a b. (Data.Optic.Traversal(a, b), (b) -> b, a) -> a

Apply f to every focus of t in x. The over of many foci.

over_all(each_of_list, \(n) -> n * 2, [1, 2, 3])

[2, 4, 6]

traverse_of_eff

traverse_of_eff : forall e0 a b. (Data.Optic.Traversal(a, b), (b) -> b ! {e0}, a) -> a ! {e0}

over_all for a modifying function that carries effects: the result carries whatever the function does and nothing else. Foci are visited in traversal order, so the effects happen in that order too.

fn counted(n : Int) : Int ! {State(Int)} =
  modify(\(c) -> c + n)
  n * 2

fn main() =
  println(run_state(0, \() -> traverse_of_eff(each_of_list, counted, [1, 2, 3])))

([2, 4, 6], 6)

each_of_list

each_of_list : forall a. Data.Optic.Traversal(List(a), a)

Every element of a list. The traversal composition usually starts from.

over_all(each_of_list, \(n) -> n + 1, [1, 2, 3])

[2, 3, 4]

compose_lens_traversal

compose_lens_traversal : forall a b c. (Data.Optic.Lens(a, b), Data.Optic.Traversal(b, c)) -> Data.Optic.Traversal(a, c)

Focus through a lens and then through a traversal. One a inside the whole, then every b inside that a, so the result is a traversal.

collect_of(compose_lens_traversal(lens_snd, each_of_list), (1, [2, 3]))

[2, 3]

compose_traversal_lens

compose_traversal_lens : forall a b c. (Data.Optic.Traversal(a, b), Data.Optic.Lens(b, c)) -> Data.Optic.Traversal(a, c)

Focus through a traversal and then through a lens. Every a inside the whole, then the one b inside each of those, so the result is again a traversal: one focus per focus of the outer one, in the same order.

over_all(compose_traversal_lens(each_of_list, lens_fst), \(n) -> n * 10, [(1, 2), (3, 4)])

[(10, 2), (30, 4)]

modify_all_at

modify_all_at : forall a b. (Data.Optic.Traversal(a, b), (b) -> b) -> Unit ! {Control.State.State(a)}

Apply f to every part of the threaded state that t focuses, the many foci form of modify_at.

exec_state([1, 2, 3], \() -> modify_all_at(each_of_list, \(n) -> n * 2))

[2, 4, 6]