Characterizations of Partial Well-Behaved Lenses
summary
Defines five lens laws for partial functions, proves implication maps among them, and characterizes two concrete cases: when only put is partial the Fischer et al. conditions still guarantee a corresponding total get, and when both get and put are partial those conditions fail so a new law weak Source stability is introduced and used to restore characterization. Provides formal proofs of equivalences, exhibits which put-side properties (for example put injectivity and put potency) suffice, and discusses consequences for BX-style update languages.
AI-written summary · about
chapters (12)
- 0:00Introduction
- 1:25BX and lenses basics
- 3:57Well-behaved lenses
- 7:14Partial functions problem
- 8:17Lens laws for partials
- 11:04Implications with partial put
- 13:13Only put partial
- 14:18Both get and put partial
- 16:25Key result: partial get/put
- 17:28Further work
- 18:32Main findings
- 18:55Q&A
related talks
45mBidirectional Data Transformations
17mOptimal Predicate Pushdown Synthesis
46mMay Your Data Ever Be Coherent
19mHomomorphism Calculus for User-Defined Aggregations
15mHarnessing LLMs for Scalable Data Minimization
35mScalable data pipelines with shapeless and cats
13mGradually Structured Data
27mThe Essence of Online Data Processing