| ID | ff9da715-79d4-47ac-9a0c-e396e63cb21f |
|---|---|
| DeertopiaVisibility | public |
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
}
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