moonlight-category

Part of Moonlight, the sheaf-theoretic computation layer beneath Melusine and Pale Meridian.

moonlight-category is Moonlight's categorical tier. Building on moonlight-core, it provides a totalised, explicit-error category abstraction together with the finite, runtime-validated categories and site/path presentations the compiler uses to model its own structure.

Relationship to data-category

If you want general indexed category theory in Haskell, prefer Sjoerd Visscher's data-category. Its typed-arrow calculus is the primary inspiration for this package's indexed layer, and several modules under Moonlight.Category.Indexed are adapted from it. Thank you to Sjoerd Visscher for the design and implementation work in data-category.

Full attribution and the upstream BSD-3-Clause license are recorded in THIRD_PARTY_NOTICES.md.

What it provides

• A category abstraction. The Category class is totalised: objects, morphisms, 2-morphisms, compositors and a category-specific error type are associated types, and every operation returns Either.
• Limits and colimits. A class tower for products, coproducts, pullbacks, pushouts, equalizers and coequalizers.
• Higher structure. 2-categories, bicategories, monoidal and enriched categories.
• Finite categories. FinCat: runtime-validated finite categories with handles, bit-packed thin variants, composable chains and core/automorphism groupoid extraction.
• Finite-category presentations. Moonlight.Category.Presentation provides a focused authoring EDSL for finite posets and fully enumerated finite categories, compiling down to validated FinCat.
• Sites and presentations. Site manifests with validation, reachable-closure and import-cycle diagnostics, path categories, quotients, and compilation down to FinCat.
• Rewriting witnesses. Adhesive and PBPO pushout-complement witnesses, structured cospans, double categories, and decorated composition/presentation.
• Indexed category theory. The typed-arrow layer adapted from data-category.
• Simplicial substrate. Runtime-dimensional Δ morphisms, finite truncated simplicial sets, standard/boundary/horn spaces, nerves, Kan interfaces, and connected-component/core-groupoid queries over finite composable categories.

Public modules

The Moonlight.Category.Pure.* leaves live in named implementation sublibraries: abstract for generic category theory, finite for FinCat/presentation runtime, site for site and path compilation, indexed for the adapted data-category typed-arrow layer, and simplicial for Δ, simplicial sets, nerves and Kan interfaces. Effectful law harnesses and cross-package test fixtures live in the laws sublibrary rather than the pure production components.

Dependency footprint

Hackage's package-level dependency summary aggregates dependencies from every component in the distribution. Depending on the main moonlight-category library does not select moonlight-category:laws and therefore does not add Tasty, Hedgehog, or moonlight-pale:test-laws. Consumers opt into that reusable law harness explicitly with a dependency on moonlight-category:laws.

Finite-category presentations

Use Moonlight.Category.Presentation to write finite categories declaratively. Compilation always produces the validated runtime representation FinCat.

Finite posets

below declares strict generating inequalities. Compilation takes the transitive closure, rejects cycles, and supplies identities implicitly.

import Moonlight.Category.Presentation

threeChain :: Either FinCatBuildError FinCat
threeChain =
  finCategory $ do
    [a, b, c] <- objects ["A", "B", "C"]
    below a b
    below b c

Fully enumerated finite categories

In the general dialect, each call to arrow declares one actual nonidentity morphism of the resulting category. Equations determine the nonidentity composition table.

import Moonlight.Category.Presentation

commutingTriangle :: Either FinCatBuildError FinCat
commutingTriangle =
  finCategory $ do
    a <- object "A"
    b <- object "B"
    c <- object "C"

    f <- arrow a b "f"
    g <- arrow b c "g"
    h <- arrow a c "h"

    equate (g `after` f) h

Identities may be named inside equations:

inversePair :: Either FinCatBuildError FinCat
inversePair =
  finCategory $ do
    a <- object "A"
    b <- object "B"

    f <- arrow a b "f"
    g <- arrow b a "g"

    equate (g `after` f) (identityAt a)
    equate (f `after` g) (identityAt b)

Longer paths are accepted when their proper intermediate composites are determined elsewhere in the presentation. Equation declaration order is irrelevant.

The presentation dialect accepts declared morphisms and equations over determined composites. An equation such as equate f g for distinct declared morphisms is rejected rather than silently identifying them.

For querying and composing morphisms after compilation, import Moonlight.Category.Notation separately.

Acknowledgements

The representation of finite and finitely-presented categories as concrete, runtime-validated data structures, including FinCat and the site/path presentations that compile down to it, was directly inspired by the AlgebraicJulia ecosystem and the work on attributed C-sets (acsets), whose thesis is precisely that categorical objects can be realised as performant data structures. The implementation here is independent; the conceptual debt is real and gratefully acknowledged.

Evan Patterson, Owen Lynch, and James Fairbanks. "Categorical Data Structures for Technical Computing." arXiv:2106.04703. https://arxiv.org/abs/2106.04703

Thank you to Evan Patterson, Owen Lynch, James Fairbanks, and the AlgebraicJulia community.

License

Moonlight's original code is licensed under MIT; see LICENSE. The indexed modules adapted from data-category remain BSD-3-Clause; their copyright notice, license terms, and attribution are recorded in THIRD_PARTY_NOTICES.md.