  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.
