Are lenses and bi-directional patterns the same concept?

Learn
3

That’s nice to know, but I am not after an over-arching optics concept, even if it can fit any pattern. Like last time, I wonder: what are the actual ways to define a lens, given the structure of a data type? In other words, given an algebra of type constructions (e.g. products, coproducts) is there an algebra of lens constructions that can describe any lens? For example:

{-# LANGUAGE GADTs #-}
data Lens s a where
   IdLens :: Lens s s
   -- ^ complement: ()
   Assoc :: Lens s a -> Lens a b -> Lens s b
   -- ^ complement: product of the complements
   -- ((b,c),c') ~ (b,(c,c'))
   Fst :: Lens s a -> Lens (s,c) a
   Snd :: Lens s a -> Lens (c,s) a
   Distr :: Lens s a -> Lens t a -> Lens (Either s t) a
   -- ^ (a,c) + (a,c') ~ (a,c+c')
   Null :: Lens Void a

We can therefore make an analogy: Lens s a is like the assertion a divides s for numbers. Each of the above constructors corresponds to a theorem about divisibility.