Program Adverbs and Tlon Embeddings
summary
Proposes program adverbs as reified functor classes (applicative/selective/monad) that embed effects LiftA2 and Embed constructors to capture static vs dynamic control and to retain syntactic shape; defines Tlön embeddings that are less expressive than free monads so they forbid unwanted dynamic control flows and preserve parallelism. Implements composable adverbs via à-la-carte/church encodings, verifies properties in Coq artifact, and demonstrates two case studies (Haxl-style parallelism and a network server) that the approach scales and is mechanized.
AI-written summary · about
chapters (9)
- 0:00Start
- 0:42Verifying Existing Program
- 1:24Challenges of Embedding: Simplicity
- 3:10Challenges of Embedding: Modularity
- 4:55An Example: Circuits
- 6:55Free Monads and Mixed Embeddings
- 11:14Classes of Functors and Program Adverbs
- 11:41What about Modularity?
- 12:31Computation Pattern à la Carte
related talks
45mA categorical view of computational effects
01h 14mBeyond Free Monads
21mEffectful Lenses: There and Back with Different Monads
25mAdapTT: Functoriality for Dependent Type Casts
33mExtensible Effects: A Leaner Cake for Purely Functional Code
21mCompositions for Free: Reasoning about Effectful Lenses
26mAbstraction Functions as Types
43mFunctional Programming with Effects