moonlight-algebra 0.1.0.1 → 0.1.0.2
raw patch · 15 files changed
+559/−112 lines, 15 files
Files
- CHANGELOG.md +8/−0
- LICENSE +1/−1
- bench/abstract/Main.hs +2/−4
- bench/aggregate/Main.hs +2/−4
- bench/finite-lattice/Main.hs +2/−4
- moonlight-algebra.cabal +14/−10
- src-abstract/Moonlight/Algebra/Pure/Quantale.hs +218/−0
- src-laws/Moonlight/Algebra/Effect/Laws.hs +66/−69
- src-public/Moonlight/Algebra.hs +6/−3
- test/abstract/AbstractTests.hs +2/−0
- test/abstract/Main.hs +2/−2
- test/abstract/QuantaleSpec.hs +224/−0
- test/aggregate/Main.hs +0/−13
- test/coherence/Main.hs +10/−0
- test/finite-lattice/Main.hs +2/−2
CHANGELOG.md view
@@ -1,5 +1,13 @@ # Changelog +## 0.1.0.2 - 2026-08-21++- Add the public quantale tower: `Quantale`, commutative, residuated, integral,+ and chain refinements; Viterbi, Łukasiewicz, and tropical carriers; and+ law coverage for the complete algebra.+- Align focused and aggregate coherence tests with their actual dependency and+ optimization boundaries.+ ## 0.1.0.1 - 2026-07-22 - Documentation: the public `finite-lattice` sublibrary front door
LICENSE view
@@ -1,6 +1,6 @@ MIT License -Copyright (c) 2026 The Blue Rose, Rosalia Fialkova+Copyright (c) 2026 Blue Rose Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files (the "Software"), to deal
bench/abstract/Main.hs view
@@ -6,10 +6,8 @@ import AbstractBench ( abstractBenchmarks, )-import Moonlight.Pale.Bench.Runner- ( runBenchmark,- )+import Test.Tasty.Bench (defaultMain) main :: IO () main =- runBenchmark abstractBenchmarks+ defaultMain [abstractBenchmarks]
bench/aggregate/Main.hs view
@@ -9,13 +9,11 @@ import FiniteLatticeBench ( finiteLatticeBenchmarkSuite, )-import Moonlight.Pale.Bench.Runner- ( runBenchmarks,- )+import Test.Tasty.Bench (defaultMain) main :: IO () main =- runBenchmarks+ defaultMain [ abstractBenchmarks, finiteLatticeBenchmarkSuite ]
bench/finite-lattice/Main.hs view
@@ -6,10 +6,8 @@ import FiniteLatticeBench ( finiteLatticeBenchmarkSuite, )-import Moonlight.Pale.Bench.Runner- ( runBenchmark,- )+import Test.Tasty.Bench (defaultMain) main :: IO () main =- runBenchmark finiteLatticeBenchmarkSuite+ defaultMain [finiteLatticeBenchmarkSuite]
moonlight-algebra.cabal view
@@ -1,6 +1,6 @@ cabal-version: 3.4 name: moonlight-algebra-version: 0.1.0.1+version: 0.1.0.2 homepage: https://github.com/PaleRoses/moonlight bug-reports: https://github.com/PaleRoses/moonlight/issues synopsis: Algebraic type class tower for Pale Meridian.@@ -57,6 +57,7 @@ Moonlight.Algebra.Pure.Polynomial Moonlight.Algebra.Pure.PowerSet Moonlight.Algebra.Pure.Product+ Moonlight.Algebra.Pure.Quantale Moonlight.Algebra.Pure.Quotient Moonlight.Algebra.Pure.Ring Moonlight.Algebra.Pure.SparseVec@@ -128,6 +129,9 @@ import: shared-properties visibility: private hs-source-dirs: src-laws+ -- Law construction supports tests; it is absent from every benchmark link+ -- graph and does not need production simplification.+ ghc-options: -O0 exposed-modules: Moonlight.Algebra.Effect.LawNames Moonlight.Algebra.Effect.Laws@@ -153,8 +157,9 @@ other-modules: AbstractTests OrderedLatticeSpec+ QuantaleSpec SparseVecSpec- ghc-options: -Wall -Wcompat+ ghc-options: -Wall -Wcompat -O0 default-extensions: TypeFamilies UndecidableInstances@@ -165,7 +170,6 @@ , moonlight-algebra:abstract , moonlight-algebra:moonlight-algebra-laws , moonlight-core >= 0.1 && < 0.2- , moonlight-pale:test >= 0.1 && < 0.2 , tasty >= 1.4 && < 1.6 , tasty-hunit >= 0.10 && < 0.11 , tasty-hedgehog >= 1.4 && < 1.5@@ -176,6 +180,7 @@ type: exitcode-stdio-1.0 hs-source-dirs: test/finite-lattice main-is: Main.hs+ ghc-options: -O0 other-modules: FiniteLatticeSpec FiniteLatticeTests@@ -187,20 +192,22 @@ base >= 4.22 && < 5 , containers >= 0.6 && < 0.9 , moonlight-algebra:finite-lattice- , moonlight-pale:test >= 0.1 && < 0.2 , tasty >= 1.4 && < 1.6 , tasty-hunit >= 0.10 && < 0.11 , tasty-quickcheck >= 0.10 && < 0.12 , QuickCheck >= 2.14 && < 2.19 -test-suite moonlight-algebra-test+-- The focused suites own behavior. This component owns only the union of their+-- module, instance, and dependency surfaces, compiled at O0.+test-suite moonlight-algebra-coherence-test import: shared-properties type: exitcode-stdio-1.0 hs-source-dirs:- test/aggregate+ test/coherence test/abstract test/finite-lattice main-is: Main.hs+ ghc-options: -O0 other-modules: AbstractTests FiniteLatticeSpec@@ -208,6 +215,7 @@ LawSpec OrderedLatticeSpec PresentationSpec+ QuantaleSpec SparseVecSpec default-extensions: FunctionalDependencies@@ -220,7 +228,6 @@ , moonlight-algebra:finite-lattice , moonlight-algebra:moonlight-algebra-laws , moonlight-core >= 0.1 && < 0.2- , moonlight-pale:test >= 0.1 && < 0.2 , tasty >= 1.4 && < 1.6 , tasty-hedgehog >= 1.4 && < 1.5 , tasty-hunit >= 0.10 && < 0.11@@ -242,7 +249,6 @@ , moonlight-algebra , moonlight-algebra:abstract , moonlight-core >= 0.1 && < 0.2- , moonlight-pale:bench >= 0.1 && < 0.2 , tasty-bench >= 0.3 && < 0.6 , vector >= 0.13 && < 0.14 @@ -270,7 +276,6 @@ , deepseq >= 1.4 && < 1.6 , lattices >= 2.2 && < 2.3 , moonlight-algebra:finite-lattice- , moonlight-pale:bench >= 0.1 && < 0.2 , tasty-bench >= 0.3 && < 0.6 , vector >= 0.13 && < 0.14 @@ -305,6 +310,5 @@ , moonlight-algebra:abstract , moonlight-algebra:finite-lattice , moonlight-core >= 0.1 && < 0.2- , moonlight-pale:bench >= 0.1 && < 0.2 , tasty-bench >= 0.3 && < 0.6 , vector >= 0.13 && < 0.14
+ src-abstract/Moonlight/Algebra/Pure/Quantale.hs view
@@ -0,0 +1,218 @@+-- | Quantales: monoids in the join-semilattice — 'tensor' distributes over+-- 'join' and annihilates 'bottom' — with commutative and residuated+-- refinements, and the Viterbi, Łukasiewicz and tropical carriers.+--+-- Laws: tensor is associative with unit 'tensorUnit'; tensor distributes over+-- join on both sides and @tensor a bottom = bottom = tensor bottom a@;+-- commutative quantales add @tensor a b = tensor b a@; residuated quantales+-- satisfy the Galois law @joinLeq (tensor x y) z = joinLeq x (residual y z)@.+-- 'IntegralQuantale' marks carriers whose unit is top; 'ChainQuantale' marks+-- carriers whose join is selective.+module Moonlight.Algebra.Pure.Quantale+ ( Quantale (..),+ CommutativeQuantale,+ ResiduatedQuantale (..),+ IntegralQuantale,+ ChainQuantale,+ ChainOrder (..),+ Viterbi (..),+ Lukasiewicz (..),+ Tropical (..),+ tensors,+ )+where++import Data.Kind (Constraint, Type)+import Moonlight.Algebra.Pure.Lattice+ ( BoundedJoinSemilattice (..),+ HeytingAlgebra (implies),+ JoinSemilattice (..),+ joinLeq,+ )++type Quantale :: Type -> Constraint+class BoundedJoinSemilattice a => Quantale a where+ tensor :: a -> a -> a+ tensorUnit :: a++instance Quantale () where+ tensor _ _ = ()+ tensorUnit = ()++instance Quantale Bool where+ tensor = (&&)+ tensorUnit = True++instance (Quantale left, Quantale right) => Quantale (left, right) where+ tensor (leftA, rightA) (leftB, rightB) =+ (tensor leftA leftB, tensor rightA rightB)+ tensorUnit =+ (tensorUnit, tensorUnit)++instance Quantale value => Quantale (key -> value) where+ tensor left right key =+ tensor (left key) (right key)+ tensorUnit =+ const tensorUnit++type CommutativeQuantale :: Type -> Constraint+class Quantale a => CommutativeQuantale a++instance CommutativeQuantale ()++instance CommutativeQuantale Bool++instance+ (CommutativeQuantale left, CommutativeQuantale right) =>+ CommutativeQuantale (left, right)++instance CommutativeQuantale value => CommutativeQuantale (key -> value)++type ResiduatedQuantale :: Type -> Constraint+class CommutativeQuantale a => ResiduatedQuantale a where+ residual :: a -> a -> a++instance ResiduatedQuantale () where+ residual _ _ = ()++instance ResiduatedQuantale Bool where+ residual = implies++instance+ (ResiduatedQuantale left, ResiduatedQuantale right) =>+ ResiduatedQuantale (left, right)+ where+ residual (leftA, rightA) (leftB, rightB) =+ (residual leftA leftB, residual rightA rightB)++instance ResiduatedQuantale value => ResiduatedQuantale (key -> value) where+ residual left right key =+ residual (left key) (right key)++-- | Marker law: 'tensorUnit' is the top element, so 'tensor' is two-sided+-- deflationary and valuation fixpoints converge within the simple-path bound.+type IntegralQuantale :: Type -> Constraint+class Quantale a => IntegralQuantale a++instance IntegralQuantale ()++instance IntegralQuantale Bool++instance+ (IntegralQuantale left, IntegralQuantale right) =>+ IntegralQuantale (left, right)++instance IntegralQuantale value => IntegralQuantale (key -> value)++-- | Marker law: 'join' is selective (returns one of its arguments), so a+-- single witness attains any finite join.+type ChainQuantale :: Type -> Constraint+class Quantale a => ChainQuantale a++instance ChainQuantale ()++instance ChainQuantale Bool++-- | The total order a selective 'join' induces on a chain quantale; the 'Ord'+-- instance is lawful exactly when the 'ChainQuantale' law holds.+type ChainOrder :: Type -> Type+newtype ChainOrder a = ChainOrder {getChainOrder :: a}+ deriving stock (Eq, Show)++instance (ChainQuantale a, Eq a) => Ord (ChainOrder a) where+ compare (ChainOrder left) (ChainOrder right)+ | left == right = EQ+ | joinLeq left right = LT+ | otherwise = GT++-- | Carrier discipline: values lie in the unit interval; the operations+-- preserve it.+type Viterbi :: Type -> Type+newtype Viterbi a = Viterbi {getViterbi :: a}+ deriving stock (Eq, Ord, Show)++instance Ord a => JoinSemilattice (Viterbi a) where+ join = max++instance (Ord a, Num a) => BoundedJoinSemilattice (Viterbi a) where+ bottom = Viterbi 0++instance (Ord a, Num a) => Quantale (Viterbi a) where+ tensor (Viterbi left) (Viterbi right) =+ Viterbi (left * right)+ tensorUnit = Viterbi 1++instance (Ord a, Num a) => CommutativeQuantale (Viterbi a)++instance (Ord a, Fractional a) => ResiduatedQuantale (Viterbi a) where+ residual (Viterbi left) (Viterbi right)+ | left <= right = Viterbi 1+ | otherwise = Viterbi (right / left)++instance (Ord a, Num a) => IntegralQuantale (Viterbi a)++instance (Ord a, Num a) => ChainQuantale (Viterbi a)++-- | Carrier discipline: values lie in the unit interval; the operations+-- preserve it.+type Lukasiewicz :: Type -> Type+newtype Lukasiewicz a = Lukasiewicz {getLukasiewicz :: a}+ deriving stock (Eq, Ord, Show)++instance Ord a => JoinSemilattice (Lukasiewicz a) where+ join = max++instance (Ord a, Num a) => BoundedJoinSemilattice (Lukasiewicz a) where+ bottom = Lukasiewicz 0++instance (Ord a, Num a) => Quantale (Lukasiewicz a) where+ tensor (Lukasiewicz left) (Lukasiewicz right) =+ Lukasiewicz (max 0 (left + right - 1))+ tensorUnit = Lukasiewicz 1++instance (Ord a, Num a) => CommutativeQuantale (Lukasiewicz a)++instance (Ord a, Num a) => ResiduatedQuantale (Lukasiewicz a) where+ residual (Lukasiewicz left) (Lukasiewicz right) =+ Lukasiewicz (min 1 (1 - left + right))++instance (Ord a, Num a) => IntegralQuantale (Lukasiewicz a)++instance (Ord a, Num a) => ChainQuantale (Lukasiewicz a)++-- | Min-plus costs. The lattice order is the dual of the derived 'Ord': join+-- is the numeric minimum and 'bottom' is 'TropicalInfinity'. The quantale+-- laws hold over all of @a@; only integrality ('tensorUnit' as top) and the+-- truncated 'residual' require the nonnegative cone.+type Tropical :: Type -> Type+data Tropical a+ = TropicalFinite !a+ | TropicalInfinity+ deriving stock (Eq, Ord, Show)++instance Ord a => JoinSemilattice (Tropical a) where+ join = min++instance Ord a => BoundedJoinSemilattice (Tropical a) where+ bottom = TropicalInfinity++instance (Ord a, Num a) => Quantale (Tropical a) where+ tensor TropicalInfinity _ = TropicalInfinity+ tensor _ TropicalInfinity = TropicalInfinity+ tensor (TropicalFinite left) (TropicalFinite right) =+ TropicalFinite (left + right)+ tensorUnit = TropicalFinite 0++instance (Ord a, Num a) => CommutativeQuantale (Tropical a)++instance (Ord a, Num a) => ResiduatedQuantale (Tropical a) where+ residual TropicalInfinity _ = TropicalFinite 0+ residual (TropicalFinite _) TropicalInfinity = TropicalInfinity+ residual (TropicalFinite left) (TropicalFinite right) =+ TropicalFinite (max 0 (right - left))++instance (Ord a, Num a) => ChainQuantale (Tropical a)++tensors :: (Quantale a, Foldable foldable) => foldable a -> a+tensors =+ foldl' tensor tensorUnit
src-laws/Moonlight/Algebra/Effect/Laws.hs view
@@ -44,12 +44,11 @@ ) import Moonlight.Core qualified as Core import qualified Moonlight.Pale.Test.Laws.Algebraic as Algebraic-import Moonlight.Pale.Test.LawSuite- ( LawBundle,- hedgehogLawDefinition,- lawBundleHedgehog,- lawSuiteGroup,- renderLawBundles,+import Moonlight.Pale.Test.Laws.Suite+ ( LawSuite,+ lawGroup,+ namedHedgehogLaw,+ renderLawSuite, ) import Test.Tasty (TestTree, testGroup) import Test.Tasty.Hedgehog (testProperty)@@ -415,16 +414,14 @@ testsWithConfig config = testGroup "moonlight-algebra"- [ lawSuiteGroup- "laws"- (renderLawBundles id (algebraLawBundles config)),+ [ renderLawSuite (lawGroup "laws" (algebraLawSuites config)), representationBoundaryTests config, boolSemiringTests, latticeImplementationTests ] -algebraLawBundles :: AlgebraGeneratorConfig -> [LawBundle String]-algebraLawBundles config =+algebraLawSuites :: AlgebraGeneratorConfig -> [LawSuite]+algebraLawSuites config = let genFreeAbelianInt = genFreeAbelianGroup config (genIntBasis config) genAdditiveFreeAbelianInt = Additive <$> genFreeAbelianInt genAdditiveLaneVector = Additive <$> genLaneVector@@ -435,87 +432,87 @@ genPolynomialInteger = genPolynomial config genCoefficient genPowerSetAtom = genPowerSet config genAtom genSparseVecIntegerInt = genSparseVec config (genIntBasis config) genCoefficient- in [ lawBundleHedgehog+ in [ lawGroup "additive-wrapper"- [ hedgehogLawDefinition MonoidAssoc (genTripleOf genAdditiveFreeAbelianInt) (applyTriple monoidAssoc),- hedgehogLawDefinition MonoidLeftId genAdditiveFreeAbelianInt monoidLeftId,- hedgehogLawDefinition MonoidRightId genAdditiveFreeAbelianInt monoidRightId,- hedgehogLawDefinition GroupInvLeft genAdditiveFreeAbelianInt groupInvLeft,- hedgehogLawDefinition GroupInvRight genAdditiveFreeAbelianInt groupInvRight,- hedgehogLawDefinition AbelianComm (genPairOf genAdditiveFreeAbelianInt) (applyPair abelianComm)+ [ namedHedgehogLaw MonoidAssoc (genTripleOf genAdditiveFreeAbelianInt) (applyTriple monoidAssoc),+ namedHedgehogLaw MonoidLeftId genAdditiveFreeAbelianInt monoidLeftId,+ namedHedgehogLaw MonoidRightId genAdditiveFreeAbelianInt monoidRightId,+ namedHedgehogLaw GroupInvLeft genAdditiveFreeAbelianInt groupInvLeft,+ namedHedgehogLaw GroupInvRight genAdditiveFreeAbelianInt groupInvRight,+ namedHedgehogLaw AbelianComm (genPairOf genAdditiveFreeAbelianInt) (applyPair abelianComm) ],- lawBundleHedgehog+ lawGroup "lane-vector-additive"- [ hedgehogLawDefinition MonoidAssoc (genTripleOf genAdditiveLaneVector) (applyTriple laneVectorMonoidAssoc),- hedgehogLawDefinition MonoidLeftId genAdditiveLaneVector laneVectorMonoidLeftId,- hedgehogLawDefinition MonoidRightId genAdditiveLaneVector laneVectorMonoidRightId,- hedgehogLawDefinition GroupInvLeft genAdditiveLaneVector laneVectorGroupInvLeft,- hedgehogLawDefinition GroupInvRight genAdditiveLaneVector laneVectorGroupInvRight,- hedgehogLawDefinition AbelianComm (genPairOf genAdditiveLaneVector) (applyPair laneVectorAbelianComm),- hedgehogLawDefinition LaneVectorSubtraction (genPairOf genLaneVector) (applyPair laneVectorSubtraction)+ [ namedHedgehogLaw MonoidAssoc (genTripleOf genAdditiveLaneVector) (applyTriple laneVectorMonoidAssoc),+ namedHedgehogLaw MonoidLeftId genAdditiveLaneVector laneVectorMonoidLeftId,+ namedHedgehogLaw MonoidRightId genAdditiveLaneVector laneVectorMonoidRightId,+ namedHedgehogLaw GroupInvLeft genAdditiveLaneVector laneVectorGroupInvLeft,+ namedHedgehogLaw GroupInvRight genAdditiveLaneVector laneVectorGroupInvRight,+ namedHedgehogLaw AbelianComm (genPairOf genAdditiveLaneVector) (applyPair laneVectorAbelianComm),+ namedHedgehogLaw LaneVectorSubtraction (genPairOf genLaneVector) (applyPair laneVectorSubtraction) ],- lawBundleHedgehog+ lawGroup "free-monoid"- [ hedgehogLawDefinition FreeMonoidAssoc (genTripleOf genFreeMonoidInt) (applyTriple freeMonoidAssoc),- hedgehogLawDefinition FreeMonoidLeftId genFreeMonoidInt freeMonoidLeftId,- hedgehogLawDefinition FreeMonoidRightId genFreeMonoidInt freeMonoidRightId+ [ namedHedgehogLaw FreeMonoidAssoc (genTripleOf genFreeMonoidInt) (applyTriple freeMonoidAssoc),+ namedHedgehogLaw FreeMonoidLeftId genFreeMonoidInt freeMonoidLeftId,+ namedHedgehogLaw FreeMonoidRightId genFreeMonoidInt freeMonoidRightId ],- lawBundleHedgehog+ lawGroup "ring"- [ hedgehogLawDefinition RingAddAssoc (genTripleOf genZn7) (applyTriple ringAddAssoc),- hedgehogLawDefinition RingMulComm (genPairOf genZn7) (applyPair ringMulComm)+ [ namedHedgehogLaw RingAddAssoc (genTripleOf genZn7) (applyTriple ringAddAssoc),+ namedHedgehogLaw RingMulComm (genPairOf genZn7) (applyPair ringMulComm) ],- lawBundleHedgehog+ lawGroup "lattice"- [ hedgehogLawDefinition (CommonLaw LatticeAbsorptionJoin) (genPairOf genPowerSetAtom) (applyPair latticeAbsorptionJoin),- hedgehogLawDefinition (CommonLaw LatticeAbsorptionMeet) (genPairOf genPowerSetAtom) (applyPair latticeAbsorptionMeet)+ [ namedHedgehogLaw (CommonLaw LatticeAbsorptionJoin) (genPairOf genPowerSetAtom) (applyPair latticeAbsorptionJoin),+ namedHedgehogLaw (CommonLaw LatticeAbsorptionMeet) (genPairOf genPowerSetAtom) (applyPair latticeAbsorptionMeet) ],- lawBundleHedgehog+ lawGroup "heyting"- [ hedgehogLawDefinition HeytingImpliesSelfTop genPowerSetAtom heytingImpliesSelfTop,- hedgehogLawDefinition HeytingMeetImplication (genPairOf genPowerSetAtom) (applyPair heytingMeetImplication),- hedgehogLawDefinition HeytingConsequentMeetImplication (genPairOf genPowerSetAtom) (applyPair heytingConsequentMeetImplication),- hedgehogLawDefinition HeytingImplicationDistributesMeet (genTripleOf genPowerSetAtom) (applyTriple heytingImplicationDistributesMeet),- hedgehogLawDefinition HeytingNegDefault genPowerSetAtom heytingNegDefault,- hedgehogLawDefinition HeytingEquivalenceDefault (genPairOf genPowerSetAtom) (applyPair heytingEquivalenceDefault)+ [ namedHedgehogLaw HeytingImpliesSelfTop genPowerSetAtom heytingImpliesSelfTop,+ namedHedgehogLaw HeytingMeetImplication (genPairOf genPowerSetAtom) (applyPair heytingMeetImplication),+ namedHedgehogLaw HeytingConsequentMeetImplication (genPairOf genPowerSetAtom) (applyPair heytingConsequentMeetImplication),+ namedHedgehogLaw HeytingImplicationDistributesMeet (genTripleOf genPowerSetAtom) (applyTriple heytingImplicationDistributesMeet),+ namedHedgehogLaw HeytingNegDefault genPowerSetAtom heytingNegDefault,+ namedHedgehogLaw HeytingEquivalenceDefault (genPairOf genPowerSetAtom) (applyPair heytingEquivalenceDefault) ],- lawBundleHedgehog+ lawGroup "module"- [ hedgehogLawDefinition ModuleDistribScalarAdd (genTriple genCoefficient genCoefficient genPolynomialInteger) (applyTriple moduleDistribScalarAdd),- hedgehogLawDefinition ModuleDistribVectorAdd (genTriple genCoefficient genPolynomialInteger genPolynomialInteger) (applyTriple moduleDistribVectorAdd)+ [ namedHedgehogLaw ModuleDistribScalarAdd (genTriple genCoefficient genCoefficient genPolynomialInteger) (applyTriple moduleDistribScalarAdd),+ namedHedgehogLaw ModuleDistribVectorAdd (genTriple genCoefficient genPolynomialInteger genPolynomialInteger) (applyTriple moduleDistribVectorAdd) ],- lawBundleHedgehog+ lawGroup "unit"- [ hedgehogLawDefinition UnitInverseOne (pure ()) unitInverseOne,- hedgehogLawDefinition UnitInverseCorrect genIntegerUnit unitInverseCorrect,- hedgehogLawDefinition UnitInverseAbsent (genIntegerNonUnit config) unitInverseAbsent+ [ namedHedgehogLaw UnitInverseOne (pure ()) unitInverseOne,+ namedHedgehogLaw UnitInverseCorrect genIntegerUnit unitInverseCorrect,+ namedHedgehogLaw UnitInverseAbsent (genIntegerNonUnit config) unitInverseAbsent ],- lawBundleHedgehog+ lawGroup "gcd"- [ hedgehogLawDefinition GcdDividesLeft (genNonZeroGcdContext config) gcdDividesLeft,- hedgehogLawDefinition GcdDividesRight (genNonZeroGcdContext config) gcdDividesRight,- hedgehogLawDefinition ExtGcdBezout (genPairOf genInteger) (applyPair extGcdBezout),- hedgehogLawDefinition ModInverseCorrect (genModInverseContext isUnit config) modInverseCorrect,- hedgehogLawDefinition ModInverseAbsentNonunit (genModInverseContext (not . isUnit) config) modInverseAbsentNonunit,- hedgehogLawDefinition CrtSound (genCrtSoundContext config) crtSound+ [ namedHedgehogLaw GcdDividesLeft (genNonZeroGcdContext config) gcdDividesLeft,+ namedHedgehogLaw GcdDividesRight (genNonZeroGcdContext config) gcdDividesRight,+ namedHedgehogLaw ExtGcdBezout (genPairOf genInteger) (applyPair extGcdBezout),+ namedHedgehogLaw ModInverseCorrect (genModInverseContext isUnit config) modInverseCorrect,+ namedHedgehogLaw ModInverseAbsentNonunit (genModInverseContext (not . isUnit) config) modInverseAbsentNonunit,+ namedHedgehogLaw CrtSound (genCrtSoundContext config) crtSound ],- lawBundleHedgehog+ lawGroup "canonicalization"- [ hedgehogLawDefinition PolynomialCanonicalizationIdempotent genPolynomialInteger polynomialCanonicalizationIdempotent+ [ namedHedgehogLaw PolynomialCanonicalizationIdempotent genPolynomialInteger polynomialCanonicalizationIdempotent ],- lawBundleHedgehog+ lawGroup "hedgehog-generators"- [ hedgehogLawDefinition ZnGeneratorNormalized genZn7 znGeneratorNormalized,- hedgehogLawDefinition PolynomialGeneratorCanonical genPolynomialInteger polynomialGeneratorCanonical,- hedgehogLawDefinition FreeAbelianGeneratorCanonical genFreeAbelianInt freeAbelianGeneratorCanonical,- hedgehogLawDefinition SparseVecGeneratorCanonical genSparseVecIntegerInt sparseVecGeneratorCanonical,- hedgehogLawDefinition PowerSetGeneratorCanonical genPowerSetAtom powerSetGeneratorCanonical+ [ namedHedgehogLaw ZnGeneratorNormalized genZn7 znGeneratorNormalized,+ namedHedgehogLaw PolynomialGeneratorCanonical genPolynomialInteger polynomialGeneratorCanonical,+ namedHedgehogLaw FreeAbelianGeneratorCanonical genFreeAbelianInt freeAbelianGeneratorCanonical,+ namedHedgehogLaw SparseVecGeneratorCanonical genSparseVecIntegerInt sparseVecGeneratorCanonical,+ namedHedgehogLaw PowerSetGeneratorCanonical genPowerSetAtom powerSetGeneratorCanonical ],- lawBundleHedgehog+ lawGroup "orientation"- [ hedgehogLawDefinition OrientationGroupInvLeft genOrientation orientationGroupInvLeft,- hedgehogLawDefinition OrientationGroupInvRight genOrientation orientationGroupInvRight,- hedgehogLawDefinition OrientationAbelianComm (genPairOf genOrientation) (applyPair orientationAbelianComm)+ [ namedHedgehogLaw OrientationGroupInvLeft genOrientation orientationGroupInvLeft,+ namedHedgehogLaw OrientationGroupInvRight genOrientation orientationGroupInvRight,+ namedHedgehogLaw OrientationAbelianComm (genPairOf genOrientation) (applyPair orientationAbelianComm) ] ]
src-public/Moonlight/Algebra.hs view
@@ -20,8 +20,9 @@ * Free structures and actions — @FreeMonoid@, @FreeAbelianGroup@, @EndoPatch@, and monoid @Action@s with their invertible, group-acting refinement. * Lattices — join/meet semilattices up through distributive, Heyting and Boolean- algebras, and the two-element sign @Orientation@ group. Compiled finite- lattices live in the public @finite-lattice@ sublibrary, @Moonlight.FiniteLattice@.+ algebras, quantales (commutative, residuated) with the Viterbi, Łukasiewicz+ and tropical carriers, and the two-element sign @Orientation@ group. Compiled+ finite lattices live in the public @finite-lattice@ sublibrary, @Moonlight.FiniteLattice@. * Rings and arithmetic — the semiring and commutative-ring laws extended with the @IntegralDomain@, @GCDDomain@ and @EuclideanDomain@ refinements, modular arithmetic (@Zn@), quotient rings @R/(n)@ (@Quotient@), @NumberTheory@ and @GCD@.@@ -52,8 +53,9 @@ module EndoPatch, -- * Actions module Action,- -- * Lattices and orientation+ -- * Lattices, quantales and orientation module Lattice,+ module Quantale, module Orientation, -- * Rings, modular arithmetic and number theory module Ring,@@ -95,6 +97,7 @@ import Moonlight.Algebra.Pure.Polynomial as Polynomial import Moonlight.Algebra.Pure.PowerSet as PowerSet import Moonlight.Algebra.Pure.Product as Product+import Moonlight.Algebra.Pure.Quantale as Quantale import Moonlight.Algebra.Pure.Quotient as Quotient import Moonlight.Algebra.Pure.Ring as Ring import Moonlight.Algebra.Pure.SparseVec as SparseVec
test/abstract/AbstractTests.hs view
@@ -5,6 +5,7 @@ import Moonlight.Algebra.Effect.Laws qualified as EffectLaws import OrderedLatticeSpec qualified+import QuantaleSpec qualified import SparseVecSpec qualified import Test.Tasty ( TestTree,@@ -17,5 +18,6 @@ "moonlight-algebra" [ EffectLaws.tests, OrderedLatticeSpec.tests,+ QuantaleSpec.tests, SparseVecSpec.tests ]
test/abstract/Main.hs view
@@ -1,8 +1,8 @@ module Main (main) where import AbstractTests qualified-import Moonlight.Pale.Test.Runner (runTestTree)+import Test.Tasty (defaultMain) main :: IO () main =- runTestTree AbstractTests.tests+ defaultMain AbstractTests.tests
+ test/abstract/QuantaleSpec.hs view
@@ -0,0 +1,224 @@+module QuantaleSpec+ ( tests,+ )+where++import Data.List (maximumBy)+import Data.Ratio ((%))+import Hedgehog qualified as HH+import Hedgehog.Gen qualified as Gen+import Hedgehog.Range qualified as Range+import Moonlight.Algebra+ ( BoundedJoinSemilattice (..),+ ChainOrder (..),+ ChainQuantale,+ IntegralQuantale,+ JoinSemilattice (..),+ Quantale (..),+ ResiduatedQuantale (..),+ joinLeq,+ )+import Moonlight.Algebra+ ( Lukasiewicz (..),+ Tropical (..),+ Viterbi (..),+ )+import Test.Tasty+ ( TestTree,+ testGroup,+ )+import Test.Tasty.Hedgehog+ ( testProperty,+ )++tests :: TestTree+tests =+ testGroup+ "quantale"+ [ quantaleLawTests "Bool" Gen.bool,+ quantaleLawTests "Viterbi Rational" genViterbiRational,+ quantaleLawTests "Lukasiewicz Rational" genLukasiewiczRational,+ quantaleLawTests "Tropical Rational" genTropicalRational,+ quantaleLawTests "(Bool, Viterbi Rational)" genBoolViterbiPair,+ testGroup+ "integral markers"+ [ integralQuantaleLawTests "Bool" Gen.bool,+ integralQuantaleLawTests "Viterbi Rational" genViterbiRational,+ integralQuantaleLawTests "Lukasiewicz Rational" genLukasiewiczRational,+ integralQuantaleLawTests "(Bool, Viterbi Rational)" genBoolViterbiPair+ ],+ testGroup+ "chain markers"+ [ chainQuantaleLawTests "Bool" Gen.bool,+ chainQuantaleLawTests "Viterbi Rational" genViterbiRational,+ chainQuantaleLawTests "Lukasiewicz Rational" genLukasiewiczRational,+ chainQuantaleLawTests "Tropical Rational (signed)" genTropicalSignedRational+ ],+ testGroup+ "the chain order induced by a selective join"+ [ chainOrderLawTests "Viterbi Rational" genViterbiRational,+ chainOrderLawTests "Lukasiewicz Rational" genLukasiewiczRational,+ chainOrderLawTests "Tropical Rational (signed)" genTropicalSignedRational+ ]+ ]++quantaleLawTests ::+ (ResiduatedQuantale carrier, Eq carrier, Show carrier) =>+ String ->+ HH.Gen carrier ->+ TestTree+quantaleLawTests label gen =+ testGroup+ label+ [ testProperty "tensor is associative" $ HH.property $ do+ left <- HH.forAll gen+ middle <- HH.forAll gen+ right <- HH.forAll gen+ tensor (tensor left middle) right HH.=== tensor left (tensor middle right),+ testProperty "tensorUnit is a left identity" $ HH.property $ do+ value <- HH.forAll gen+ tensor tensorUnit value HH.=== value,+ testProperty "tensorUnit is a right identity" $ HH.property $ do+ value <- HH.forAll gen+ tensor value tensorUnit HH.=== value,+ testProperty "tensor is commutative" $ HH.property $ do+ left <- HH.forAll gen+ right <- HH.forAll gen+ tensor left right HH.=== tensor right left,+ testProperty "tensor distributes over join on the left" $ HH.property $ do+ left <- HH.forAll gen+ middle <- HH.forAll gen+ right <- HH.forAll gen+ tensor left (join middle right)+ HH.=== join (tensor left middle) (tensor left right),+ testProperty "tensor distributes over join on the right" $ HH.property $ do+ left <- HH.forAll gen+ middle <- HH.forAll gen+ right <- HH.forAll gen+ tensor (join left middle) right+ HH.=== join (tensor left right) (tensor middle right),+ testProperty "bottom annihilates tensor on the left" $ HH.property $ do+ value <- HH.forAll gen+ tensor bottom value HH.=== bottom,+ testProperty "bottom annihilates tensor on the right" $ HH.property $ do+ value <- HH.forAll gen+ tensor value bottom HH.=== bottom,+ testProperty "residual is right adjoint to tensor" $ HH.property $ do+ left <- HH.forAll gen+ middle <- HH.forAll gen+ right <- HH.forAll gen+ joinLeq (tensor left middle) right HH.=== joinLeq left (residual middle right),+ testProperty "tensorUnit is the greatest element" $ HH.property $ do+ value <- HH.forAll gen+ HH.assert (joinLeq value tensorUnit)+ ]++integralQuantaleLawTests ::+ (IntegralQuantale carrier, Eq carrier, Show carrier) =>+ String ->+ HH.Gen carrier ->+ TestTree+integralQuantaleLawTests label gen =+ testProperty (label <> ": tensor is two-sided deflationary") $ HH.property $ do+ left <- HH.forAll gen+ right <- HH.forAll gen+ HH.assert (joinLeq (tensor left right) left)+ HH.assert (joinLeq (tensor left right) right)++chainQuantaleLawTests ::+ (ChainQuantale carrier, Eq carrier, Show carrier) =>+ String ->+ HH.Gen carrier ->+ TestTree+chainQuantaleLawTests label gen =+ testProperty (label <> ": join is selective") $ HH.property $ do+ left <- HH.forAll gen+ right <- HH.forAll gen+ HH.assert (join left right == left || join left right == right)++chainOrderLawTests ::+ (ChainQuantale carrier, Eq carrier, Show carrier) =>+ String ->+ HH.Gen carrier ->+ TestTree+chainOrderLawTests label gen =+ testGroup+ label+ [ testProperty "strict ascent is the lattice order minus equality" $ HH.property $ do+ left <- HH.forAll gen+ right <- HH.forAll gen+ (compare (ChainOrder left) (ChainOrder right) == LT)+ HH.=== (joinLeq left right && left /= right),+ testProperty "the order is antisymmetric" $ HH.property $ do+ left <- HH.forAll gen+ right <- HH.forAll gen+ compare (ChainOrder left) (ChainOrder left) HH.=== EQ+ (chainOrderLeq left right && chainOrderLeq right left)+ HH.=== (left == right),+ testProperty "the order is transitive" $ HH.property $ do+ left <- HH.forAll gen+ middle <- HH.forAll gen+ right <- HH.forAll gen+ let triple = [left, middle, right]+ HH.assert+ ( and+ [ not (chainOrderLeq lower between && chainOrderLeq between upper)+ || chainOrderLeq lower upper+ | lower <- triple,+ between <- triple,+ upper <- triple+ ]+ ),+ testProperty "the greatest element under the order attains the join" $ HH.property $ do+ values <- HH.forAll (Gen.list (Range.linear 1 12) gen)+ getChainOrder (maximumBy compare (map ChainOrder values))+ HH.=== foldr1 join values+ ]+ where+ chainOrderLeq :: (ChainQuantale value, Eq value) => value -> value -> Bool+ chainOrderLeq lower upper =+ compare (ChainOrder lower) (ChainOrder upper) /= GT++genUnitIntervalRational :: HH.Gen Rational+genUnitIntervalRational = do+ denominator <- Gen.integral (Range.linear 1 12)+ numerator <- Gen.integral (Range.linear 0 denominator)+ pure (numerator % denominator)++genViterbiRational :: HH.Gen (Viterbi Rational)+genViterbiRational =+ Viterbi <$> genUnitIntervalRational++genLukasiewiczRational :: HH.Gen (Lukasiewicz Rational)+genLukasiewiczRational =+ Lukasiewicz <$> genUnitIntervalRational++genTropicalRational :: HH.Gen (Tropical Rational)+genTropicalRational =+ Gen.frequency+ [ (1, pure TropicalInfinity),+ (6, TropicalFinite <$> genNonnegativeRational)+ ]++genTropicalSignedRational :: HH.Gen (Tropical Rational)+genTropicalSignedRational =+ Gen.frequency+ [ (1, pure TropicalInfinity),+ (6, TropicalFinite <$> genSignedRational)+ ]++genSignedRational :: HH.Gen Rational+genSignedRational = do+ denominator <- Gen.integral (Range.linear 1 12)+ numerator <- Gen.integral (Range.linearFrom 0 (-12 * denominator) (12 * denominator))+ pure (numerator % denominator)++genNonnegativeRational :: HH.Gen Rational+genNonnegativeRational = do+ denominator <- Gen.integral (Range.linear 1 12)+ numerator <- Gen.integral (Range.linear 0 (12 * denominator))+ pure (numerator % denominator)++genBoolViterbiPair :: HH.Gen (Bool, Viterbi Rational)+genBoolViterbiPair =+ (,) <$> Gen.bool <*> genViterbiRational
− test/aggregate/Main.hs
@@ -1,13 +0,0 @@-module Main (main) where--import AbstractTests qualified-import FiniteLatticeTests qualified-import Moonlight.Pale.Test.Runner (runTestTreeGroup)--main :: IO ()-main =- runTestTreeGroup- "moonlight-algebra"- [ AbstractTests.tests,- FiniteLatticeTests.tests- ]
+ test/coherence/Main.hs view
@@ -0,0 +1,10 @@+-- | Compile both focused test sections against their dependency union. Empty+-- imports retain module and instance coherence without executing the focused+-- behavioral suites a second time.+module Main (main) where++import AbstractTests ()+import FiniteLatticeTests ()++main :: IO ()+main = pure ()
test/finite-lattice/Main.hs view
@@ -1,8 +1,8 @@ module Main (main) where import FiniteLatticeTests qualified-import Moonlight.Pale.Test.Runner (runTestTree)+import Test.Tasty (defaultMain) main :: IO () main =- runTestTree FiniteLatticeTests.tests+ defaultMain FiniteLatticeTests.tests