Tealeaves

Tealeaves is a Coq framework for proving theorems about syntax abstractly, i.e. independently of a concrete grammar. This independence makes syntactical theory reusable between developments, and is achieved by separating a choice of grammar from a choice of variable representation. Our central abstraction is a "structured" kind of monad that we call decorated traversable, which is an abstraction of abstract syntax trees. Tealeaves "core" is a Coq implementation of the equational theory of such monads, as well as higher-level principles built on top of this theory.

How to build Tealeaves

System requirements:

• make (see GNU Make)
• Autosubst
• An installation of Coq. This branch has been tested with Coq 8.16.

Compilation instructions:

• Run make in the top-level directory
• Run make clean to remove all build artifacts (including compiled files) and start over
• By default make generates Coqdocs under html
• Run make alectryon (if Alectryon is installed) to generate documents under html-alectryon/

Documentation

Coqdocs are found under /docs/html/toc.html

Alectryon files are found under /docs/html-alectryon/

Organization

Navigating the Typeclass Hierarchy

The theory of decorated traversable monads (DTMs) is formlized in three equivalent ways:

• Classically: "a DTM is a monoid in the category of decorated-traversable endofunctors"
• In the style of Kleisli: "a DTM is a type constructor with a generalized bind operation subject to equations"
• In terms of parameterized coalgebras: "a DTM is a container of elements, paired with a context, which can be replaced with subtrees"

These different views are respetively formalized under these directories:

• Tealeaves/Classes/Categorical
• Tealeaves/Classes/Kleisli
• Tealeaves/Classes/Coalgebraic

Here is a convenient table for navigating the typeclass hierarchy:

| Tealeaves Typeclasses | Functor | Monad | |---------------------------|---------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------|---------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------| | Plain | Classes/Functor.v | Categorical / Kleisli | | Decorated | Categorical / Kleisli | Categorical / Kleisli | | Traversable | Categorical / Kleisli / Coalgebraic | Categorical / Kleisli / Coalgebraic | | Decorated+Traversable | Categorical / Kleisli / Coalgebraic | Categorical / Kleisli / Coalgebraic |

Equivalence of the Presentations

For each concept (e.g. decorated functor, traversable monad, etc.) adapters are provided which, given a typeclass instance for one view, derive a typeclass instance for another view. For example, the typeclass instance that converts a Kleisli-presented decorated-traversable functor into a coalgebraic one is found in Tealeaves/Adapters/KleisliToCoalgebraic/DecoratedTraversableFunctor.v. Adapters that convert directly between categorical and coalgebraic instances are not given, but can be obtained by composition via converting to/from the Kleisli instances.

| Adapter | Directory | |---------------------------|------------------------------------------------------------------------------------| | Categorical ⇝ Kleisli | Tealeaves/Adapters/CategoricalToKleisli | | Categorical ⇝ Coalgebraic | Not formalized directly | | Kleisli ⇝ Categorical | Tealeaves/Adapters/KleisliToCategorical | | Kleisli ⇝ Coalgebraic | Tealeaves/Adapters/KleisliToCoalgebraic | | Coalgebraic ⇝ Kleisli | Tealeaves/Adapters/CoalgebraicToKleisli | | Coalgebraic ⇝ Categorical | Not formalized directly |

The correctness of the adapters states that (up to functional extensionality), performing a two-way roundtrip with any of the adapters results in the original structure. These proofs are found in Tealeaves/Adapters/Roundtrips

Backends

Tealeaves backends are formalized under Tealeaves/Backends. Tealeaves users should import backends directly from the top-level files in this directory. For instance, to import the single-sorted locally nameless backend, import Tealeaves/Backends/LN.v.

Adapters

Adapters that convert between locally nameless and de Bruijn representations of variable binding are found under Tealeaves/Backends/Adapters.

Examples

Examples of using Tealeaves to formalize various calculi are found in Tealeaves/Examples

Multisorted Tealeaves

A multisorted definition of DTMs is contained in Tealeaves/Classes/Multisorted. A multisorted locally nameless backend is contained in Tealeaves/Backends/Multisorted/LN.v.

Other Directories

| Directory | Contents | |-------------------------------------------------------------------|---------------------------------------------------------------------------------------| | Tealeaves/Categories | Instances of the Category typeclass | | Tealeaves/Functors | Common endofunctors (Type -> Type) and instances of DTM concepts (Kleisli style) | | Tealeaves/Functors/Categorical | A few endofunctors (Type -> Type) and instances of DTM concepts (Categorical style) | | Tealeaves/Tactics | Tactics for internal use | | Tealeaves/Simplification | Simplication tactics for backends for downstream use |

Additionally, subdirectories named Theory/ are scattered in various places. Mostly these contain definitions and lemmas regarding various DTM concepts which, for whatever reason (e.g. to avoid cyclic dependencies), are formalized in files separately from those defining the relevant concepts.