Skip to content

index.md

Latest commit

 

History

History
89 lines (62 loc) · 4.18 KB

index.md

File metadata and controls

89 lines (62 loc) · 4.18 KB
Raw

luna-generic

This manual documents the planned v0.5.0 API of Luna-Flow/luna-generic.

Overview

luna-generic provides general algebraic traits and default numeric instances for Luna projects.

The current release candidate centers on three changes:

  • FromNat and FromInteger provide conversion operations; exact preservation requires a separate law certificate.
  • Integral is ℤ or a quotient ℤ/2^k, and normalize must be a section of its canonical map.
  • lift_to and Section keep the choice of a representative apart from homomorphisms.

Install

moon add Luna-Flow/luna-generic@0.4.0

Then import "Luna-Flow/luna-generic" in your moon.pkg. The package needs the MoonBit toolchain 0.10 or later (moonc ≥ 0.10).

Pages

The repository is one MoonBit package at src, documented as core. Its certificate subsystem, Hom and Section, has its own pages as hom.

Part Tutorial API Design
core: traits, conversions, instances tutorial API design
hom: homomorphisms and sections tutorial API design

Exported traits

  • AddMonoid, MulMonoid
  • AddGroup, MulGroup
  • Semiring, Ring, Field exact structures with explicit Law certificates
  • AddMonoidOps, SemiringOps, RingOps, FieldOps, NumOps operation bundles
  • FromNat, FromInteger
  • Integral, Nat
  • RoundedArithmetic for rounded floating operations
  • Deprecated: NatHomomorphism, IntegralHomomorphism

Exported operations and default types

  • Operations: One, Zero, Inverse, Conjugate
  • Default numeric types: Int, Int16, Int64, UInt, UInt16, UInt64, BigInt, Float, Double

Integer model

  • Integral covers signed integers, unsigned integers, and BigInt
  • Nat covers the integral types with non-negative representatives: UInt, UInt16, and UInt64
  • Fixed-width integers are ℤ/2^k; FromInteger::from_integer reduces modulo 2^k
  • Integral::normalize picks the representative of a value as a BigInt; IntegralTh records the round-trip law
  • Unsigned integer instances stop at Semiring

Conversions

  • FromInteger::from_integer converts out of BigInt: exact for BigInt, modular for fixed-width integers, rounded for Float and Double
  • lift_to(x) lifts to the representative and maps it into the target; it is a function, not a homomorphism
  • NatHomomorphism::from_nat and IntegralHomomorphism::from_integral are deprecated in favour of FromNat, FromInteger and lift_to

Generalized homomorphisms

  • Hom[S, A, B]: a certificate for maps preserving S, bound to source and target runtime Models; checked composition returns ModelMismatch
  • Section[S, Q, A]: a certificate that a lift picks one representative per class of a quotient; Section::of_integral is the canonical one for integral types
  • Signature tags: AddMonoidSig, MulMonoidSig, AddGroupSig, SemiringSig, RingSig
  • Algebra dictionaries Algebra[S, A], operations Op[A], the product type Prod[A, B] and reduct witnesses Reduct[S, T]
  • Hom::check / Hom::check_by test the homomorphism laws on samples with strict, lax or approximate strength
  • Hom::check_models / Hom::check_models_by add exact runtime Model identity checks to finite diagnostics
  • See the hom API, tutorial and design

Where to read next

The core tutorial writes small generic algorithms against these traits. The core API lists every exported trait and instance, and the core design explains why the hierarchy and the conversions are shaped this way.

  • New to the package: read the core tutorial, then the hom tutorial.
  • Using it in a library: keep the core API and the hom API at hand; each trait lists the laws an instance must satisfy.
  • Contributing: read both design pages, core and hom, before changing a trait or adding an inference rule.

Validation

Recommended release checks:

moon check
moon test