quantity

Documentation

Overview

Package quantity is the QUANTITY STRATUM: the usage semiring that the quantitative type theory threads through binders (Phase 5), kept behind an interface so the lattice is a swappable module.

The annotation DOMAIN lives in core (core.Qty: 0, 1, ω) because annotations are part of a term's identity and are hashed; this package supplies the RULES — how usages add across occurrences and multiply through nesting — and the compatibility judgment the elaborator's usage checker applies at each binder. The 0-fragment is the erasure boundary the codegen stratum reads.

Index

• type Semiring
  • func Default() Semiring
• type ZeroOneOmega
  • func (ZeroOneOmega) Add(a, b core.Qty) core.Qty
  • func (ZeroOneOmega) Compatible(declared, used core.Qty) bool
  • func (ZeroOneOmega) Mul(a, b core.Qty) core.Qty
  • func (ZeroOneOmega) One() core.Qty
  • func (ZeroOneOmega) Zero() core.Qty

Types

type Semiring

type Semiring interface {
	Zero() core.Qty
	One() core.Qty
	Add(a, b core.Qty) core.Qty
	Mul(a, b core.Qty) core.Qty
	// Compatible reports whether an observed usage satisfies a declared
	// annotation (0 requires unused; 1 requires exactly once; ω accepts any).
	Compatible(declared, used core.Qty) bool
}

Semiring abstracts the usage arithmetic: an additive monoid (Zero, Add) for combining usages of distinct occurrences, and a multiplicative monoid (One, Mul) for composing usage through nested positions.

func Default

func Default() Semiring

Default returns the 0/1/ω semiring, Rune v1's sole quantity-stratum implementation.

type ZeroOneOmega

type ZeroOneOmega struct{}

ZeroOneOmega is the default usage semiring: Atkey's 0/1/ω lattice. Zero means erased, One linear, Omega unrestricted. Addition saturates: two nonzero usages make ω. Multiplication is annihilated by 0 and saturates to ω unless an operand is 1.

func (ZeroOneOmega) Add

func (ZeroOneOmega) Add(a, b core.Qty) core.Qty

func (ZeroOneOmega) Compatible

func (ZeroOneOmega) Compatible(declared, used core.Qty) bool

func (ZeroOneOmega) Mul

func (ZeroOneOmega) Mul(a, b core.Qty) core.Qty

func (ZeroOneOmega) One

func (ZeroOneOmega) One() core.Qty

func (ZeroOneOmega) Zero

func (ZeroOneOmega) Zero() core.Qty