std.algebra

Generated by sema doc from crates/sema-runtime/assets/stdlib/sema/algebra.sema. Import with from std.algebra import …. For a narrative introduction see std.algebra.

algebra

std.algebra — the small algebraic hierarchy, with its laws attached (§3.9).

Part of the Sema standard library, written in Sema and shipped with the compiler (embedded via crates/sema-runtime/src/stdlib.rs). Import with from std.algebra import Semigroup, Monoid, Functor, Monad, identity.

Every trait here carries law clauses. A law is a universally quantified property over the implementing type: sema assure generates values for each free identifier and looks for a counterexample. Passing means no counterexample was found in the generated cases — falsification evidence, not a proof. Nothing here is verified in the mathematical sense.

What the type system can and cannot express

Sema’s generics are erased and carry only declared trait bounds (§5.29): there are no higher-kinded types, so Functor cannot be F[A] -> F[B]. map and bind are therefore endomorphic — Self -> Self — which is the honest projection of the real signature onto a type system without HKTs. A conforming type fixes its own element type.

Sema also has no associated (receiver-less) trait functions: every trait method takes self. Monoid.empty and Monad.pure would be associated functions in a language that has them, so here they take a witness receiver — any value of the type, used only to select the implementation, never read. Monoid states that explicitly as the empty_is_canonical law.

Laws that are stated, and laws that could not be

Expressible and enforced (see each trait): Semigroup associativity Monoid left_identity, right_identity, empty_is_canonical Functor preserves_identity Monad right_identity

Not expressible as a law, and deliberately NOT faked: Functor composition — map(map(x, f), g) == map(x, g ∘ f) quantifies over two arbitrary functions. A law quantifies free identifiers over Self only, and assurance generates no function values, so writing this as a law would produce a clause that reads right and tests nothing. Witnessed instances belong in a test. Monad left_identity — pure(v).bind(f) == f(v) quantifies over an arbitrary function f and over an arbitrary element v, which is not a Self value. Monad associativity — bind(bind(m, f), g) == bind(m, v => bind(f(v), g)) quantifies over two arbitrary functions.

Monad.right_identity survives because the only function it needs is v => pure(a, v), which the law can write itself.

def identity

def identity(value) !{}

Parameters

name	type
value	any

Effects !{}

trait Semigroup

An associative binary operation on a type.

trait Monoid

A semigroup with a two-sided identity element.

empty takes a witness receiver because Sema has no associated functions; the receiver selects the implementation and its value is never read, which is exactly what empty_is_canonical asserts.

trait Functor

A type that can map a function over its contents, structure preserved.

Endomorphic (Self -> Self) because the language has no higher-kinded types — see the module docstring.

trait Monad

A functor with pure and bind.

pure takes a witness receiver for the same reason Monoid.empty does.

def combine_all

def combine_all[T: Semigroup](xs: list[T]) -> T !{}

Parameters

name	type
xs	list[T]

Returns T

Effects !{}