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.
System requirements:
Compilation instructions:
- Run
makein the top-level directory - Run
make cleanto remove all build artifacts (including compiled files) and start over - By default
makegenerates Coqdocs underhtml - Run
make alectryon(if Alectryon is installed) to generate documents underhtml-alectryon/
Coqdocs are found under /docs/html/toc.html
Alectryon files are found under /docs/html-alectryon/
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
bindoperation 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:
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 |
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
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 that convert between locally nameless and de Bruijn representations of variable binding are found under Tealeaves/Backends/Adapters.
Examples of using Tealeaves to formalize various calculi are found in Tealeaves/Examples
A multisorted definition of DTMs is contained in Tealeaves/Classes/Multisorted. A multisorted locally nameless backend is contained in Tealeaves/Backends/Multisorted/LN.v.
| 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.