constraints

1 files changed, 403 insertions, 0 deletions

diff --git a/docs/constraints.org b/docs/constraints.org
new file mode 100644
index 0000000..9f866fa
--- /dev/null
+++ b/docs/constraints.org
@@ -0,0 +1,403 @@
+#+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"