algebra design
Design goal
algebra gives generic linear-algebra code a vocabulary for whole vector and
matrix objects that is honest about what each object can do. A trait may only
be implemented by a type that satisfies its laws, and an algorithm should be
able to ask for exactly the structure it uses: a shape, an abelian group, a
Hadamard ring, a transpose, or a matrix product. The package therefore defines
small traits ordered by inclusion instead of one Matrix or VectorSpace
trait. The API page lists the traits; this page explains
the mathematics they encode and the choices that follow from it.
Mathematical background
Modules and vector spaces
Let be a ring with unit. A (left) -module is an abelian group together with a scalar action , , such that for all and
A vector space is a module over a field. Most of linear algebra is stated for vector spaces, but most of the code only needs much less: matrix addition needs the abelian group, matrix multiplication needs a semiring of scalars, and only elimination needs division. Integer matrices, for example, form a -module and are not a vector space; requiring a field would exclude them from algorithms that never divide.
Coordinates
A dense vector of length over is an element of , a dense matrix an element of . Entry-wise addition makes both abelian groups; the scalar action makes them -modules. For fixed , the entry-wise product
makes a ring as well (the product ring), with unit .
Matrices as a category
Matrix multiplication is not an operation on one set. Its shape rule
says that matrices are the morphisms of a category whose objects are the natural numbers: an matrix is an arrow , multiplication is composition, and the identity matrix is the identity arrow on . A product is defined exactly when the arrows are composable. Over a fixed object the arrows (the square matrices) form a ring, the familiar .
Associativity of composition holds whenever is a semiring. For , , :
Commutativity of multiplication was never used, so the law holds for matrices over any semiring, including non-commutative ones such as quaternions. The same computation with shows , and distributivity of the product over matrix addition follows entry-wise from distributivity in .
Transpose
The transpose is the map from to . It is total and
The product rule needs more. For composable and :
The two sums agree term by term exactly when ,
that is, when the scalars commute. So
is a theorem for matrices over
a commutative ring and false in general.11 For a ring with an involution that reverses
products, , the conjugate transpose
does satisfy without
commutativity, because each term becomes .
This is why the concrete matrix types offer adjoint next to transpose. Transpose is a contravariant
functor only in the commutative case.
Design decisions
Abelian group instead of module
Problem. The natural trait for “a vector” is an -module, but a module has two carriers: the vectors and the scalars.
Options. (a) A Module trait whose scalar type is fixed, for example
Double. (b) A trait with an associated scalar type. (c) Only the additive
structure, leaving scalars to concrete methods.
Decision. (c): AdditiveVector and AdditiveMatrix state the abelian
group and nothing about scalars.
Why. MoonBit traits have a single Self parameter and no associated types,
so option (b) cannot be expressed. Option (a) would make every module over
Int, BigInt or a user scalar type unrepresentable, and would hard-code one
floating-point type into a public trait. Scalar multiplication therefore stays
a method of the concrete types (scale, left_scale, right_scale) where the
scalar type is known.
No zero in the vector traits
A runtime-shaped vector type has no single zero: the identity of
depends on . A trait method zero() -> Self would have to choose a length.
The traits therefore ask for Add, Neg and Sub only, and the group laws
are stated without a named zero:
The element is the zero of the right length. The upstream Zero
trait from luna-generic remains available for scalar types, where a single
zero exists.
Hadamard product as its own level
Mul on a vector type could mean the Hadamard product, a dot product, or a
cross product, and only the first is closed ( for all
). VecMulVector fixes the meaning to the Hadamard product and lives above
AdditiveVector, so an algorithm that only adds vectors does not exclude types
without a product. Scalar-valued products such as the dot product are maps
out of the category of vectors; they are methods of the
concrete backends (DenseVector::dot), not structure traits.
Matrix multiplication is partial and documented, not typed
Problem. On a runtime-shaped matrix type, * is defined only for
composable shapes. A trait method returning Self cannot report failure.
Options. (a) Put Mul into the smallest matrix trait. (b) Encode shapes in
types. (c) Separate shape, transpose and addition from multiplication, and let
each implementation document the behaviour outside the domain.
Decision. (c). TransposeMatrix and AdditiveMatrix are useful without
multiplication, and MatMulMatrix is a separate level whose implementors must
document their failure behaviour. A type with statically known shapes, such as
a fixed or matrix, implements MatMulMatrix with a
total *.
Why. MoonBit has no type-level naturals, so (b) is not available for
dynamic dimensions. Option (a) would force a partial operation onto every
matrix type, including ones that never multiply. Checked multiplication with a
Result remains available on the concrete types (@immut.Matrix::matmul),
where the error type is fixed.
Transpose returns Self
TransposeMatrix::transpose returns the same type. Transpose is total on every
shape, so it is a closed operation and fits a trait method. Whether the result
is materialized or a view is not part of the contract; the
container layer, by contrast, has a transpose that may
produce a different target type.
Correctness and invariants
The traits are empty or have one observation method, so correctness is a property of each implementation. The laws an implementation promises are:
| Level | Laws (whenever both sides are defined) |
|---|---|
AdditiveVector, AdditiveMatrix | abelian group laws; operations preserve shape |
VecMulVector | is a ring under + and *: associativity, distributivity |
TransposeMatrix | reversed; |
AdditiveMatrix | |
MatMulMatrix | ; distributivity; if the scalars commute |
Two caveats apply to concrete scalar types.
Fixed-width integers. Int is the ring , not
. The laws above hold exactly in that ring, because wrapping
addition and multiplication are the ring operations of
; a matrix product that overflows is still the
correct product modulo .
Floating point. Float and Double are not rings: addition is not
associative under rounding. The laws hold only up to rounding error, and tests
must compare with a tolerance. For an inner product of length computed in
any order, the standard model ,
, gives
entry-wise, where for Double.22 N. J. Higham, Accuracy and Stability of Numerical Algorithms,
2nd ed., SIAM, 2002, §3.1 and §3.5. The bound follows by applying the model to
each of the additions and multiplications of one inner product. Applying the bound twice,
each of and is within
of the exact product, , so
the two evaluation orders can differ by twice that amount. This is the scale a
tolerance-based comparison must allow.
Alternatives rejected
- A
VectorSpaceorModuletrait. Rejected until scalar association can be expressed without fixing a scalar type; see the first decision. - A shape-dependent
zero(rows, cols)method. It would duplicate the upstreamZerotrait with a different meaning and still could not serve generic code that does not know the shape. - Inner products and norms as structure traits. They map into the scalars,
depend on the scalar type (a norm into
Doubleis not a norm intoInt), and have several reasonable choices. They stay backend methods. - One
Matrixtrait with every operation. It would force partial multiplication and Hadamard products onto types that do not have them.
Boundaries
algebra does not define scalar traits (those come from luna-generic and
arithmetic), storage, element access, mutation or construction (those belong
to container), checked error reporting, decompositions,
solvers, norms or inner products. It does not provide implementations for the
concrete @immut and @mutable types; backends/default
does that through owned wrapper types.
Footnotes
-
For a ring with an involution that reverses products, , the conjugate transpose does satisfy without commutativity, because each term becomes . This is why the concrete matrix types offer
adjointnext totranspose. ↩ -
N. J. Higham, Accuracy and Stability of Numerical Algorithms, 2nd ed., SIAM, 2002, §3.1 and §3.5. The bound follows by applying the model to each of the additions and multiplications of one inner product. ↩