core design
Design goal
luna-generic gives LunaFlow a shared algebraic vocabulary. Packages such as
arithmetic, luna-complex, linear-algebra, and luna-poly should be able
to describe their requirements in terms of reusable traits instead of inventing
their own incompatible capability layers.
Main design decisions
- The trait graph is layered and intentionally small.
- Structural traits such as
Ring,Field,Integral, andNatare kept separate from operational traits such asZero,One,Inverse, andConjugate. - Conversions are split into two halves that meet at ℤ, represented by
BigInt. The target side is the canonical map ℤ ->R(FromInteger), which is unique and always a homomorphism. The source side isIntegral::normalize, which picks a representative and is a homomorphism only for ℤ itself.lift_tocomposes them and promises nothing about operations. - The halves are single-parameter traits because every conversion factors through ℤ, the initial ring: no trait has to relate two types.
IntegralextendsFromIntegerwith the lawfrom_integer(normalize(x)) == x, which makes an integral type a quotient of ℤ with chosen representatives.FromIntegertakes aBigIntrather than a generic integral source, so the traits do not refer to each other.- Unsigned types stop before additive inverse, so the abstraction stays mathematically honest.
Fieldmeans a commutative field. Its laws, like those of every structural trait, are a contract on the implementor, not something the compiler checks.
Mathematical background
Each structural trait is the signature of an algebraic structure, and the structure’s axioms are the laws an instance promises. With ranging over the carrier:
| Trait | Structure | Laws added to its supertraits |
|---|---|---|
AddMonoid | monoid | , |
MulMonoid | monoid | , |
AddGroup | group | |
MulGroup | group | |
Semiring | semiring | , , , |
Ring | ring | the AddGroup laws |
Field | field | , for , |
The supertrait graph mirrors the inclusions between the structures: every
ring is a semiring, every semiring is both an additive and a multiplicative
monoid, and so on. A function bounded by T : Ring may use exactly the
consequences of the ring axioms, which is what makes the generic code
correct for every instance.
A homomorphism of such structures preserves every operation of the signature:
Integers as quotients of ℤ
This section gives the mathematics behind FromNat, FromInteger,
Integral and lift_to. The core tutorial shows how
to use them without it.
The canonical map is unique
For every ring R there is exactly one ring homomorphism ℤ -> R. A ring
homomorphism φ must send 1 to 1, and additivity then forces
φ(n) = 1 + ... + 1 (n times) for n > 0 and φ(-n) = -φ(n). Conversely,
n ↦ n·1 preserves + and * by distributivity. The same argument gives
exactly one semiring homomorphism ℕ -> R for every semiring R. In
categorical terms ℕ and ℤ are initial objects.
The derivation in full, first for ℕ. Let be a semiring and define by recursion:
Additivity, by induction on (associativity of in ):
Multiplicativity, by induction on (absorption , additivity, distributivity):
Uniqueness: any semiring homomorphism satisfies and , the same recursion, so by induction.
For ℤ, let be a ring. Every integer is a difference of naturals; put . This is well defined, because means in ℕ, hence in , and adding to both sides (with commutative) gives . It is additive term by term, and multiplicative by distributivity:
A ring homomorphism must also satisfy , so it agrees with on negatives too, and is unique.11 In the language of category theory, ℕ is the initial object of the category of semirings and ℤ that of rings. ℤ is the Grothendieck group of the additive monoid ℕ, which is the construction used above.
Because the map depends only on R, it is a property of the target and fits
a single-parameter trait: FromNat::from_natural and
FromInteger::from_integer.
Fixed-width integers
Int adds and multiplies modulo 2^32, so as a ring it is ℤ/2^32. Its
from_integer is the reduction ℤ -> ℤ/2^32, which is surjective.
normalize goes the other way and picks one integer in every residue class,
the one in [-2^31, 2^31). The law from_integer(normalize(x)) == x says
exactly that normalize is a section of the reduction:
normalizeis injective, because it has a left inverse.- Its image contains exactly one element of every class: at most one because it is injective, and at least one because of the law.
- It is not a homomorphism:
normalize(2147483647 + 1) = -2^31, whilenormalize(2147483647) + normalize(1) = 2^31.
In symbols, with and the reduction, whose kernel is , the shipped instances use
with taking values in . Both are well defined, since and give the same value, and both satisfy , since each differs from by a multiple of . The two injectivity steps above, written out:
The failure of additivity is a multiple of the modulus:
For and on Int the difference is , so no
choice of representatives can repair it: is a homomorphism only when
, that is for BigInt.
The hom design shows what a section does preserve.
When a conversion is a homomorphism
lift_to : S -> R is R::from_integer composed with S::normalize. When
S is ℤ/m (with m = 0 for BigInt), a ring homomorphism ℤ/m -> R exists
if and only if m·1 = 0 in R:
- If
ψis one, then0 = ψ(0) = ψ(m·1) = m·1inR. - If
m·1 = 0, the canonical mapℤ -> Rsendsmℤto0and so factors through ℤ/m. It is unique becauseℤ -> ℤ/mis surjective.
In that case lift_to is this homomorphism: write the canonical map
ℤ -> R as ψ ∘ π with π : ℤ -> ℤ/m; then
lift_to = ψ ∘ π ∘ normalize = ψ. So:
Int64 -> Intis a homomorphism, because2^64 ≡ 0 (mod 2^32).Int -> Int64is not, because2^32 ≢ 0 (mod 2^64).- No fixed-width integer maps homomorphically into
BigInt,FloatorDouble, wherem·1 ≠ 0for everym > 0.
The same argument as one chain, with the canonical map and when :
For the two modulus examples, in ℤ/2^32, while in ℤ/2^64 because .
Why unsigned types stop at Semiring
UInt, UInt16 and UInt64 are read as natural numbers that wrap: Nat
promises non-negative representatives, and code over them treats values as
counts and sizes. ℕ has no additive inverses, so it is a semiring and not a
ring:
a contradiction. As an abstract ring the unsigned type is ℤ/2^k, which does
have negatives, . Exposing them would make -1 silently mean
in generic code written for rings, which is the confusion the
Nat reading avoids. The core library also provides no Neg for unsigned
types, and MoonBit does not let this package add an instance of a foreign
trait to a foreign type, so AddGroup could not be implemented without a
wrapper type anyway. The canonical map is still total: from_integer(-1) on
UInt is , the image of in ℤ/2^32.
Why the traits do not refer to each other
Every conversion factors through ℤ: S -> ℤ -> R. The first half depends
only on S (Integral), the second only on R (FromInteger), so neither
trait has to relate two types. FromInteger takes a BigInt rather than a
generic integral source, which lets Integral extend it without a cycle.
Fields and division rings
Field is Ring + Inverse + Div with commutative multiplication. The
commutativity is part of the contract even though no method states it.
Definitions
A division ring is a ring with in which every has a
two-sided inverse, . A field is a division ring
whose multiplication commutes, . The two differ only in that law,
and the method signatures of Ring + Inverse + Div cannot tell them apart.
The standard example of a division ring that is not a field is Hamilton’s quaternions ℍ, with basis and . From , multiplying on the right by gives , so ; similarly :
What breaks without commutativity
In any division ring the inverse of a product reverses the order:
The other order is the inverse of the other product, , and inversion is injective, so
In ℍ, , while
. Division is ambiguous in the same way:
and are different elements in general, and Div
provides only one of them.
Generic code bounded by F : Field may rely on : rewrite
as , compute as , or reorder
products to save work. A non-commutative type that implemented Field
would compile and then get wrong answers from such code. That is why the
trait states commutativity, and why a division ring that is not a field must
not implement it. Generic code that also works for division rings asks for
Ring + Inverse + Div and keeps the order of its factors.
Every finite division ring is commutative,22 Wedderburn’s little theorem (1905): a finite division ring is a field. Over the reals, Frobenius’ theorem (1877) adds that the only finite-dimensional associative division algebras are ℝ, ℂ and ℍ. so the distinction only arises for infinite types.
Floating-point instances
Float and Double implement Field up to rounding. Their multiplication
is commutative exactly, , because IEEE 754
rounds the exact product, which does not depend on the order. Associativity
and distributivity hold only approximately, and 0 has no inverse: inv
aborts on it.
Alternatives rejected
- A two-parameter conversion trait
Into[S, R]: MoonBit traits have onlySelf, and the factorization through ℤ makes it unnecessary. - One broad “number” trait: it would hide the difference between ℤ, ℤ/2^k, approximate reals and fields, which are exactly the differences generic code has to respect.
NatHomomorphismandIntegralHomomorphismas the conversion interface: they promised a homomorphism that a fixed-width source cannot give. They remain only as deprecated traits.- A separate division-ring trait: no shipped type needs it, and code that
must work without commutativity can ask for
Ring + Inverse + Div.
Boundaries
- This package does not define matrices, complex numbers, polynomials, parsing, or numerical algorithms.
- It does not erase the semantic difference between exact and approximate number systems.
- It does not check laws at compile time. The laws of every structural
trait, including the commutativity of
Field, are contracts on the implementor, tested with the tools of the hom API. - It does not model an arbitrary-precision ℕ: such a type is not a quotient
of ℤ, so it cannot be
Integral.
Footnotes
-
In the language of category theory, ℕ is the initial object of the category of semirings and ℤ that of rings. ℤ is the Grothendieck group of the additive monoid ℕ, which is the construction used above. ↩
-
Wedderburn’s little theorem (1905): a finite division ring is a field. Over the reals, Frobenius’ theorem (1877) adds that the only finite-dimensional associative division algebras are ℝ, ℂ and ℍ. ↩