Units and explicit conversion

Intention

I want to bring lengths to one unit before adding them.

Conversion between units is explicit: the scenes compare adding a metre to a kilometre before and after an explicit conversion.

Correct formFrozen execution sceneBoundary

Incorrect form and why it stays silent

Incorrect form

magnitude(1 m) + magnitude(1 km)

pure function Metres(x: Magnitude) -> Magnitude = unit_convert(x, "m");

Dimension and unit are checked at evaluation: the incorrect expression below yields RUNTIME_ERROR. A separate mutation shows an implementation defect: unit_convert inside a pure function is rejected with LDC-E2403, although conversion is defined as deterministic.

Correct form

Arxo Law

language "law.core" version "0.2";
package recipes.l.r05 version "0.1.0";
namespace "urn:recipe:l-calc:05";

unit m dimension Length scale 1 / 1;
unit km dimension Length scale 1000 / 1;
unit s dimension Time scale 1 / 1;
relation total(x: Magnitude);
rule Sum strict { when true; then total(magnitude(1 m) + unit_convert(magnitude(1 km), "m")); }

Frozen execution scene

Facts and choice	Question	Answer
1. metre plus kilometre after conversion	if scalar_of((magnitude(1 m) + unit_convert(magnitude(1 km), "m")) / magnitude(1 m)) == 1001 / 1 then true else false	true / COMPUTED
2. metre share of a kilometre	if scalar_of(unit_convert(magnitude(1 km), "m") / magnitude(1 m)) == 1000 / 1 then true else false	true / COMPUTED
3. different units without conversion	magnitude(1 m) + magnitude(1 km)	no value / RUNTIME_ERROR

metre plus kilometre after conversion

Arxo Law

test "metre plus kilometre after conversion" {
    given {
        context {
            legal_time @2026-09-13;
            decision_time @2026-09-13T09:00:00+05:00;
            knowledge_time @2026-09-13T09:00:00+05:00;
            timezone "Asia/Almaty";
        }

    }
    evaluate if scalar_of((magnitude(1 m) + unit_convert(magnitude(1 km), "m")) / magnitude(1 m)) == 1001 / 1 then true else false;
    expect value == true;
    expect evaluation_status == COMPUTED;

}

metre share of kilometre

Arxo Law

test "metre share of kilometre" {
    given {
        context {
            legal_time @2026-09-13;
            decision_time @2026-09-13T09:00:00+05:00;
            knowledge_time @2026-09-13T09:00:00+05:00;
            timezone "Asia/Almaty";
        }

    }
    evaluate if scalar_of(unit_convert(magnitude(1 km), "m") / magnitude(1 m)) == 1000 / 1 then true else false;
    expect value == true;
    expect evaluation_status == COMPUTED;

}

mixed units without conversion

Arxo Law

test "mixed units without conversion" {
    given {
        context {
            legal_time @2026-09-13;
            decision_time @2026-09-13T09:00:00+05:00;
            knowledge_time @2026-09-13T09:00:00+05:00;
            timezone "Asia/Almaty";
        }

    }
    evaluate magnitude(1 m) + magnitude(1 km);

    expect evaluation_status == RUNTIME_ERROR;
    expect issue(UNIT_MISMATCH);
}

Counterfactual

Mutation: relation total(x: Magnitude); → pure function Metres(x: Magnitude) -> Magnitude = unit_convert(x, "m"); relation total(x: Magnitude);; expected LDC-E2403. Additional counterfactuals are shown as separate table rows.

A separate witness checks the absence of the required static rejection for a conversion known to be wrong at compile time. The executable rejection is already pinned by the last scene above; a passing static check does not prove this form correct.

Python

>>> import runpy
>>> checks = runpy.run_path("docs/recipes/l-calc/resources/check.py")
>>> checks["check_static_units"](https://github.com/arxohq/law/blob/master/docs/recipes/l-calc/5)
'ДЕФЕКТ lawc: статически известная ошибка единиц проходит check'

Boundary

Magnitude and Quantity are different kinds. A quantity tagged year does not add a calendar year to a date: deadlines belong to book E. The SI bases and scales used here are declared locally. A statically known wrong conversion or operation passes the static check but is rejected at evaluation. A unit_convert call inside a pure function is rejected (LDC-E2403); the formula stays pure and conversion is moved into the query.

Pitfall

Adding a metre to a kilometre without conversion is a unit mismatch, not an implicit conversion.