Exact rationals.
Divide-by-zero is a type error.

The type carries its own guarantees

A Reduced is a numerator and denominator bundled with two proofs: that the denominator is positive, and that numerator and denominator are coprime (the fraction is in lowest terms).

-- std/rational_reduced.kan — invariants as PROOF fields
def Reduced : U
  = (num : Int)                          -- the sign lives in the numerator
  * (den : Nat)
  * (Lt zero den)                        -- den > 0        — a proof, not a comment
  * (Coprime (natAbs num) den)           -- lowest terms   — a proof

Because those fields are proofs, a value of type Reduced is one the checker has verified is well-formed. There is no raw back door that builds a 3/0; the smart constructor reduce divides out gcd(|num|, den) and discharges all four obligations for you.

✕ You cannot divide by zero

Building a rational requires a proof that the denominator is positive — you literally cannot write one with denominator zero, because there is no proof of Lt zero zero to hand over. And reciprocal/division return an Option: none exactly when the input is the zero rational. It is honest arithmetic, not a runtime guard bolted on afterward.

def reduce : (n : Int) -> (d : Nat) -> Lt zero d -> Reduced   -- needs a proof d > 0

def recipR : Reduced -> Option Reduced          -- none  ⇔  the zero rational
def divR   : Reduced -> Reduced -> Option Reduced -- none  ⇔  dividing by zero

Contrast a language where 1.0/0.0 silently yields inf, or an integer 1/0 crashes at runtime. Here the possibility is closed off in the type.

= Exact arithmetic, always in lowest terms

Every operation is exact and returns a result that is again provably in lowest terms (each recomputes and re-reduces). And because the form is canonical, structural equality is mathematical equality — eqR needs no cross-multiplication.

def addR : Reduced -> Reduced -> Reduced      -- +   (exact, re-reduced)
def mulR : Reduced -> Reduced -> Reduced      -- ×
def subR : Reduced -> Reduced -> Reduced      -- −
def eqR  : Reduced -> Reduced -> Bool         -- decidable equality on ℚ

-- 1/2 + 1/3 — building it type-checks, so every obligation was discharged
def demo_sum : Reduced = addR (reduce (pos 1) 2 p) (reduce (pos 1) 3 q)

Built on a verified gcd — no axioms

“Lowest terms” is not asserted; it is proven. Underneath sits a full verified Euclidean tower, entirely axiom-free: verified division (a = q·b + r ∧ r < b), a verified gcd that provably divides both arguments and is maximal, and the theorem that dividing by the gcd yields a coprime pair. The rational’s coprimality field is exactly that theorem, applied.

-- std/gcd.kan
def gcd_dvd      : (Dvd (gcdI a b) a) * (Dvd (gcdI a b) b)      -- divides both
def gcd_greatest : Dvd c a -> Dvd c b -> Dvd c (gcdI a b)       -- maximal
def reduce_coprime : Lt zero (gcdI a b) -> Coprime (a/g) (b/g)  -- lowest terms, proven

What’s next: promoting the field laws (associativity, distributivity of the rational operations) from “they compute correctly” to “proven as theorems.” The safety guarantees above already hold today.

Check it yourself

Every snippet is real code from the repository.

$ kan check std/rational_reduced.kan
# ...every definition type-checks — so divide-by-zero really is impossible here.

exact · lowest terms, proven · divide-by-zero is a type error