Skip to content
docs
Arxo ↗

LDC-E2403 — A function whose purity is not proved

For LLMs5 sections

What it means

Section titled “What it means”

A plain function may lower only when its complete local call graph proves it free of effects: no snapshot reads, no judgment relations, no opaque or unknown calls, no recursion without a termination certificate. An explicit purity claim raises the same bar and adds the author’s word to it. When any dependency lacks an effect descriptor — an imported name the unit cannot see into, for example — purity is unproved and the compiler refuses the function at its name.

The fix proves purity or drops the claim: compute from data alone with local pure calls, or declare the heavier effect through the channel the language provides for it. A body of plain arithmetic over its parameters lowers without a word.

Example

Section titled “Example”
Arxo Law
language "law.core" version "0.2";
package demo.diagnostics version "0.1.0";
namespace "urn:law:demo:diagnostics";


pure function Unproved(x: Integer) -> Integer = foreign.pkg::rate(x);

Fix

Section titled “Fix”
Arxo Law
language "law.core" version "0.2";
package demo.diagnostics version "0.1.0";
namespace "urn:law:demo:diagnostics";


function Increment(x: Integer) -> Integer = x + 1;

Engine message

Section titled “Engine message”

The engine reports this in its own wording:

Output
example.law:5:15: error LDC-E2403: COMPUTABILITY_NOT_PROVED (LDC-E2403): pure function "Unproved" is not proven PURE_DETERMINISTIC: call "foreign::pkg::rate" has no available effect descriptor (imported/unknown dependency) (§46/§47.5)
Section titled “Related”

Documentation for Arxo. Writings — blog.arxo.io.

Anonymous visit counts on stats.arxo.io, no cookies.