Program Adverbs and Tl\"on Embeddings

TL;DR

This paper introduces program adverbs and Tl"on embeddings, new structures for representing effectful program semantics that offer greater flexibility and preserve more syntactic information than traditional free monad-based embeddings.

Contribution

It defines program adverbs inspired by applicative and selective functors, and develops Tl"on embeddings that improve semantic modeling of effectful computations.

Findings

Tl"on embeddings retain more syntactic structure than free monad embeddings.

Program adverbs can compose multiple computational patterns.

The approach enhances flexibility in effect modeling.

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.