Numbers, all the way out
A real number in Kan is a process, not a bit pattern: ask for more digits and
it computes them — exactly. No floats, no rounding, no NaN, and no way to divide by zero.
√2, π, e are not stored — they are run. Request precision ε and Kan hands back a rational within ε. There is no last digit; there is only the next one.
Kan already has exact rationals. A constructive real goes one step further: it is a function from a precision level to a rational approximation, guaranteed to converge.
-- std/creal.kan — `x n` is a rational within 1/2ⁿ of the true value x def CReal : U = Nat -> Rational
Every irrational you can name is one of these — √2, π, e, and anything you can write as a convergent process. Arithmetic propagates precision: to get a sum to within 1/2ⁿ, Kan asks each summand for 1/2ⁿ⁺¹; multiplication bounds the operands and asks for as much as it needs. Nothing ever rounds — if a result looks off, you just ask for more digits.
Read a real off with scaledFloor x d = ⌊x·10ᵈ⌋ — the first d decimal digits.
These are real outputs, and kan run, the OCaml backend, and the C backend all agree on them:
$ kan run examples/creal.kan 14142135623 -- √2 = 1.4142135623… 31415926535 -- π = 3.1415926535… (Machin's formula) 27182818284 -- e = 2.7182818284… (Σ 1/k!) 2000000 -- √2 · √2 = 2 (exactly, up to the ε you stop at) 7071067811 -- 1/√2 = 0.7071067811…
Ask for 10 digits and you get 10; ask for 100 and Kan computes 100. The number is the program.
Dividing reals is where floating point invents inf and NaN. Kan instead
requires evidence that the divisor is bounded away from zero — an apartness witness — before
it will divide. No witness, no division; it is a type-level obligation, the same idea that makes the
rationals’ denominators nonzero, lifted to reals.
def recipC : CReal -> Apart0 -> CReal -- 1/x needs |x| bounded off 0 def divC : CReal -> CReal -> Apart0 -> CReal -- x / y, evidence-gated
Honest limits, inherent to constructive reals (not to Kan): equality is undecidable — there is
deliberately no x == y on reals; the positive notion is apartness. Order is decidable only up to
a chosen tolerance. And only computable reals are representable — which is every real you can name.
Every number above is real code from the repository, computed and cross-checked by three backends.
$ kan run examples/creal.kan # √2, π, e, and arithmetic — to ten places
exact · computed to any precision · divide-by-zero is a type error