moonlight-algebra

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

The law-governed algebraic tower the rest of the cathedral stands on.

moonlight-algebra is Moonlight's algebraic tier. Building on moonlight-core, it supplies a tower of pure, law-governed algebraic structures: standard semigroups/monoids with operation-selecting additive and multiplicative wrappers, group refinements, the lattice hierarchy up to Heyting and Boolean algebras, integral/GCD/Euclidean domain refinements, modules and vector spaces, modular arithmetic, number theory, free structures, and sparse vectors. Each structure is a thin type class or newtype boundary; its laws are stated in the module header and exercised by the private law-suite sublibrary.

Relationship to moonlight-core

moonlight-core owns the operation-bearing numeric tower: AdditiveMonoid, AdditiveGroup, MultiplicativeMonoid, Semiring, Ring, CommutativeRing, and Field. Moonlight.Algebra.Pure.Ring re-exports the law-only semiring and commutative-ring classes from core and adds only the stronger domain refinements: IntegralDomain, GCDDomain, EuclideanDomain, and CanonicalEuclideanDomain. There is one arithmetic vocabulary; the ring layer reuses core's zero, one, add, and mul.

What it provides

• Groups, free structures and actions. Standard Semigroup/Monoid, Group/AbelianGroup law refinements, Additive and Multiplicative wrappers for carriers with several lawful operations, free monoids and free abelian groups, the two-element sign/orientation group (ℤ/2), and monoid actions on a carrier with a group-acting refinement.
• The lattice hierarchy. Join/meet semilattices up to Heyting and Boolean algebras. Compiled finite lattices live in the public moonlight-algebra:finite-lattice sublibrary.
• Rings and arithmetic. Semiring → commutative ring → integral/GCD/Euclidean domains; modular arithmetic (Zn); quotient rings R/(n) of a Euclidean domain; number theory and gcd; and univariate polynomials over a coefficient ring (Horner evaluation, a free module on monomial degrees).
• Modules and magnitudes. Modules, free modules, vector spaces, bilinear spaces over a field, and real-valued magnitudes for obstructions.
• Constructions. Power-set lattices, finite n-fold product algebras with coordinatewise structure, quotients, and sparse vectors with finite support.

Tiny usage examples

import Moonlight.Algebra.Pure.Group

difference :: Additive Integer
difference = groupDifference (Additive 3) (Additive 5)

product :: Multiplicative Integer
product = Multiplicative 3 <> Multiplicative 5

Sparse kernels:

compiled = compileSparseLinearMap 128 (\i -> [(i, 1), (i + 1, 2)])

combined = add (fromEntries [('x', 2)]) (fromEntries [('x', 3), ('y', 1)])

Finite lattices

This public sublibrary owns checked finite-order compilation and the dense runtime views inside moonlight-algebra: ContextLattice, dense join/meet/<= plans, resident branded keys, Heyting implication, least/greatest fixpoints, cover edges, presentation builders, and generator support kernels.

The main moonlight-algebra library remains the abstract algebra class tower. The finite-lattice sublibrary is the finite, validated, queryable realization of a lattice over a declared closed universe.

Quick start

Declare a finite order by name binding. latticeOf infers the unique top and bottom, transitively closes the order, derives join and meet, and proves lattice-hood, returning a compiled ContextLattice or the first obstruction it finds.

import Moonlight.FiniteLattice

data Context = Bottom | West | East | Top
  deriving (Eq, Ord, Show)

diamond :: Either (LatticeBuildError Context) (ContextLattice Context)
diamond =
  latticeOf $ do
    [bottom, west, east, top] <- elements [Bottom, West, East, Top]
    below bottom west
    below bottom east
    below west top
    below east top

West and East are incomparable; their least upper bound and greatest lower bound are derived from the order alone. On the compiled lattice, order, join and meet are total, checked lookups into the dense plan:

>>> Right lattice = diamond
>>> joinContext lattice West East
Right Top
>>> meetContext lattice West East
Right Bottom
>>> leqContext lattice Bottom Top
Right True

Heyting implication

The diamond is distributive, so it carries a Heyting structure. compileContextHeyting builds the residual plan once; impliesContext is then the relative pseudocomplement: the largest x with antecedent ∧ x ≤ consequent.

>>> Right heyting = compileContextHeyting lattice
>>> impliesContext heyting West East
Right East
>>> impliesContext heyting West West
Right Top

Least and greatest fixpoints

Every monotone endomap on the lattice has a least and a greatest fixpoint (Knaster–Tarski). leastContextFixpoint climbs up from the bottom, greatestContextFixpoint descends from the top; a non-monotone step is rejected as a typed ContextMonotoneMapError.

settle :: Context -> Context
settle Bottom = West
settle West   = West
settle East   = Top
settle Top    = Top

>>> leastContextFixpoint lattice settle
Right West
>>> greatestContextFixpoint lattice settle
Right Top

The resident fast path

joinContext, meetContext, and impliesContext resolve each domain value through a map on every call. When you sweep many queries, resolve once: withResidentContext hands you branded keys whose order, join, and meet are pure array indexing without per-query lookup inside the loop.

leqRelationSize :: ContextLattice Context -> Int
leqRelationSize lattice =
  withResidentContext lattice $ \ctx ->
    let keys = residentContextKeys ctx
     in length [() | a <- keys, b <- keys, residentContextKeyLeq ctx a b]

>>> leqRelationSize lattice
9

The count is the size of the ≤ relation: four reflexive pairs, plus Bottom under West, East, and Top, plus West and East each under Top.

Public modules

All Moonlight.Algebra.Pure.* leaves are exposed by the public abstract sublibrary and gathered by the Moonlight.Algebra surface. The unsafe GCD witness (Moonlight.Algebra.Unsafe.GCDWitness) lives in the private moonlight-algebra-internal sublibrary, the compiled finite lattice realization lives in the public finite-lattice sublibrary, and the law suite (Moonlight.Algebra.Effect.Laws, Moonlight.Algebra.Test.Generators) lives in the private moonlight-algebra-laws sublibrary.

Performance

Compilation and the resident-key and <= query paths are fast; join/meet throughput and the compiled ContextLattice query surface are under active performance work.

License

MIT; see LICENSE.