docs

2 files changed, 126 insertions, 42 deletions

diff --git a/docs/evaluators.org b/docs/evaluators.org
index 1e0d7cc..84bc493 100644
--- a/docs/evaluators.org
+++ b/docs/evaluators.org
@@ -24,55 +24,83 @@ indexes them so a client can ask which evaluators declare =dml= and
 get back B and C.
 
 * Protocols
-Three object components, following the existing =implementation= /
-=make= / =from= pattern.
-
-=Protocols.Evaluator= admits programs in string format. Admission
-validates a program in the evaluator's own representation (as in:
-parses, type checks and does all it requires to validate it) and
-yields a handle.
+An evaluator is an object like any other, that can be used to execute
+program with a context, exactly as an interpreter takes an expression
+and an environment. The plan tree should already bear every value the
+program needs, so there is nothing left to bind. Each invocation
+carries independent state based atop of a database view of the world
+(being therefore hash dependent and isolated).
 
 #+begin_src ocaml
+module Make (P : PROGRAM) : sig
   class type implementation = object
-    method capabilities : string BatSet.t
-    method admit : string -> (Handle.t, condition) result
+    method invoke :
+      program:P.t -> Context.t -> (Handle.t, condition) result
   end
+end
 #+end_src
 
-=Protocols.Program= exposes entry points and an invocation, making a
-program reusable, since each invocation carries independent state
-based atop of a database view of the world (hash dependent and
-isolated).
+The protocol is parameterized by the evaluator's own plan type, so a
+plan is never encoded into values only to be decoded again. Each
+application of the functor yields its own protocol constructor, which
+is what keeps one evaluator from answering another's programs: a
+client obtains the interface through the module of the evaluator it
+intends to speak to. The FOL evaluator, which lives under
+=lib/evaluators= alongside the evaluators shipped with RNT, currently
+understands a single node:
 
 #+begin_src ocaml
-class type implementation = object
-  method entry_points : string list
-  method invoke :
-    entry:string -> bindings:Concepts.Tuple.t -> Runtime.Context.t ->
-    (Handle.t, condition) result
-end
+type plan = Base of string
 #+end_src
 
+=Base= names a relation, which is resolved through the context and
+enumerated to exhaustion. The name is resolved rather than an address
+being followed, which keeps the evaluator free of storage and makes
+every resolution happen under one snapshot.
+
 The returned handle carries a result protocol with =Protocols.Cursor=,
-giving it incremental consumption. A successor state and a command
-completion are further result protocols, added for DML and DDL
-later. It's important to notice that the kernel enumerates result
-protocols; it thererfore does not enumerate sublanguages. That is not
-to say however that we cannot have a builtin catalog relation
-installed and configured by the client that enumerates them (that's a
-concern for the future).
+giving it incremental consumption. Since executing a plan node yields
+a cursor, operators stack as cursors over cursors, in the manner of a
+volcano iterator, and no intermediate result is materialized. A
+successor state and a command completion are further result protocols,
+added for DML and DDL later. It's important to notice that the kernel
+enumerates result protocols; it thererfore does not enumerate
+sublanguages. That is not to say however that we cannot have a builtin
+catalog relation installed and configured by the client that
+enumerates them (that's a concern for the future).
 
 * Context
-=Runtime.Context.t= supplies the selected database state, handles
-(which assume authorization, since we are a capability based system),
-cancellation, and resource usage. Evaluators reach kernel resources
-*only* through it.
-
-A nested invocation shares state, transaction, cancellation, and
-budget, and may be given less authority than its caller. Reads keep
-the selected state so that nesting does not need to resolve a branch
-tip again, and a successful evaluation and cursor exhaustion never
-commit. Commit should be an explicit host operation.
+=Protocols.Context.t= supplies the selected database state, the root
+handle through which names are resolved (which assumes authorization,
+since we are a capability based system), and the status of the
+evaluation. Evaluators reach kernel resources *only* through it.
+
+#+begin_src ocaml
+type t =
+  { snapshot : Concepts.Hash.hash
+  ; root : Handle.t
+  ; status : unit -> [`Live | `Cancelled | `Exhausted] }
+#+end_src
+
+The snapshot is the hash of a commit. Since every object is content
+addressed and prolly trees do not depend on insertion order, equal
+state yields an equal hash, so a commit hash is a frozen world rather
+than a pointer into a changing one. A cursor therefore pins a hash
+instead of an open transaction, and every node of a plan reads the
+same state, which gives repeatable reads across a whole plan for free
+and makes concurrent commits simply invisible to a running
+evaluation.
+
+=status= collapses cancellation and resource exhaustion into the
+single question an operator asks between tuples, namely whether it may
+produce another tuple. The runtime owns how =Exhausted= is decided. A
+nested invocation shares the snapshot, so nesting does not need to
+resolve a branch tip again, and a successful evaluation and cursor
+exhaustion never commit. Commit should be an explicit host operation.
+
+Budgets, authority narrowing, and resource accounting are not
+implemented, and adding a fourth status case would break exhaustive
+matches in consumers, which is the price of keeping this closed.
 
 * Composition
 Evaluators compose through invocation and result protocols alone. A
diff --git a/docs/object-taxonomy.org b/docs/object-taxonomy.org
index 02636b0..d948845 100644
--- a/docs/object-taxonomy.org
+++ b/docs/object-taxonomy.org
@@ -42,12 +42,24 @@ semantics of its multigroup.
 Schematics therefore describes more than the shape of a relation,
 recording the information necessary to understand the logical
 conditions under which a relation value is a semantically consistent
-representation of its intended group. Its schema component is exposed
-through =Protocols.Schematics.Make(Schema)=, instantiated by the host
-with a logical schema implementation satisfying
-=Abstract.Schematics.SCHEMA=. Providers and consumers use the shared
-protocol module to obtain a schema and list its attributes through an
-object handle.
+representation of its intended group.
+
+Schematics being a protocol forces an object to know its own type
+through =describe=, which yields a description of a multigroup, of a
+relation, or of a tuple (for now only these). There is no separate
+notion of a heading: the type of a relation is the schematics object
+it points to, and a tuple drawn from that relation is described
+against the very same type. A tuple description then, carries both the
+description of the relation it belongs to and the domains its own
+attributes exhibit, and therefore comparing the two is the admission
+test (membership criteria).
+
+#+begin_src ocaml
+type description =
+  | Multigroup of multigroup_description
+  | Relation of relation_description
+  | Tuple of tuple_description
+#+end_src
 
 For now, types are only opaque tags carried by attributes, and schema
 operations preserve this metadata without trying to resolve these
@@ -176,11 +188,55 @@ membership, enumerate members, establish the cardinality of a
 particular invocation, and guarantee termination of an expression
 consuming the relation.
 
+The line that matters (operationally) is not countable vs uncountable
+sets, but whether the extension can be enumerated to exhaustion. A
+relation whose extension is uncountable cannot be enumerated at all,
+so it is excluded by construction rather than by a check: such a
+relation is given intensionally, by its membership criteria, and
+offers membership testing without carrying enumeration. A countably
+infinite relation may be enumerated, but never exhausted, so an
+expression that must materialize it is the thing to reject. Membership
+is in any case always intensional! One does not ask whether a value is
+extensionally among the naturals (for that is very wasteful and
+naïve), only whether it satisfies the criteria for being one, and the
+extensional lookup a substantial relation can afford is an
+optimization that is valid only because admission already enforced
+those criteria (which will obviously include constraints).
+
 Sol, as RNT's total relational language, admits procedural relations
 only where the required evaluation properties can be established. An
 unrestricted procedure must not silently introduce partiality or
 nontermination into an otherwise total relational expression.
 
+* Tuple
+A tuple is a value of a relation rather than an object of the
+administrative tree. It is not registered with the object manager and
+holds no name of its own, since it is reached through the relation
+that asserts it. It remains an object at runtime, carrying Schematics
+so that it can describe the type it claims.
+
+A tuple is a type label together with its attributes. The label names
+the relation whose criteria the tuple claims to satisfy, which is what
+allows a tuple to be handed to a multigroup and routed to the relation
+representing its type, instead of being inserted into a relation
+chosen by the caller. Admission is then a matter of typing and
+constraints: the multigroup resolves the label, compares the tuple
+against the relation's schematics, and applies its predicate and local
+constraints before the tuple becomes asserted.
+
+The label is redundant while a tuple sits inside a relation, since the
+relation already names the type. It earns its keep for a tuple in
+flight, which is the admission case.
+
+Two representations exist for the same value. The evaluator and the
+protocols carry tuples as plain values, which is what a cursor yields
+and what a program receives as bindings. Storage keeps the attributes
+as their own content addressed subtree, so that two tuples asserting
+the same thing share one representation, and identical attributes
+yield an identical address regardless of the order in which they were
+written. Ephemeral tuples, which are never interned, are values that
+simply never reach storage.
+
 * Multigroup
 A multigroup represents a collection of related groups and is
 represented logically by a database of relations considered together