diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,5 +1,11 @@ # Changelog +## 0.1.0.2 - 2026-07-22 + +- Documentation: the `Moonlight.Core` umbrella header now carries the worked + recipes — persistent union-find, bounded fixpoints, checked total maps, and + the matching seam. The README is reduced to a dependency and module map. + ## 0.1.0.1 - 2026-07-22 - Public named sublibraries drop the redundant package prefix: diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -3,118 +3,9 @@ > Part of **Moonlight**, the sheaf-theoretic computation layer beneath > [Melusine](https://bluerose.blue) 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 - -```haskell -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. - -```haskell -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`. - -```haskell -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. - -```haskell -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. - -```haskell -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)) -``` +`moonlight-core` is Moonlight's foundation tier. The front door is the total +umbrella module `Moonlight.Core`; its header carries the contract, the API map, +and the worked recipes. This page is the dependency map and the build commands. ## Surface & boundaries @@ -127,13 +18,12 @@ | `moonlight-core:moonlight-core-syntax` | `Moonlight.Core.Pattern.AntiUnify` | Patterns and term anti-unification without the full umbrella. | | `moonlight-core:moonlight-core-automata` | `Moonlight.Core.Pattern.Automata` or `.Kernel` | The bottom-up automata substrate and compiled matcher. Depend on syntax too when naming its types directly. | | `moonlight-core:moonlight-core-egraph-program` | `Moonlight.Core.EGraph.Program` | The host-neutral e-graph program algebra without the rest of the foundation. | -| `moonlight-core` | `Moonlight.Core.Unsound` | The explicit trust boundary; see [Main idea](#main-idea). | +| `moonlight-core` | `Moonlight.Core.Unsound` | The explicit trust boundary. | 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 diff --git a/moonlight-core.cabal b/moonlight-core.cabal --- a/moonlight-core.cabal +++ b/moonlight-core.cabal @@ -1,6 +1,6 @@ cabal-version: 3.0 name: moonlight-core -version: 0.1.0.1 +version: 0.1.0.2 synopsis: Mathematical basis for Pale Meridian. description: A total vocabulary of numeric classes, structural identity, orders, patterns, fixpoints, union-find, finite registries, and host-neutral e-graph programs. license: MIT diff --git a/src-public/Moonlight/Core.hs b/src-public/Moonlight/Core.hs --- a/src-public/Moonlight/Core.hs +++ b/src-public/Moonlight/Core.hs @@ -1,9 +1,100 @@ {-| -Authoritative frozen umbrella re-export of the moonlight-core foundation -surface. Direct @Moonlight.Core.*@ module imports outside this module are -internal-use-at-own-risk, except for the deliberately explicit -"Moonlight.Core.Unsound" trust boundary. Unsafe refinement constructors are not -re-exported here. +The single, total import of the @moonlight-core@ foundation — the vocabulary +every layer above shares. Every name reachable from @Moonlight.Core@ is +/total/: failure is a value in the return type, never an exception. @tryInv@ +returns @Maybe@, @makeSet@ returns @Either UnionFindAllocationError@, and +@fixpointBounded@ returns @Either (FixpointDivergence a)@; operations with no +failure case (@magnitude@, @neg@, @union@) return bare values. + +Direct @Moonlight.Core.*@ imports elsewhere are internal-use-at-own-risk, and +the unsafe refinement constructors are not re-exported here. The one deliberate +hole in construction-time checking is "Moonlight.Core.Unsound", whose +constructors assert a refinement the checker cannot see. + +The re-exported vocabulary, by role: + +* Numeric tower — @Scalar@, @Numeric@ (@OrderedRing@, @OrderedField@, + @ContinuousField@) and @ApproxEq@, with canonical and exact numbers via + @Canon@, @CanonicalNumber@, @ExactToken@. +* Validation and refinement — @Validation@, @Refinement@, @Niche@: the + construction-time checks that back the totality contract. +* Identity and language — @DomainId@, @Identifier@ (with the e-graph + identifiers and @PatternVar@), @Capability@, @ModuleIdentifier@, and the + @Language@ / @ZipMatch@ node algebra. +* Theories, patterns and matching — @Theory@, @Pattern@, @Substitution@, + @Match@: the one-layer structural-matching seam the e-graph and rewriting + layers stand on. +* Identity hashing — @StableHash@, @Hash@, @DenseKey@. +* Order, finiteness and fixpoints — @Finite@, @Order@, @OrdCollection@, + @Fix.Order@, and @Fixpoint@ (with the dense solver), which report + non-convergence as a value. +* Collections and registries — @Aggregate@, @MapAccum@, @MapInvert@, @Queue@, + @Dedup@, @Scan@, @Relational@, checked-total @TotalRegistry@, and the + persistent and transactional @UnionFind@. +* Programs and terms — the host-neutral @EGraph.Program@ and @Site.Program@ + algebras and the relational @Term.Database@ with its canonicalization. +* Manifests and metadata — @ProofManifest@, @LawName@, @Guidance@, @Boundary@, + @Cardinality@, @IsoNorm@, @TypeLevel@, @Error@. + +Each module's Haddock carries the signatures; the laws are named through +@LawName@ and machine-checked in the package law suites, not restated here. + +Worked recipes follow: the total path returns a value, the failure path a typed +sum. Each assumes @import Moonlight.Core@. + +/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. + +> 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@ rather than looping. + +> 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 (assumes @Data.List.NonEmpty (NonEmpty (..))@ +and a qualified @Data.Map.Strict@). + +> 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. + +> 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)) -} module Moonlight.Core ( -- * Numeric tower