# 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.

## Incorrect form and why it stays silent

```text title="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

```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` |

```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;
    
}
```

```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;
    
}
```

```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.