Lenses

A lens onto an Option V-valued slot of α, exposed through its some-writes: read may find the slot unvalued, write always values it, and read_write is the put-get law. Lenses originate in the view-update problem ([BS81]) and were named and axiomatized in the bidirectional transformation literature ([FGM+07]). Very-well-behaved lenses are simultaneously the coalgebras of the store comonad and the algebras of the state monad (the two are adjoint); this structure carries the put-get fragment. Equivalently this could be a lawful state-monad interface (LawfulMonadStateOf, Batteries) over the Option V slot — but that demands a lawful erasing write (set none), which is unsatisfiable whenever the valuation is total (a vowel inventory in which every vowel carries the feature has no unvalued symbol to erase to). Alphabets with representable underspecification do support erasure (Function.update _ _ none); requiring it would exclude the fully-specified alphabets, so only valued writes are demanded here.

A lens-equipped alphabet is a data-word alphabet (symbol paired with a value slot). With an infinite value domain, a transducer whose state is one slot readout is a one-register machine in the sense of [KF94]; with finite V — the case here — everything stays classical finite-state, which is what lets an alphabet-generic subregular transducer compress its state to the slot readout rather than carry a full symbol (Subregular.Harmony.System runs its harmony feature through one). The "monadic" of BMRS (monadic second-order logic, one free variable) is unrelated.

Main definitions

• Lens: the read/write pair with the put-get law.
• Lens.proj: the canonical lens of a function type at an index — evaluation paired with Function.update.

structure Lens (α : Type u) (V : Type v) : Type (max u v)

A lens onto an Option V-valued slot of α, exposed through its some-writes.

• read : α → Option V

  Read the slot; none when it is unvalued.

• write : V → α → α

  Write a value into the slot.

• read_write (v : V) (s : α) : self.read (self.write v s) = some v

  Put-get: reading back a written value gives that value.

def Lens.proj {ι : Type u} {V : Type v} [DecidableEq ι] (i : ι) : Lens (ι → Option V) V

The canonical lens of a function type at an index: read is evaluation, write is Function.update.

Equations

• Lens.proj i = { read := fun (s : ι → Option V) => s i, write := fun (v : V) (s : ι → Option V) => Function.update s i (some v), read_write := ⋯ }

@[simp]

theorem Lens.proj_read {ι : Type u} {V : Type v} [DecidableEq ι] (i : ι) (s : ι → Option V) : (proj i).read s = s i

@[simp]

theorem Lens.proj_write {ι : Type u} {V : Type v} [DecidableEq ι] (i : ι) (v : V) (s : ι → Option V) : (proj i).write v s = Function.update s i (some v)