Optic

(defun get-src-block-by-name (headline name)
  (car (org-element-map headline 'src-block
         (lambda (src-block)
           (when (string= (org-element-property :name src-block)
                          name)
             (org-element-property :value src-block))))))

(defun make-relations (relations)
  (when relations
    (string-join
     (mapcar (lambda (rel)
               (string-match
                "Every \\(\\w+\\) is a \\(\\w+\\)"
                rel)
               (when-let ((super (match-string 1 rel))
                          (sub (match-string 2 rel)))
                 (concat super " -> " sub)))
             (seq-remove #'string-empty-p (split-string relations "\n")))
     "\n")))

(org-element-map (org-element-parse-buffer) 'headline
  (lambda (headline)
    (when-let ((title (car (org-element-property :title headline)))
               ;(laws (get-src-block-by-name headline "laws"))
               (info (get-src-block-by-name headline "info"))
               (relations (make-relations
                           (get-src-block-by-name headline "relations"))))
      (princ (format "\n%s [shape=\"record\", label=\"{%s|%s}\"]\n%s\n"
                     title
                     title
                     (replace-regexp-in-string
                      "=>" "⇒"
                      (replace-regexp-in-string
                       "->" "→"
                       (replace-regexp-in-string "\n" "\\\\n" info)))
                     relations)))))
digraph optics {
  bgcolor="transparent"
   node [
    shape=record
    style=filled
    fillcolor=gray95
  ]
  $input
}

file:optics-diagram.png

Folklore

Optics and quantity

There is a very obscure but very useful bit of intuition that I learned from Bob Atkey in this seminar, which is that superclasses of Lens differ in the quantity that they have access to their continuation. A lens must call its continuation exactly once, an affine traversal can call its continuation at most once, and a traversal can call its continuation any finite number of times. In the van Laarhoven encoding, a lens must call its continuation at least once because there is no other way to get a value in the unknown functor f, and there is also no way to combine the result of two different calls so it can only return one of them. For affine traversals we use pointed functors, which allow us to get into the functor without calling the continuation but still do not allow us to combine the result from two different calls. For traversals we use applicatives, which do both.

https://cybercat.institute/2025/01/28/bidirectional-typechecking/

this is cut-and-pasted from @eitan.chatav from the monoidal café discord server.

Every prism and lens and monocle is a traversal. Every monocle is a traversal and a grate. Every grate and traversal is a setter.

A monocle in profunctor representation is: forall p. Monoidal p => p a b -> p s t

A traversal in lens representation is: forall f. Applicative f => (a -> f b) -> s -> f t

A grate in colens representation is: forall f. Functor f => (f a -> b) -> f s -> t

A setter is: (a -> b) -> s -> t

Types of optics

Iso

AKA Adapter in lens-family.

iso : (s -> a) -> (b -> t) -> Iso s t a b
f . from f ≡ id
from f . f ≡ id
Every Iso is a Lens.
Every Iso is a Prism.

Lens

lens : (s -> a) -> (s -> b -> t) -> Lens s t a b
view l (set l v s) ≡ v
set l (view l s) s ≡ s
set l v' (set l v s) ≡ set l v' s
Every Lens is a Traversal.
Every Lens is a Setter.
Every Lens is a Getter.

The profunctor representation clearly reflects the isomorphism.

Prism

prism : (b -> t) -> (s -> Either t a) -> Prism s t a b
Every Prism is a Traversal.

Traversal

traversal : (∀ f. Applicative f => (a -> f b) -> s -> f t) -> Traversal s t a b

Libraries

lens

idris2-lens

optics

fresnel

purescript-profunctor-lenses

monocle

References