CEP-0029: Predicate Fact Algebra¶

Draft

Draft proposal for negative facts, richer predicate logic, runtime value narrowing, and meta-constraints over constraint Type values. V1 predicates carry only accepted positive facts.

Summary¶

Catalyst should eventually decide how far predicate facts can go beyond V1's positive fact model.

V1 Type.Predicate values can carry facts for successful checks such as implementation, structural satisfaction, type-kind classification, and dyn-safety. V1 sema does not use negative facts.

Example¶

Possible future shape:

if T.satisfies(mutable_fields(.x)) {
  value.x = 1
} else {
  @diagnostic.note("`T` has no mutable `x` field")
}

Today the true branch may carry positive facts. This proposal asks whether false branches, runtime value narrowing, and implication checks should also become semantic facts.

Motivation¶

Richer predicate logic could improve conditional declarations, diagnostics, generic constraints, narrowing, and reflection. It also risks creating a complex proof language.

Proposed Direction¶

The proposal should cover:

negative facts and false-branch facts;
richer boolean fact algebra;
runtime value narrowing;
meta-constraints over constraint Type values;
checking whether one structural constraint implies another;
diagnostics for contradictory or unreachable facts.

V1 Compatibility¶

V1 producers normally leave facts_when_false empty, and V1 sema does not rely on negative facts. Constraint implication checking remains deferred.