Make interval-valued quantities part of the type system

[isomorphisms]

Current status — 2026-09-02

PARTIALLY_IMPLEMENTED. Verified open PR #44 supplies exact rational one-dimensional intervals, open/closed/half-open endpoints, empty handling, membership, and interval addition. Still open: multiplication/division, outward floating rounding, dependency/correlation such as x - x, unbounded forms, comparison outcomes, dimensional composition, and broader uncertainty/probability semantics. Do not treat the first kernel as completion of this issue.

---

Goal

Idriç should support interval-valued quantities as a type-system concern rather than treating intervals as an isolated numeric library idea.

The compiler should understand that a value may represent a set/range of possible values while preserving whatever other semantic structure the quantity carries:

Interval Float16
Interval Length
Interval Temperature
Interval (Quantity D)

Do not collapse the range, dimension, unit, or uncertainty source into a bare scalar prematurely.

Settled interval kernel

Preserve ordinary interval forms explicitly:

[a,b]
(a,b)
[a,b)
(a,b]
empty
unbounded endpoints where supported

Basic exact arithmetic should obey the usual enclosure semantics:

[1,3] + [4,9] = [5,12]

Multiplication should enclose all endpoint-product possibilities using the appropriate extrema.

When endpoint arithmetic is finite precision, especially Float16/Float32, require outward rounding where necessary so the represented interval contains the exact mathematical result. A numerically close but too-narrow interval is semantically wrong.

Dependency / correlation is deliberately not solved by naive intervals

Keep this forcing example visible:

x : [0,1]
x - x

Naive independent interval propagation gives [-1,1], while the compiler may know that both occurrences are the same x, in which case the exact result is 0.

Do not claim ordinary interval arithmetic solves this. Preserve room for expression identity, affine arithmetic, symbolic constraints, or another correlation-aware refinement later.

Nominal value, tolerance, uncertainty, and rounding are different facts

The August 29, 2026 discussion made this distinction explicit:

exact nominal value
manufacturing tolerance
measurement uncertainty
machine rounding

A nominal 1/4 inch can be an exact rational quantity. A physical socket labelled 1/4 inch is not thereby asserted to have mathematically exact physical width.

A useful first tolerance representation is simply an interval around an exact nominal value:

0.250 in ± 0.001 in
    -> [0.249 in, 0.251 in]

0.250 in +0.002/-0.001
    -> [0.249 in, 0.252 in]

This should compose with #28 dimensional/unit information.

Comparisons need not immediately become Bool

When ranges overlap, the type system should preserve the unresolved state rather than manufacture a Boolean answer. Candidate semantic outcomes include:

definitely_less
definitely_greater
definitely_equal where justified
overlap / unresolved

The final decision type is open; the requirement is not to erase uncertainty merely because the machine eventually has predicate bits.

This may also be useful for physical-fit questions: a tolerance-bearing socket/fastener relation can be definitely fitting, definitely not fitting, or unresolved/overlapping under the supplied tolerances.

Do not conflate interval uncertainty with infinitesimals

Keep distinct unless a later mathematical design explicitly relates them:

• dual-number infinitesimal ε² = 0 — first-order/tangent information;
• an ordered infinitesimal in an ordered field extension;
• measurement tolerance/uncertainty;
• finite-precision rounding error;
• a symbolic placeholder such as x ± ε whose semantics have not yet been chosen.

A dual number may become valuable elsewhere in Idriç, but it should not silently become the universal representation of physical tolerance.

Candidate tests

[1,3] + [4,9] = [5,12]
exact rational endpoints stay exact where possible
open/closed endpoint semantics are preserved
empty intervals are explicit
unbounded intervals are explicit
finite-precision operations round outward
Interval Length + Interval Length -> Interval Length
Interval Length + Interval Time -> unresolved/incompatible dimension
0.250 in ± 0.001 in -> [0.249 in,0.251 in]
x:[0,1]; x-x remains a documented dependency/correlation probe

Open questions

• endpoint openness at type level vs value level;
• exact representation of infinities and empty sets;
• correlation-aware refinement;
• whether a general uncertainty wrapper sits above intervals;
• efficient lowering of fixed-shape interval operations;
• interaction with numerical sensitivity work (Future: carry numerical sensitivity information through Idriç #14);
• how much static interval normalization belongs in elaboration;
• whether the separate intervals repository remains useful as a research notebook even if Idriç becomes the implementation home.

Related

• Future: carry numerical sensitivity information through Idriç #14 — numerical sensitivity
• Explore dimensional analysis in the type system #28 — dimensional analysis / units
• Represent instants, signed durations, and calendar periods as distinct mathematical types #31 — instants, signed durations, calendar periods
• Infer higher-math structures from operations, laws, and theorem constraints #42 — higher-math constraint inference
• Design notebook: exact intervals, outward rounding, tolerance, and dependency dilapidated-shed/intervals.idr#1 — interval research notebook
• Design note: preserve mathematical semantics through type constraints instead of erasing to scalars walnut-burgundy/computer-science#60 — broader semantic-preservation design note

Broader goal: make “this quantity lies somewhere in this range” a first-class mathematical fact that survives typing, inference, optimization, and lowering.

[isomorphisms]

August 29 clarification: real-world quantities and false precision

The motivation is broader than manufacturing tolerance. A recurring design complaint is that a real-world reported scalar is often not epistemically an exact scalar at all, even when the computer can print many digits.

Keep at least these layers distinct:

mathematical value / exact definition
machine representation precision
measurement resolution and error
sampling uncertainty
model uncertainty
population / estimand uncertainty
rounding / numerical error

Example: a program may compute 38.32695% exactly from the rows in one finite dataset. That does not imply that 38.32695% is known to be the true population preference rate to five decimal places. The sample statistic can be exact relative to the stored records while the inferential claim remains uncertain because of sampling, measurement, nonresponse, model assumptions, etc.

This is one reason not to equate wider floats with greater truth. More mantissa bits can reduce numerical representation error while contributing nothing to uncertainty in the underlying real-world quantity.

Intervals are the first rung, not the complete uncertainty theory

Intervals are attractive as the first implementation because they are simple, compositional, useful for tolerances/error bounds, and force the type system to stop pretending every quantity is one exact point.

But do not infer a probability distribution from an interval alone. An interval carries a set/range, not a probability measure. Gaussian/central-limit behavior requires additional probabilistic structure and hypotheses; a CLT is not a consequence of having interval-valued data.

Leave room later for several uncertainty-bearing forms, potentially including:

Interval A
bounded/error-budget A
probability distribution on A
empirical/sample distribution
confidence/credible set or another inferential object
likelihood/evidence-bearing estimate
mixture / alternative hypotheses

Exact names and hierarchy are OPEN. The requirement is that these forms not be flattened into Float merely because they eventually need numerical computation.

Ordering relative to calendar work

This strengthens the decision to implement the easy interval kernel before attempting a full calendar-time design. Calendar semantics involve not only arithmetic difficulty but genuine ambiguity/non-uniqueness/context dependence. Build a better vocabulary for partial knowledge and ambiguity first, then use the future time-library survey in walnut-burgundy/computer-science#61 before committing to civil-time semantics.

[isomorphisms]

Epsilon notation for open endpoints: keep it, but keep the semantic distinction visible

For the first interval implementation, open/closed endpoint membership should remain explicit data. Still, preserve the proposed ε notation as a useful surface intuition:

(a,b]  ~  [a+ε,b]
[a,b)  ~  [a,b-ε]

Do not currently define this ε to be the dual-number infinitesimal solely because Idriç also wants a type with ε² = 0. Dual numbers encode first-order nilpotent/tangent information; an ordered infinitesimal suitable for interval endpoint exclusion needs ordering semantics that ε²=0 alone does not provide.

So the implementation boundary is:

• interval openness/closedness is exact interval structure;
• ±ε may be accepted later as notation/sugar for endpoint exclusion;
• dual-number ε²=0 remains separately available;
• if a later type/knowledge layer supplies an ordered infinitesimal and a principled bridge, revisit the identification then.

Also do not assume that opening an endpoint by -ε can simply be inverted by +ε to restore a closed endpoint. Membership information must not be erased and guessed back.

This is intentionally a place where the language can be mathematically playful without making the core interval semantics depend on a dubious identification.

[isomorphisms]

Implementation cross-link: #44 now contains the deliberately narrow interval kernel from this issue: exact rational 1-D intervals, closed/open/half-open endpoints, empty reversed/open-singleton handling, membership, and interval addition. Endpoint openness carries explicit +epsilon / -epsilon boundary vocabulary, while nilpotent dual epsilon (epsilon^2 = 0) remains a distinct unordered type. Correlated uncertainty, probability, Gaussian inference, floating outward rounding, and interval multiplication/division remain deferred.