Skip to content

Add exact units, signed time, and interval type-system core - #44

Open
isomorphisms wants to merge 7 commits into
Idriçfrom
examples/units-time-intervals
Open

Add exact units, signed time, and interval type-system core#44
isomorphisms wants to merge 7 commits into
Idriçfrom
examples/units-time-intervals

Conversation

@isomorphisms

@isomorphisms isomorphisms commented Aug 29, 2026

Copy link
Copy Markdown
Owner

Scope

Small tests-first implementation of the algebraically settled slice from #28, #30, and #31.

Exact quantities / dimensions

  • exact rational fixture scalar;
  • dimension exponents for Length/Mass/Time;
  • multiplication/division normalize compound dimensions;
  • exact metre/cm/mm/in/ft conversions;
  • litre and explicitly named US gallon/quart/pint/cup scales;
  • gallon / second typechecks as Volume / Time without a special compound-unit class.

Time

  • Instant kept distinct from signed Duration;
  • add/subtract/negate duration;
  • instant ± duration;
  • instant difference;
  • exact seconds/minutes/hours only;
  • no calendar/timezone/DST semantics.

No Group/Semigroup inheritance hierarchy is added. The algebraic classification can remain knowledge available to later computer-science/AICI reasoning while ordinary source only sees the operations it needs.

Intervals

  • exact rational one-dimensional intervals;
  • closed/open/half-open endpoints;
  • empty interval handling for reversed bounds and open singleton bounds;
  • membership;
  • interval addition;
  • endpoint openness uses typed +epsilon / -epsilon boundary vocabulary;
  • nilpotent dual-number epsilon (epsilon^2 = 0) remains a separate type and is deliberately not ordered;
  • no fake inverse that "adds epsilon back" and silently recloses an endpoint.

Deliberately deferred: interval multiplication/division, outward floating rounding, correlated uncertainty (x-x dependency), probability/Gaussian inference, calendar time, and the broader open-ended uncertainty design.

Tests-first history

  • tests first: ae6bcfbf0e7ccae46f57a171be40b0c78fc73ab9
  • implementation: 57de2109ff81b4f4bf7f2610a63d34b5278b3804
  • real compiler harness: edric007, now included by ./edric test
  • harness permission correction only: current head a3ffc1c03e040e31a0867d473611b1bf8960cca0

Verification

VERIFIED on the exact current PR head in the pull-request merge context.

  • feature head: a3ffc1c03e040e31a0867d473611b1bf8960cca0
  • tested PR merge commit: 59ad1d9c83028ca1dbdb8ba50f486cdd7dca9425
  • workflow: Edric type-system smoke
  • run: 33277502908
  • job: 99166698046
  • full ./edric all bootstrap completed successfully
  • focused receipt: idris2/basic/edric007: success 00.854s
  • output comparison: 1/1 tests successful

The only correction made after the first semantic green run was making the edric007/run harness file executable; no mathematical/type semantics were weakened or changed.

Related: #28, #30, #31, #42.

@isomorphisms isomorphisms left a comment

Copy link
Copy Markdown
Owner Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Self-check boundary: this PR intentionally implements only the exact rational/unit, signed-duration/instant, and additive interval kernels. Do not broaden it to calendar semantics, probability distributions, general uncertainty, or algebraic interface inheritance merely to make the first slice feel complete. Compiler failures should be repaired minimally without weakening the pinned equations.

@isomorphisms isomorphisms left a comment

Copy link
Copy Markdown
Owner Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Cross-reference for later review: #28 owns dimensions/units, #30 owns intervals/uncertainty, #31 owns instants/durations/calendar separation, and #42 owns broader constraint inference. This PR is the common executable first slice, not a replacement for those design issues.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant