Abstracting away from optics

[neutropolis]

Hiding optic idioms in favor of more standard names, such as attribute, association, etc. This coq snippet is just a proof of concept.

Record one_to_one (p : Type -> Type) `{Monad p}
                  (record : forall (q : Type -> Type), Monad q -> Type) :=
{ q : Type -> Type
; A : Type
; M : Monad q
; MS : MonadState A q
; ev : record q _
; hom : lensAlgHom p q A
}.
Arguments hom [p _ record].
Arguments ev [p _ record].

Definition attribute := lensAlg'.

Notation "a ▷ f " := (f a) (at level 40, left associativity).

Record Address (p : Type -> Type) `{Monad p} := mkAddress
{ _zip  : attribute p nat
; _city : attribute p string
}.
Arguments _zip [p _].
Arguments _city [p _].

Record Person (p : Type -> Type) `{Monad p} := mkPerson
{ _name    : attribute p string
; _address : one_to_one p Address
}.
Arguments _name [p _].
Arguments _address [p _].

Definition address {p} `{Monad p} (data : Person p) :=
  hom (_address data).

Definition zip {p} `{Monad p} {data : Person p} :=
  _zip (ev (_address data)).

Definition modifyPersonZip {p} `{Monad p}
                           (f : nat -> nat)
                           (data : Person p) : p unit :=
  (data ▷ address • zip) ~ f.