Program Adverbs and Tlön Embeddings
arXiv:2207.05227 · doi:10.1145/3547632
Abstract
Free monads (and their variants) have become a popular general-purpose tool for representing the semantics of effectful programs in proof assistants. These data structures support the compositional definition of semantics parameterized by uninterpreted events, while admitting a rich equational theory of equivalence. But monads are not the only way to structure effectful computation, why should we limit ourselves? In this paper, inspired by applicative functors, selective functors, and other structures, we define a collection of data structures and theories, which we call program adverbs, that capture a variety of computational patterns. Program adverbs are themselves composable, allowing them to be used to specify the semantics of languages with multiple computation patterns. We use program adverbs as the basis for a new class of semantic embeddings called Tlön embeddings. Compared with embeddings based on free monads, Tlön embeddings allow more flexibility in computational modeling of effects, while retaining more information about the program's syntactic structure.
arXiv commentAccepted by ICFP 2022. 32 pages. Extended version
References in corpus (9)
- General Recursion via Coinductive Types
- Interaction Trees: Representing Recursive and Impure Programs in Coq
- From C to Interaction Trees: Specifying, Verifying, and Testing a Networked Server
- Total Haskell is Reasonable Coq
- SteelCore: An Extensible Concurrent Separation Logic for Effectful Dependently Typed Programs
- Free Applicative Functors
- An Equational Theory for Weak Bisimulation via Generalized Parameterized Coinduction
- One Monad to Prove Them All
- Program Adverbs and Tlön Embeddings