Skip to content

Instantly share code, notes, and snippets.

@rntz

rntz/lenses?

Created August 11, 2022 14:42
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save rntz/739bfcc2011cd29956dfc44a700da7c9 to your computer and use it in GitHub Desktop.
Save rntz/739bfcc2011cd29956dfc44a700da7c9 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
lenses?
chart
(A,A') -> (B,B')
lens
get : A -> B
put : A × B' -> A'
chart
get : A -> B
weird : A × A' -> B'
A' = ΔA
B' = ΔB
chart-as-incrementalization
f: A → B
f': A × ΔA → ΔB
RA ⊆ ΔA × A × A
RA(dx, x, y) means "dx changes x into y"
f' is a derivative of f iff:
when RA(dx, x, y)
then RB(f'(x,dx), f x, f y)
ie: f' tells me how (f x) changes as x changes
lens
f: A → B
f': A × ΔB → ΔA
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment