Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Directories: A Convenient and Well-Behaved Formalism for Hierarchical Organization in Categorical Systems Theory

Owen Lynch, Markus Lohmayer

TL;DR

This paper addresses the problem of providing a strict, human-readable hierarchical organization for categorical structures. It introduces directories as a polynomial-monad-inspired framework and lifts them to a $2$-monad on $\mathsf{Cat}$, yielding $2$-algebras equivalent to cocartesian, cartesian, or symmetric monoidal categories, while remaining strictly indexed by path-like names. The main contributions are the construction of the $Dtry$ monad, the non-empty subdirectory invariant via $\text{Record}_{\neq \emptyset}$, and the path-indexed analogue of the Fam construction supported by a concrete Haskell implementation. Together, these developments offer a strict, named alternative to coherence-heavy monoidal formalisms and enable practical programming paradigms for hierarchical systems such as EPHS.

Abstract

This paper introduces an inherently strict presentation of categories with products, coproducts, or symmetric monoidal products that is inspired by file systems and directories. Rather than using nested binary tuples to combine objects or morphisms, the presentation uses named tuples. Specifically, we develop 2-monads whose strict 2-algebras are product categories, coproduct categories, or symmetric monoidal categories, in a similar vein to the classical Fam construction, but where the elements of the indexing set are period-separated identifiers like $\mathtt{cart.motor.momentum}$. Our development of directories is also intended to serve the secondary purpose of expositing certain aspects of polynomial monads, and is accompanied by Haskell code that shows how the mathematical ideas can be implemented.

Directories: A Convenient and Well-Behaved Formalism for Hierarchical Organization in Categorical Systems Theory

TL;DR

This paper addresses the problem of providing a strict, human-readable hierarchical organization for categorical structures. It introduces directories as a polynomial-monad-inspired framework and lifts them to a -monad on , yielding -algebras equivalent to cocartesian, cartesian, or symmetric monoidal categories, while remaining strictly indexed by path-like names. The main contributions are the construction of the monad, the non-empty subdirectory invariant via , and the path-indexed analogue of the Fam construction supported by a concrete Haskell implementation. Together, these developments offer a strict, named alternative to coherence-heavy monoidal formalisms and enable practical programming paradigms for hierarchical systems such as EPHS.

Abstract

This paper introduces an inherently strict presentation of categories with products, coproducts, or symmetric monoidal products that is inspired by file systems and directories. Rather than using nested binary tuples to combine objects or morphisms, the presentation uses named tuples. Specifically, we develop 2-monads whose strict 2-algebras are product categories, coproduct categories, or symmetric monoidal categories, in a similar vein to the classical Fam construction, but where the elements of the indexing set are period-separated identifiers like . Our development of directories is also intended to serve the secondary purpose of expositing certain aspects of polynomial monads, and is accompanied by Haskell code that shows how the mathematical ideas can be implemented.
Paper Structure (17 sections, 24 theorems, 30 equations)

This paper contains 17 sections, 24 theorems, 30 equations.

Table of Contents

  1. Introduction
  2. Motivation
  3. Outline
  4. Directories
  5. Directories are maps from paths to values
  6. Directories as tries
  7. Disallowing non-empty subdirectories
  8. Using $\mathit{Dtry}$
  9. Morphisms of directories
  10. A note on implementation
  11. The $\mathsf{Fam}$ construction
  12. Indexing by paths in a directory
  13. 2-algebras of $\mathsf{Dtry}$
  14. Conclusion
  15. Free Monads and Distributive Laws
  16. ...and 2 more sections

Key Result

Lemma 2.3

If for a functor $p \colon \mathsf{Set} \to \mathsf{Set}$ such an indexed family $\{F_i\}_{i \colon p(1)}$ exists, then that indexed family is unique up to isomorphism. That is, if such that is the identity on $\sum_{i \colon p(1)} 1$, then $F_i \cong F_i'$ for all $i \colon p(1)$.

Theorems & Definitions (73)

  • Definition 2.1
  • Definition 2.2
  • Lemma 2.3
  • Example 2.4
  • Example 2.5
  • Example 2.6
  • Definition 2.7
  • Example 2.8
  • Proposition 2.9
  • proof
  • ...and 63 more