feat(3vl): FPPC-amended three-valued logic (read-site nulls + null propagation + cod override)#73
Merged
Merged
Conversation
7bebc65 to
fd9ec74
Compare
4 tasks
fd9ec74 to
4bdf5a9
Compare
Implements the runtime half of the FPPC 3VL amendment (approved by M. Toro), distinguishing a missing value (null, lenient) from a genuine error (Failure, empties the path): - Read site (FPPC Ra): a missing property in AttrLookup and a missing key / null base in FieldAccess now read as Success(Value::Null) instead of Failure. A bound element's absent property is `ok null`, so the connectives and comparisons see a null value rather than an error. (attr_of_value already did this for comprehension elements; the main path now matches.) - Cast: `null AS T` -> null for any target; a failed cast of a *non-null* value stays a Failure (error). This is the runtime relaxation that lets null reach the 3VL logic through the implicit operand-cast wrapper, without turning real cast errors into null. - eval_binop: classic 3VL null propagation. Arithmetic and comparison operators yield null on any null operand; IN is 3VL (null argument or unmatched-with-a- null-in-the-list -> null); AND/OR use the SQL truth table with the absorbing element short-circuiting (false AND null = false, true OR null = true) and null otherwise. Genuine errors never reach here: the operand-cast wrapper propagates a Failure (which empties the path) before eval_binop runs. - Unary: NOT null -> null, -null -> null. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
The FPPC `cod` meta-function propagates bottom if either operand is bottom, which falsely prunes queries like `WHERE x.status OR true` as empty. Per the approved amendment, override it for the short-circuit connectives only: OR/AND degrade to bottom only when BOTH operands are incompatible with the expected type. A single bottom/null operand beside a valid Bool still types as Bool (`bottom OR B : B`) — a deliberate under-approximation so a dynamically-valid branch is not pruned. Non-short-circuit operators (arithmetic, comparisons) and NOT keep the default: any bottom operand degrades. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
4bdf5a9 to
87ff63f
Compare
End-to-end coverage of the amended semantics: OR/AND/NOT truth tables, read-site nulls (missing property/field -> null; the `WHERE x.status OR true` headline), comparison/equality 3VL (`null = null -> null`; `= null` drops rows while IS NULL matches), arithmetic null propagation, 3VL IN, `null AS T -> null`, and null field access. The error-vs-null distinction at a connective (a failed cast or a non-bool value beside a dominating boolean) is tagged PENDING(Matías) and pins the FPPC-faithful reading (error empties the path) as the default. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Document the residual-WHERE / general-expression 3VL (run_expr/eval_binop: null propagation, SQL truth tables, null AS T, type-error-empties), the FPPC Ra read-site rule (missing property -> null, not Failure), the cod override, and the known ISO gap (essential type errors / NOT-NULL sites should raise a hard data exception 22G12/22G03; froGQL empties per the FPPC model) as a future ISO data-exceptions workstream. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
87ff63f to
7691ed2
Compare
jeanpaulduchens
pushed a commit
that referenced
this pull request
Jul 6, 2026
…rción de operandos El merge de la 3VL (#73) rompía pushdown_null_test: el despacho de la rama temporal inlineó el cast de operandos pero omitió el caso 'null inhabits every type' que la 3VL agregó al brazo AS. Un operando null devolvía Failure en vez de fluir como Null a la lógica 3VL, de modo que 'x.a = 999 OR true' con x.a ausente tiraba la fila en vez de conservarla. Ahora la coerción inline trata null explícitamente, idéntico al brazo AS de main; los temporales conservan su bypass. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Supersedes #63 and the closed #27. Implements the FPPC 3VL amendment approved by M. Toro, on current
main(v0.2.7).The design (Matías's three rules + FPPC
Ra)codoverride (typechecker) — for the short-circuit connectivesOR/ANDonly, degrade to bottom only when both operands are bottom. A single bottom/null operand beside a valid Bool still types as Bool. Non-short-circuit ops (+, comparisons) andNOTkeep the strict default.null AS T → nullfor any target; any other failed cast is an error (not null).Plus FPPC rule
Ra: a missing property/field reads asok null, so the connectives see a null (lenient) while genuine errors stayFailure(which empties the path). This is the crux that #63 could not express: it kept missing reads asFailureand absorbed them at the connective, which also laundered real type errors into booleans.Why this is the right altitude (vs #63)
WHERE x.status OR truemust keep all rows, andWHERE ('a' AS INTEGER) OR truemust not. These need null ≠ error at the connective:WHERE x.status OR true(missing)null OR true)WHERE ('a' AS INTEGER) OR truenull = nullnull✅true(structural)Read-site nulls make missing-value lenient; errors stay errors. Comparison 3VL comes along necessarily (once
missing → null,= nullwould match unlessnull = null → null).Changes
src/runtime/engine.rs—AttrLookup/FieldAccessmissing →Null;null AS T → null;eval_binopnull-propagation for arithmetic/comparison, 3VLIN, SQL truth-tableAND/OR;NOT null/-null → null.AND/ORroute through the existing operand-cast wrapper, so a real error (non-bool / failed cast) propagates and empties the path — no dedicated short-circuit arms, no duplicated truth tables.src/typing/checker.rs— thecodoverride folded into the existing codomain check (ok1 || ok2forAND/OR,ok1 && ok2otherwise).tests/three_valued_logic_test.rs— 21 tests (below).One open decision — tagged
PENDING(Matías)At runtime, does a genuine error (failed cast / non-bool value) beside a dominating boolean empty the path or get absorbed? This PR pins the FPPC-faithful reading (empty), consistent with the paper's monadic
Rbopand Matías's "failed cast = error, not null". If he rules "absorb", three tagged tests flip and the fix is a localized wrapper change. Nothing else depends on it.Tests (21) & verification
Truth tables, read-site nulls, comparison 3VL (
= nulldrops /IS NULLmatches), arithmetic propagation, 3VLIN,null AS T, null field access, and thePENDING(Matías)error-empties cases.cargo fmt --allcargo clippy --workspace --all-targets -- -D clippy::allcargo testsweep (incl.bench_test) — no regressions;null_test,count_test,dm_set_test,record_testall green (read-site nulls don't disturb aggregates/DM/= null)🤖 Generated with Claude Code