References & Citations
Computer Science > Programming Languages
Title: Program Adverbs and Tlön Embeddings
(Submitted on 11 Jul 2022 (v1), last revised 26 Jul 2022 (this version, v2))
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\"on embeddings. Compared with embeddings based on free monads, Tl\"on embeddings allow more flexibility in computational modeling of effects, while retaining more information about the program's syntactic structure.
Submission history
From: Yao Li [view email][v1] Mon, 11 Jul 2022 23:47:47 GMT (172kb,D)
[v2] Tue, 26 Jul 2022 20:25:34 GMT (175kb,D)
Link back to: arXiv, form interface, contact.