path: root/docs/constraints.org

#+TITLE: Constraints and Membership Criteria

* Conceptual Foundation

A relation's *intension* is its meaning: what the relation represents
in the conceptual model. Where the extension is the set of tuples
currently admitted, the intension declares which tuples /could/ be
admitted. Constraints are the formal mechanism by which a relation's
intension narrows the infinite space of possible tuples to only those
consistent with the conceptual model.

Because Sakura models everything as a relation, constraints are
themselves relations. Checking a constraint is checking membership in
a constraint-relation. When a DML operation (insert/delete)
manipulates a relation, it verifies that the manipulated data
satisfies membership in all attached constraint-relations before
committing the change.

** Membership Criteria vs. Constraints

Sakura distinguishes two levels of admission control:

- *Membership criteria* (=membership_criteria : Tuple.t -> bool=) is
  the opaque predicate baked into every relation. For stored relations
  it validates schema/domain conformance. For ephemeral relations
  (less_than, plus, etc.) it /is/ the intensional definition --- the
  rule that characterizes the relation rather than an enumeration of
  members.

- *Constraints* (=Constraint.t=) are declarative, inspectable
  structures attached to a relation via its =constraints= field. They
  are evaluated at DML time against the current database snapshot and
  produce structured diagnostics on failure.

Membership criteria are checked first. If the tuple passes, the
constraint list is evaluated.

** Negation and Closed-World Reasoning

The =Not= constructor requires an explicit universe relation name.
This forces closed-world reasoning: negation is only meaningful
relative to a known domain. Without a declared universe, =NOT P=
would vacuously hold for anything outside the domain of discourse.

At runtime the universe annotation is declarative --- it is not
checked as a tuple-existence predicate, because the tuple being
validated has not been stored yet. The evaluator simply negates the
body and treats any =MembershipFailed= diagnostic from the body as
successful negation.

** Cardinality Awareness

Constraints can narrow cardinality. A =Forall= over a finite
quantifier relation, or a range restriction via comparison relations,
constrains an otherwise infinite domain to a finite subset. The
=ConstrainedFinite= variant of =Conventions.Cardinality.t= tags
relations known to be finite due to constraints but whose exact count
is not computed.

* Constraint Language

The constraint language is a small first-order logic over relation
membership:

#+begin_src ocaml
type t =
  | MemberOf of { target : relation_name; binding : binding }
  | Not of { body : t; universe : relation_name }
  | And of t list
  | Or of t list
  | Exists of { variable : attr_name; quantifier : relation_name; body : t }
  | Forall of { variable : attr_name; quantifier : relation_name; body : t }
#+end_src

** MemberOf

The atomic constraint. It checks whether the tuple, after binding
resolution, is a member of the target relation.

#+begin_src ocaml
MemberOf { target = "orders"; binding = BindingMap.singleton "order_id" (Var "order_id") }
#+end_src

This says: "the value of =order_id= in the current tuple must appear
as =order_id= in some tuple of the =orders= relation." This is a
foreign key constraint.

Everything is a relation --- domains, comparison relations, user
relations. =MemberOf= resolves them uniformly from the database.

** Bindings

Bindings map target attribute names to expressions:

#+begin_src ocaml
type binding_expr =
  | Var of attr_name          (* resolve from current tuple *)
  | Const of AbstractValue.t  (* literal value *)
#+end_src

A binding like ={ "left" -> Var "age"; "right" -> Const 18 }= applied
to a tuple with =age=25= produces the pairs
=[("left", 25); ("right", 18)]=, which are then checked for
membership in the target relation (e.g., =greater_than_or_equal=).

** Logical Connectives

- =And cs=: All sub-constraints must hold. Short-circuits on first failure.
- =Or cs=: At least one must hold. Short-circuits on first success.
- =Not { body; universe }=: The body must /not/ hold. The universe
  declares the domain of negation for logical soundness.

** Quantifiers

- =Exists { variable; quantifier; body }=: There exists a tuple in
  the quantifier relation such that, when bound to =variable=, the
  body holds. The quantifier must be a finite relation.
- =Forall { variable; quantifier; body }=: For all tuples in the
  quantifier relation, the body holds. Also requires finiteness.

Quantifiers bind values from the quantifier relation into the tuple's
attribute map, extending the scope for the body evaluation.

* Comparison Shorthands

Because comparisons are relations, comparison constraints are
=MemberOf= with the appropriate relation name and binding. Shorthand
constructors eliminate boilerplate:

#+begin_src ocaml
Constraint.lt  ~left:(Var "age") ~right:(Const (Obj.repr 65))
(* equivalent to:
   MemberOf { target = "less_than";
              binding = { "left" -> Var "age"; "right" -> Const 65 } } *)

Constraint.between ~value:(Var "score") ~low:(Const 0) ~high:(Const 100)
(* And [ gte score 0; lte score 100 ] *)
#+end_src

Available shorthands: =lt=, =lte=, =gt=, =gte=, =eq=, =neq=, =between=.

* Comparison and Arithmetic Relations

The prelude registers domain-parameterized comparison relations. Each
takes a domain's =compare= function and a predicate over the compare
result:

| Relation name         | Schema         | Predicate       |
|-----------------------+----------------+-----------------|
| =less_than=           | (left, right)  | =compare < 0=   |
| =less_than_or_equal=  | (left, right)  | =compare <= 0=  |
| =greater_than=        | (left, right)  | =compare > 0=   |
| =greater_than_or_equal= | (left, right) | =compare >= 0= |
| =equal=               | (left, right)  | =compare = 0=   |
| =not_equal=           | (left, right)  | =compare <> 0=  |

Arithmetic relations follow the same pattern with richer schemas:

| Relation     | Schema                          | Invariant             |
|--------------+---------------------------------+-----------------------|
| =plus=       | (a, b, sum)                     | =a + b = sum=         |
| =times=      | (a, b, product)                 | =a * b = product=     |
| =minus=      | (a, b, difference)              | =a - b = difference=  |
| =divide=     | (a, b, quotient, remainder)     | =a = b*q + r, 0<=r<b= |

All are ephemeral (generator-based, infinite). They serve as the
vocabulary for constraint expressions.

* Domain Compare

Each =Domain.t= now carries a =compare= field:

#+begin_src ocaml
type t = {
  name : Name.t;
  generator : Generator.t;
  membership_criteria : Tuple.t -> bool;
  cardinality : Cardinality.t;
  compare : AbstractValue.t -> AbstractValue.t -> int;
}
#+end_src

The =compare= function dispatches comparison for values of that
domain. The comparison relations use domain comparators rather than
spreading =Obj.magic= casts at each call site. The four prelude
domains define their comparators:

- =integer=, =natural=: integer comparison
- =rational=: float comparison
- =string=: lexicographic comparison

* Evaluation Engine

** Eval Context

The evaluator cannot depend on =Relation.t=, =Database.t=, or
=Manipulation= (they compile later). Instead it receives a callback
record:

#+begin_src ocaml
type eval_context = {
  check_membership :
    relation_name ->
    (attr_name * AbstractValue.t) list ->
    bool;
  iterate_finite :
    relation_name ->
    (attr_name * AbstractValue.t) list list option;
}
#+end_src

Both callbacks are closed over a specific =(storage, db)= pair at
construction time. The =db= is a =Management.Database.t= representing
one exact version (one hash). All relation lookups resolve against
that snapshot only. This is critical: constraint evaluation sees a
consistent view of the database, never a partially-mutated state.

** How =check_membership= Works

For a stored relation, =check_membership= loads every tuple from the
Merkle tree and checks whether any tuple's attributes match the bound
pairs. For an ephemeral relation (no tree), it delegates to
=membership_criteria=.

This distinction matters for foreign key constraints. A FK like
"order_items.order_id must exist in orders" requires checking actual
tuple existence in the =orders= relation, not just schema
conformance.

** Evaluation Rules

| Constructor | Rule                                                        |
|-------------+-------------------------------------------------------------|
| =MemberOf=  | Bind variables from tuple, call =check_membership=          |
| =Not=       | Negate body. =MembershipFailed= from body counts as success |
| =And=       | All must hold (short-circuit on first failure)              |
| =Or=        | Any must hold (short-circuit on first success)              |
| =Exists=    | Iterate quantifier, bind each row, true if any body holds   |
| =Forall=    | Iterate quantifier, bind each row, true only if all hold    |

Quantifiers require finite quantifier relations (=iterate_finite=
returns =Some rows=). An infinite quantifier produces
=UnboundedQuantifier= diagnostic.

** Diagnostics

Failures produce structured diagnostics rather than opaque booleans:

#+begin_src ocaml
type diagnostic =
  | MembershipFailed of { target : string; bound_values : ... }
  | RelationNotFound of string
  | UnboundedQuantifier of { variable; quantifier }
  | ConstraintFailures of (string * diagnostic) list
#+end_src

Named constraint evaluation collects all failures into
=ConstraintFailures=, giving the caller a complete picture of which
constraints were violated and why.

* Enforcement in Manipulation

Constraints are enforced in =Manipulation.create_tuple=. The sequence is:

1. Check =membership_criteria= (schema/domain validation)
2. If the relation has constraints, build an =eval_context= from the
   current =(storage, db)= pair
3. Evaluate each named constraint against the tuple
4. On any failure, return =ConstraintViolation= with diagnostic details
5. On success, proceed to hash, store, and persist

The =eval_context= is built fresh for each =create_tuple= call with
the /current/ database state. This ensures FK lookups see recently
inserted tuples, not a stale snapshot from constraint registration
time.

** Registering Constraints

=register_constraint= performs two actions:

1. Attaches the constraint body to the relation via
   =update_relation_constraints=, which merges new constraints with
   any existing ones
2. Records the constraint name and relation in the =sakura:constraint=
   catalog relation

The constraint body is stored in the =Relation.t= object's
=constraints= field, not separately. This means the constraint
travels with the relation through algebraic operations.

* Propagation Through Algebra

When algebraic operations derive new relations, constraints propagate
according to rules that preserve soundness:

| Operation | Propagation rule                                    |
|-----------+-----------------------------------------------------|
| Select    | Preserve all source constraints                     |
| Project   | Filter: keep only constraints whose variables are   |
|           | all within the projected attributes                 |
| Rename    | Apply variable renaming to constraint references    |
| Equijoin  | Merge constraints from both input relations         |
| Union     | Drop all constraints (conservative: constraints     |
|           | only hold if both inputs agree)                     |
| Diff      | Preserve left relation's constraints                |
| Take      | Preserve source constraints                         |

The =filter_by_attrs=, =rename_vars=, and =merge= utility functions
on =Constraint.t= implement these transformations.

** Example: Project Filtering

Given a relation =R(x, y)= with constraint "=x < 100=", projecting
to =[y]= drops the constraint because =x= is no longer in scope.
Projecting to =[x]= or =[x, y]= preserves it.

#+begin_src ocaml
Constraint.filter_by_attrs ["y"] (Constraint.lt ~left:(Var "x") ~right:(Const 100))
(* => None — dropped because "x" not in ["y"] *)

Constraint.filter_by_attrs ["x"] (Constraint.lt ~left:(Var "x") ~right:(Const 100))
(* => Some (lt ...) — preserved *)
#+end_src

* Utility Functions

=Constraint.t= provides introspection and transformation utilities:

- =vars_in : t -> attr_name list= --- collect all =Var= names
  referenced in a constraint, recursively through all sub-expressions.

- =rename_vars : (attr_name * attr_name) list -> t -> t= --- rename
  variable references throughout a constraint tree. Used by the rename
  algebra operator.

- =filter_by_attrs : attr_name list -> t -> t option= --- returns
  =None= if the constraint references any variable not in the given
  set. Used by projection to drop inapplicable constraints. For =Or=,
  all branches must survive (dropping a branch changes semantics).

- =merge : (string * t) list -> (string * t) list -> (string * t) list=
  --- AND-merge two named constraint lists. Constraints sharing a name
  are combined with =And=. Used by equijoin.

* Examples

** Foreign Key

#+begin_src ocaml
(* order_items.order_id must reference an existing order *)
let fk =
  Constraint.MemberOf {
    target = "orders";
    binding = Constraint.BindingMap.singleton "order_id" (Var "order_id")
  }
in
register_constraint storage db
  ~constraint_name:"fk_order"
  ~relation_name:"order_items"
  ~body:fk
#+end_src

Inserting an order_item with =order_id=999= when no such order exists
produces =ConstraintViolation "constraint fk_order violated"=.

** Mutual Exclusion

#+begin_src ocaml
(* A ticket cannot be both open and closed *)
let not_closed =
  Constraint.Not {
    body = Constraint.MemberOf {
      target = "closed_ticket";
      binding = Constraint.BindingMap.singleton "ticket_id" (Var "ticket_id")
    };
    universe = "open_ticket"
  }
in
register_constraint storage db
  ~constraint_name:"not_closed"
  ~relation_name:"open_ticket"
  ~body:not_closed
#+end_src

** Self-Reference Inequality

#+begin_src ocaml
(* An employee cannot manage themselves *)
let neq = Constraint.neq ~left:(Var "emp_id") ~right:(Var "mgr_id") in
register_constraint storage db
  ~constraint_name:"no_self_manage"
  ~relation_name:"reports_to"
  ~body:neq
#+end_src

This uses the =not_equal= comparison relation: it checks membership
in ={(left, right) | left <> right}=.

* References

- Codd, E. F. (1979), "Extending the Database Relational Model to Capture More Meaning"
- Date, C. J. and Darwen, H. (2006), "The Third Manifesto"
- McGoveran, D. (1994), "The Semantic Relational Data Model"