Lawful State Lenses

This file specializes polynomial-functor lenses to state lenses. In Poly, following Spivak and Niu's Polynomial Functors: A Mathematical Theory of Interaction, a dependent lens p → q is a natural transformation between polynomial functors, represented by a forward map on positions and a backward map on directions. For the self-monomial polynomial PFunctor.selfMonomial σ, both positions and directions are states of type σ. Thus a lens selfMonomial σ → selfMonomial τ has exactly the shape of a classical state lens:

• get : σ → τ, reading a view/component state;
• put : τ → σ → σ, writing an updated view/component back into the source.

The law classes below use the standard bidirectional-programming names from Foster, Greenwald, Moore, Pierce, and Schmitt's lens work: PutGet, GetPut, and the stronger PutPut law, often called very well-behavedness. We keep these laws on selfMonomial lenses rather than on arbitrary polynomial lenses: for a general PFunctor.Lens p q, the backward map returns a direction of p, not a new position of p, so the usual get/put round-trip equations are not well-typed without this state-polynomial specialization.

The binary relation IsSeparated captures the non-interference condition for two lenses with the same source. This is the condition used by Pacheco and Cunha's point-free lens calculus to justify splitting a source into two independently updatable views: updating the left and right views should not change the other view, and the two updates should commute. It is also the state-lens analogue of the separation-logic intuition behind separation lenses: two views describe spatially separated portions of a state.

References:

• David I. Spivak and Nelson Niu, Polynomial Functors: A Mathematical Theory of Interaction, Cambridge University Press, 2025.
• J. Nathan Foster, Michael B. Greenwald, Jonathan T. Moore, Benjamin C. Pierce, and Alan Schmitt, Combinators for Bidirectional Tree Transformations: A Linguistic Approach to the View-Update Problem, POPL 2005.
• Hugo Pacheco and Alcino Cunha, Generic Point-free Lenses, MPC 2010.

@[reducible, inline]

abbrev PFunctor.Lens.State (σ τ : Type u) : Type u

A state lens from source state σ to view state τ.

This is not a new kind of optic. It is the existing polynomial-functor lens between the self-monomial polynomials selfMonomial σ and selfMonomial τ. Its position map is the state get, and its direction map is the state put.

Basic operations

def PFunctor.Lens.State.mk {σ τ : Type u} (get : σ → τ) (put : τ → σ → σ) : State σ τ

Construct a state lens from a getter and a putter.

def PFunctor.Lens.State.get {σ τ : Type u} (L : State σ τ) : σ → τ

Read the view/component state selected by a state lens.

def PFunctor.Lens.State.put {σ τ : Type u} (L : State σ τ) (t : τ) (s : σ) : σ

Write an updated view/component state back into the source state.

The argument order follows the usual bidirectional-programming convention: L.put t s updates source s with new view t.

@[simp]

theorem PFunctor.Lens.State.mk_get {σ τ : Type u} (get : σ → τ) (put : τ → σ → σ) : (mk get put).get = get

@[simp]

theorem PFunctor.Lens.State.mk_put {σ τ : Type u} (get : σ → τ) (put : τ → σ → σ) (t : τ) (s : σ) : (mk get put).put t s = put t s

def PFunctor.Lens.State.id (σ : Type u) : State σ σ

The identity state lens.

@[simp]

theorem PFunctor.Lens.State.id_get {σ : Type u} (s : σ) : (State.id σ).get s = s

@[simp]

theorem PFunctor.Lens.State.id_put {σ : Type u} (t s : σ) : (State.id σ).put t s = t

def PFunctor.Lens.State.comp {σ τ υ : Type u} (L₂ : State τ υ) (L₁ : State σ τ) : State σ υ

Compose state lenses.

def PFunctor.Lens.State.«term_∘ₛ_» : Lean.TrailingParserDescr

Compose state lenses.

@[simp]

theorem PFunctor.Lens.State.comp_get {σ τ υ : Type u} (L₂ : State τ υ) (L₁ : State σ τ) (s : σ) : (L₂.comp L₁).get s = L₂.get (L₁.get s)

@[simp]

theorem PFunctor.Lens.State.comp_put {σ τ υ : Type u} (L₂ : State τ υ) (L₁ : State σ τ) (u : υ) (s : σ) : (L₂.comp L₁).put u s = L₁.put (L₂.put u (L₁.get s)) s

def PFunctor.Lens.State.fst (σ τ : Type u) : State (σ × τ) σ

The first projection state lens from a product state.

def PFunctor.Lens.State.snd (σ τ : Type u) : State (σ × τ) τ

The second projection state lens from a product state.

@[simp]

theorem PFunctor.Lens.State.fst_get {σ τ : Type u} (s : σ × τ) : (fst σ τ).get s = s.1

@[simp]

theorem PFunctor.Lens.State.fst_put {σ τ : Type u} (x : σ) (s : σ × τ) : (fst σ τ).put x s = (x, s.2)

@[simp]

theorem PFunctor.Lens.State.snd_get {σ τ : Type u} (s : σ × τ) : (snd σ τ).get s = s.2

@[simp]

theorem PFunctor.Lens.State.snd_put {σ τ : Type u} (x : τ) (s : σ × τ) : (snd σ τ).put x s = (s.1, x)

Lens laws

class PFunctor.Lens.State.IsPutGet {σ τ : Type u} (L : State σ τ) : Prop

The PutGet law for a state lens.

In the bidirectional-programming literature this is the consistency law: after writing an updated view t into a source s, reading the view back returns exactly t.

• get_put (s : σ) (t : τ) : L.get (L.put t s) = t

  Reading immediately after writing returns the written view.

class PFunctor.Lens.State.IsGetPut {σ τ : Type u} (L : State σ τ) : Prop

The GetPut law for a state lens.

In the bidirectional-programming literature this is the stability law: writing back the view already present in a source leaves the source unchanged.

• put_get (s : σ) : L.put (L.get s) s = s

  Writing the current view back into the source is a no-op.

class PFunctor.Lens.State.IsPutPut {σ τ : Type u} (L : State σ τ) : Prop

The PutPut law for a state lens.

This is the constant-complement law used in the classical view-update literature: two consecutive writes are observationally the same as the second write alone. Lenses satisfying PutGet, GetPut, and PutPut are commonly called very well-behaved.

• put_put (s : σ) (t₁ t₂ : τ) : L.put t₂ (L.put t₁ s) = L.put t₂ s

  Consecutive writes collapse to the last write.

class PFunctor.Lens.State.IsWellBehaved {σ τ : Type u} (L : State σ τ) extends L.IsPutGet, L.IsGetPut : Prop

A well-behaved state lens.

This bundles the two basic round-trip laws, PutGet and GetPut, following the standard terminology for asymmetric lenses in bidirectional programming.

• get_put (s : σ) (t : τ) : L.get (L.put t s) = t
• put_get (s : σ) : L.put (L.get s) s = s

class PFunctor.Lens.State.IsVeryWellBehaved {σ τ : Type u} (L : State σ τ) extends L.IsWellBehaved, L.IsPutPut : Prop

A very well-behaved state lens.

This extends well-behavedness with PutPut, the law saying that repeated updates keep a constant complement and collapse to the last update.

• get_put (s : σ) (t : τ) : L.get (L.put t s) = t
• put_get (s : σ) : L.put (L.get s) s = s
• put_put (s : σ) (t₁ t₂ : τ) : L.put t₂ (L.put t₁ s) = L.put t₂ s

instance PFunctor.Lens.State.id_isVeryWellBehaved {σ : Type u} : (State.id σ).IsVeryWellBehaved

instance PFunctor.Lens.State.fst_isVeryWellBehaved {σ τ : Type u} : (fst σ τ).IsVeryWellBehaved

instance PFunctor.Lens.State.snd_isVeryWellBehaved {σ τ : Type u} : (snd σ τ).IsVeryWellBehaved

instance PFunctor.Lens.State.comp_isPutGet {σ τ υ : Type u} (L₂ : State τ υ) (L₁ : State σ τ) [L₂.IsPutGet] [L₁.IsPutGet] : (L₂.comp L₁).IsPutGet

instance PFunctor.Lens.State.comp_isGetPut {σ τ υ : Type u} (L₂ : State τ υ) (L₁ : State σ τ) [L₂.IsGetPut] [L₁.IsGetPut] : (L₂.comp L₁).IsGetPut

instance PFunctor.Lens.State.comp_isWellBehaved {σ τ υ : Type u} (L₂ : State τ υ) (L₁ : State σ τ) [L₂.IsWellBehaved] [L₁.IsWellBehaved] : (L₂.comp L₁).IsWellBehaved

PutPut is intentionally not given as a generic composition instance here. Very well-behaved asymmetric lenses are closed under the classical lens composition operation, but the proof is more naturally developed alongside the larger bidirectional-lens algebra if and when it is needed.

Separation / non-interference

class PFunctor.Lens.State.IsSeparated {σ σ₁ σ₂ : Type u} (L : State σ σ₁) (R : State σ σ₂) : Prop

Non-interference for two well-behaved state lenses with a common source.

This relation says that the left and right lenses describe separated portions of the same source state. Updating either view leaves the other view unchanged, and left and right updates commute. Pacheco and Cunha use this commutation condition to justify a split combinator for two lenses with a shared concrete domain; in program-logical terminology, it is the lens-level analogue of two spatially separated state views.

• left_get_put_right (s : σ) (r : σ₂) : L.get (R.put r s) = L.get s

  Updating the right view does not change the left view.

• right_get_put_left (s : σ) (l : σ₁) : R.get (L.put l s) = R.get s

  Updating the left view does not change the right view.

• put_comm (s : σ) (l : σ₁) (r : σ₂) : L.put l (R.put r s) = R.put r (L.put l s)

  Left and right updates commute.

theorem PFunctor.Lens.State.IsSeparated.symm {σ σ₁ σ₂ : Type u} {L : State σ σ₁} {R : State σ σ₂} [h : L.IsSeparated R] : R.IsSeparated L

instance PFunctor.Lens.State.fst_snd_isSeparated {σ τ : Type u} : (fst σ τ).IsSeparated (snd σ τ)

instance PFunctor.Lens.State.snd_fst_isSeparated {σ τ : Type u} : (snd σ τ).IsSeparated (fst σ τ)