RFC-037: Type Checking of Laws

Context

Every parameter, input, output and definition in a law declares a type (string, number, boolean, amount, date, array, object) and may carry a type_spec with a unit, a precision and bounds. Until now those declarations were documentation. just validate checked the shape of the YAML against the JSON schema and nothing else; the engine is dynamically typed and looks at the value it receives, never at the declaration; min and max have been “parsed metadata, not yet enforced” since they were added.

RFC-036 made the cost visible. It introduced a run-time distinction between an absent value (null) and an unknown one, and a rule that calculating with an absence is an error. That error is correct, and it arrives too late: a register delivers null for a field the law never expected to be absent, the value travels through two cross-law calls, and article 3 of a correct law is told to add an absence test. Review of that RFC put the finger on it: whether a value may be absent belongs in the type, where the validator can see it, not in the data, where only the engine sees it.

Adding one flag does not need a type checker. Enforcing it does: to refuse EQUALS $huur null on a field that is not nullable, the validator has to know what $huur refers to and what its declaration says. Once that environment exists, the rest of the declarations can be checked at the same cost.

Decision

The engine gets a static type checker over the expressions of a law. It runs in two places with one implementation (packages/engine/src/typecheck.rs): in the validate binary after the schema check, so just validate and the pre-commit hook enforce it on every law in the corpus, and in LawExecutionService::load_law, so a law that fails the check cannot be loaded, by the editor’s WASM engine or anyone else. A finding names the law, the article, the output or action, and the rule.

Environment. For each article the checker knows the declared type and nullability of every parameter, input and output, the type of every definition from its literal, and that $referencedate is a non-nullable date. Property paths into objects ($record.field) and FOREACH bindings have no known type. The checker never reports on what it does not know: a false positive on a correct law is a bug in the checker. It also understands the engine aliases NOT_EQUALS, IS_NULL, NOT_NULL and NOT_IN, which the schema does not admit; just validate refuses those before the checker runs, so they only reach it through the loader.

Rules for absence (the rules of RFC-036, run here):

• N1 A comparison with the literal null needs a nullable field on the other side. EQUALS $huur null on a non-nullable huur cannot be true and is rejected. On a nullable field that the enclosing condition already established present the test is redundant, and the message says so.
• N2 The literal null appears only as the value of a nullable output, directly or as a branch of an IF that is that output’s value, or as an element of a LIST, of the values of IN, or the body of a FOREACH without combine (an array of absences is a value, and IN $x [null, 1] is a membership test for absence). As an operand, or as the value of a non-nullable output, it is rejected.
• N3 An IF without default yields null when no case matches. That is allowed only as the value of a nullable output; nested inside an operation, or as the value of a non-nullable output, it is rejected.
• N4 A nullable variable enters arithmetic, an ordering, AND, OR, NOT, an IF condition or a date operation, or is assigned to a non-nullable output (directly, value: $x, or as a branch of the output’s IF), only on a path where it is known to be non-null. The subject of IN is exempt (membership of an absence is structural under RFC-036 and cannot fail), and so is a FOREACH collection (a null collection iterates nothing). A path establishes presence in the then of NOT(EQUALS $x null), in the cases after EQUALS $x null and in the default, in the conditions of an AND after NOT(EQUALS $x null) (of an OR after EQUALS $x null), in the body of a FOREACH whose filter tested it, and through a boolean output that is itself such a test: an earlier action heeft_x = NOT(EQUALS $x null) makes when: $heeft_x (and NOT $heeft_x, and $heeft_x inside an AND) carry the fact, which is the corpus idiom (heeft_partner). A guard on a field, NOT(EQUALS $rec.a null), establishes the record $rec too: a field of no record is no record. Elsewhere the variable is rejected. Passing it on to another law, into EQUALS, or to a nullable output is fine. The checker does not express correlated presence beyond this (inputs keyed on $partner_bsn being present exactly when partner_bsn is); a law states that with a guard on the field it calculates with, or with the heeft_x idiom.
• N5 An input that takes a nullable output from another law and is not nullable itself is rejected, when that law is available to the checker. So is an input whose cross-law call passes a nullable variable for a required parameter the target does not declare nullable: the call is then skipped and the input is null (RFC-036). A property path $rec.bsn as argument counts with its record’s nullability; whether the field itself may be null on a present record is not known. And an article that implements a required open term without a default may not declare its output for the term nullable: the engine takes that output as the term’s value, and the delegating law reads the term as never absent.

Load order. The set of loaded laws is well-typed whatever order the laws arrive in. load_law checks the new law against the laws already loaded, and then checks again every loaded law that references the new one (an input with source.regulation, an implements of one of its terms), with the new law in view. A finding there refuses the new law and names the consumer (“loading B makes A ill-typed: A’s input x takes B.y, which may be null”). The demo and the editor therefore cannot end up with a set that one load order accepts and another refuses. What a well-typed set can no longer reach at run time (a skipped call or a null output into a non-nullable input) stays in the engine as defence in depth, with direct tests.

Rules for types:

• T1 Arithmetic and ordering take number or amount operands; ADD also joins two strings or two arrays (RFC-007), ordering also compares two dates (RFC-021).
• T2 AND, OR, NOT and an IF condition take boolean operands.
• T3 EQUALS between two known, different types is rejected; number against amount is allowed, and date against string, because dates arrive as ISO strings.
• T4 A literal assigned to an output must have the output’s type.

Each rule applies only where the operand types are known. Rules that fire on a correct law in corpus/regulation or corpus/demo are narrowed until they do not; the integration test that runs the checker over both corpora and expects zero findings is what keeps the corpus typed from here on.

Why

• The error lands where the mistake is. An author who forgets that a register may deliver “none” hears it from just validate while writing the law, with the field named, instead of from a run-time error in another law.
• Declarations become contracts. A binding that says a register may deliver null (absent: null in the demo’s bindings.yaml) and a law that says the field is never absent now contradict each other visibly, and a test can say so.
• The pipeline gets a gate. Laws written by the enrichment pipeline are checked by the same rules as laws written by hand; a generated EQUALS … null on a field nobody declared nullable does not reach the corpus.
• min, max and units are next. The environment the checker builds is what those need too; they are out of scope here and named as the next candidates.

Tradeoffs

• A checker is code that can be wrong. A too-eager rule rejects a correct law. The mitigation is the zero-findings integration test over the corpus and the discipline that a rule is narrowed, never that a law is bent to it.
• Two type systems. The checker reasons about declarations; the engine reasons about values. They agree by construction on what is checked, and the run-time rules of RFC-036 stay as the net for what the checker cannot see (an empty collection’s MAX, a property inside an object, a null handed in by a caller under an input’s name).
• The corpus has to declare. Every field a law tests for null gains a nullable: true. That is an honest annotation, not a change in logic, and it was done in the same change.

Open point: a dedicated fallback operation

An IF_ABSENT operation (subject: $x, value: <fallback>, typed as nullable T to T) would give the checker one place where a nullable value becomes a value, and would read like the legal phrase “bij gebreke van”. RFC-004 adds an operation when a real law needs it. The laws in both corpora test absence as a boolean (“heeft partner”, “is beëindigd”) and rarely fall back to a value, so the flow rule N4 over the existing IF and EQUALS … null covers them. The operation is added the day a legal text says “bij gebreke van X geldt Y”, not before.

Alternatives Considered

• Only the flag, enforced at run time. The engine could refuse null for a non-nullable input when it resolves it, and nothing more. That catches the data error at the boundary but leaves EQUALS $huur null on a non-nullable field as a comparison that is always false, silently. The validator has to read the expression.
• Nullable types instead of a flag (type: number? or a union with null). Equivalent in power; the flag keeps the type enum and the type_spec machinery untouched and is one line in the schema.
• A separate lint tool. Would drift from the engine’s own understanding of the language. One implementation in the engine crate, called from the validator and the loader, cannot.

Consequences

• Engine: packages/engine/src/typecheck.rs; called from bin/validate.rs and from load_law, which also re-checks the loaded laws that reference the new one; NullForNonNullable and NullOutput errors at run time (RFC-036).
• Schema: nullable on baseField in v0.5.8 (see RFC-036).
• Corpus: nullable declarations added where laws test for null; the integration test keeps both corpora at zero findings.
• Editor: the scenario editor offers a null cell only for nullable columns; type-check errors from loadLaw are shown to the author.
• Next: min/max (issue #444) and unit consistency (RFC-023) as rules of the same checker.

References

• RFC-036: absent and unknown values; the flag this checker enforces
• RFC-023: units, the next candidate for the checker
• RFC-004: the operation syntax the checker walks
• packages/engine/src/typecheck.rs