moonlight-core

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

moonlight-core is Moonlight's foundation tier. It is the total vocabulary every layer above shares: numeric classes, structural identity, orders, patterns, fixpoints, persistent union-find, finite registries, a term database, and a host-neutral e-graph program algebra.

Main idea

Every name reachable from the one import, Moonlight.Core, is total. Failure is a value in the return type: tryInv returns Maybe, makeSet returns Either UnionFindAllocationError, fixpointBounded returns Either (FixpointDivergence a), mkTotalRegistry returns Either [missingKey]. Operations with no failure case (magnitude, neg, union) return bare values.

Moonlight.Core.Unsound holds the unchecked constructors: importing it by name asserts a refinement the checker cannot see. Every other constructor reachable through the umbrella validates at construction.

Use

import Moonlight.Core

reciprocalOfThree :: Maybe Double
reciprocalOfThree = tryInv 3

size :: Double
size = magnitude (neg (2.5 :: Double))

Cookbook

Each recipe shows the main idea in practice: the total path returns a value, the failure path returns a typed sum.

Persistent union-find

makeSet mints fresh classes through a checked allocation boundary, union merges them, and the structure is persistent; older versions stay valid after a merge.

import Moonlight.Core

partition :: Either UnionFindAllocationError (Bool, Bool)
partition = do
  (a, uf1) <- makeSet emptyUnionFind
  (b, uf2) <- makeSet uf1
  (c, uf3) <- makeSet uf2
  let uf = union a b uf3
  pure (equivalent a b uf, equivalent a c uf)   -- Right (True, False)

Bounded fixpoints

fixpointBounded iterates a step to a fixed point under an explicit fuel bound. Non-convergence returns a typed Left.

import Moonlight.Core

converge :: Either (FixpointDivergence Int) Int
converge = fixpointBounded 100 (\n -> n `div` 2) 37   -- Right 0

diverges :: Either (FixpointDivergence Int) Int
diverges = fixpointBounded 5 (+1) 0                   -- Left (out of fuel)

Checked total maps

mkTotalRegistry demands every key of a finite universe; a gap is a typed Left [missingKeys]. In exchange, lookupTotal returns a bare value once the registry is constructed.

import Moonlight.Core
import Data.List.NonEmpty (NonEmpty (..))
import qualified Data.Map.Strict as Map

data Slot = Alpha | Beta | Gamma
  deriving (Eq, Ord, Show)

instance FiniteUniverse Slot where
  finiteUniverse = Alpha :| [Beta, Gamma]

palette :: Either [Slot] (TotalRegistry Slot String)
palette = mkTotalRegistry (Map.fromList [(Alpha, "a"), (Beta, "b"), (Gamma, "c")])

labelOfBeta :: Either [Slot] String
labelOfBeta = fmap (\reg -> lookupTotal reg Beta) palette   -- Right "b"
-- mkTotalRegistry (Map.fromList [(Alpha, "a")])  ==  Left [Beta, Gamma]

The matching seam

ZipMatch is one-layer structural matching: zipMatch succeeds iff two nodes share a shape, pairing their children positionally. It is the seam the e-graph and rewriting layers are built on.

import Moonlight.Core

data ExprF a = Lit Int | Add a a
  deriving (Functor, Foldable, Traversable, Eq, Ord, Show)

instance ZipMatch ExprF where
  zipMatch (Lit m)     (Lit n)     | m == n = Just (Lit m)
  zipMatch (Add a1 b1) (Add a2 b2)          = Just (Add (a1, a2) (b1, b2))
  zipMatch _           _                    = Nothing

aligned :: Maybe (ExprF (Int, Int))
aligned = zipMatch (Add 1 2) (Add 10 20)   -- Just (Add (1,10) (2,20))

Surface & boundaries

Most downstream code imports the umbrella. Lower-level packages may depend on one of the public sublibraries.

The private implementation slices remain basis, numeric, solver, and term. Syntax, automata, and e-graph programs are public because other foundation packages consume those exact owners. The umbrella re-exports the syntax and e-graph-program vocabulary; automata are imported only through the sublibrary. Haddock carries the signatures; the laws are named and machine-checked in the law suites.

Test

cabal test moonlight-core:moonlight-core-test

Benchmarks

cabal bench moonlight-core:moonlight-core-bench --benchmark-options='--timeout=2s --csv=comparison.csv'

hackage: rows measure a package-level baseline (containers, memory, scientific, equivalence) on the same fixture; world: rows are source-equivalent baselines where no package owner exists. Fixtures assert result agreement with the baseline before timing. Dated receipts live in docs/BENCHMARKS-m4-pro.md.

License

MIT. See LICENSE.