#+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 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"