Notes on optics

A first notion of what a lawful mixed optic should be is to push both parts of the optic into the same category and consider lawfulness there.

In the case of monadic lenses for copointed monads, this can give a reasonable notion of laws.

An interesting consideration is to see what happens if we extend the Optic formula on the product to a more symmetric case. \[ \int^{C,D} \mathbf{C}(D \times S, C \times A) \times \mathbf{C}(C \times B, D \times T) \] In the same way that lenses give teleological categories, this should give a category with formal cups and caps. I am interested on this because that means it would be a way of constructing models of DisCoCat following this idea by Delpeuch.

I have now realized that this is in fact the category of learners as described by Fong and Johnson. Can we use learners in DisCoCat?

A kaleidoscope is the optic for applicative functors. Using the free applicative construction (from Capriotti-Kaposi, for instance), we can show their concrete representation is the following.

type Kaleidoscope s t a b = forall n . (Vec n a -> b) -> (Vec n s -> t)

If we take lenses where complements are monad algebras or prisms where the complements are comonad coalgebras, we get monadic lenses and comonadic prisms, that we can write as

type MonLens m s t a b = (s -> a , m s -> b -> t)
type ComonPrism n s t a b = (s -> n t + a , b -> t)

I am not sure if these optics are elsewhere in the literature, but I have not been able to find them so far.

At the intersection between a lens and a grate there should be an optic that I have started to call glass. If the pseudomonoid action that describes a lens is (c × _) and the one for glass is (c -> _), the action that we want to get should be the one given by the coproduct pseudomonoid.

We rewrite the action of every word c₁d₁ ... cₖdₖ on some object a as follows, for some e,f ∈ C, a bicartesian closed category.

  d₁ × (c₁ -> d₂ × (c₂ -> ... x))  ≅
  d₁ × (c₁ -> d₂) × (c₁ × c₂ -> ... x)  ≅
  e × (f -> x)

And we derive the concrete representation.

  ∃ c,d .  (s -> (c × (d -> a))) × (c × (d -> b) -> t)  ≅
  ∃ c,d .  (s -> c) × (s -> (d -> a)) × (c × (d -> b) -> t)  ≅
  ∃ d   .  (s -> (d -> a)) × (s × (d -> b) -> t)  ≅
  ∃ d   .  (d -> (s -> a)) × (s × (d -> b) -> t)  ≅
  (s × ((s -> a) -> b) -> t)  ≅
  ((s -> a) -> b) -> s -> t

My intuition at the moment is “If from a getter you can create a b, then you can update s to t”, which apparently also rhymes.