#+TITLE: Sol / Sakura / RNT Integration
#+AUTHOR: Marcos Magueta
* Purpose
This document records the architectural decisions binding Sol to the
Sakura relational engine (=../sakura=) and the RNT database kernel
(=../RNT=). These decisions were reached by adversarial design review
(2026-07-11) and are normative: later documents (the pipeline
specification and the VM specification) must not contradict them
without revisiting the arguments recorded here.
* The Stack, As It Exists
Facts established from the codebases, not decisions:
- *RNT* is a database kernel currently being rewritten in OCaml (the
original execution core was C++; its design carries over). Its
execution core, *FOL* (=lib/backend/execution/FOL.ml=), mechanically
evaluates first-order relational plans under the Volcano pull
model. Every plan terminates: evaluation is model
checking against one fixed, finite model, which is decidable. RNT
makes no independent termination judgements; it trusts plan
annotations.
- *Sakura* (OCaml) is the authoritative source of semantics. It owns
cardinality analysis (=Finite= / =ConstrainedFinite= / =AlephZero= /
=Continuum=), termination enforcement (=TAKE= insertion), join
ordering, and physical storage.
- Sakura's sublanguages are cleanly separated modules: DRL (pure
retrieval, total), ICL (integrity constraints as membership checks),
DCL (branch management and 3-way merge over content-addressed
tips), DML (delta semantics), DDL, with TCL planned.
- =sublanguage.ml= classifies operations categorically: a *Query* is a
natural transformation between instance functors (state unchanged);
a *Transition* is a morphism in the category of database states.
- RNT tuples are content-addressed: each tuple is stored under the
SHA256 digest of its serialized bytes. DCL branches point to tips
identified by hash. Database states are therefore already
first-class Merkle-style values in this architecture.
- *Karuta* is a Prolog-like language targeting the BEAM, positioned at
the application layer.
* Decision 1: Totality Is a Stack-Wide Invariant
** The decision
Sol is total, and so is the entire database language stack. The
previously entertained idea of a Turing-complete PPL (predicate
procedure language) — recorded in =sakura/lib/sublanguage.ml= ("PPL ->
new effect class: potentially non-terminating computation") and in
=karuta-integration.org= ("a predicate procedure language might [be
Turing complete]") — is *retracted*.
Problems that genuinely require Turing-complete computation belong in
the application layer (Karuta on the BEAM), not in the database.
** The argument
- P1. A very large class of useful programs is expressible in a total
language: arithmetic, data-structure algorithms, parsers, theorem
provers, sorting, type checkers, relational evaluators — anything
whose recursion is structural and provably terminating.
- P2. Admitting unbounded recursion anywhere in the stack re-imports
the halting problem into every layer above it, destroying the
termination guarantee that RNT's execution core is *named after*
(see =RNT/new-docs/fol.org=: "do not make the query language
Turing-complete").
- P3. Stored procedures are the layer where users write the most
logic; that is the worst possible place to lose the guarantee.
- C. Therefore the database language is total, with no partial
escape hatch inside the database. Partiality lives outside, in the
application layer.
* Decision 2: Sol Is the Database Language; Karuta Compiles to It
** The decision
- Sol is *the* language of the Sakura/RNT RDBMS, and its VM is the
database runtime. It plays the role SQL plays in PostgreSQL: the
language exposed at the REPL and over the wire.
- Karuta remains the application-layer language. It compiles to the
s-expression interchange form and internally targets Sol; this
compilation happens *inside Sakura* — Sakura hosts the Karuta
front-end and lowers it onto Sol, the same way it receives Sol
directly from the REPL or the wire. Karuta does not front the
sublanguages directly anymore; Sol does.
- The sublanguages (DRL, ICL, DCL, DML, DDL, TCL) are not separate
surface languages. They are fragments of Sol, distinguished
semantically (query vs. transition), not syntactically balkanized
as in SQL.
** The argument
- P1 (uniformity requirement). A stored relation and a computed
relation must be handled identically: the same application syntax,
the same membership semantics. "The same way we handle a relation
stored in the database, we invoke a function facing a relational
interface."
- P2. Two surface languages over one semantic core is the negation of
uniformity — it reproduces the SQL disease: a *collection* of
sublanguages with no harmonic whole.
- C. One language, Sol. Everything else (Karuta included) is a
compiler front-end or client of it.
* Decision 3: Transitions Are Relations Over Database States
** The decision
Sol expresses state change (DML, DDL, DCL) as *relations between
database states*. A database state =S= is a first-class value — which
the architecture already supports, since tuples are content-addressed
and branch tips are hashes.
An insert is a relation:
#+BEGIN_SRC sol
[Insert relation: Person tuple: T before: S after: S']
#+END_SRC
This proposition holds exactly when state =S'= is state =S= with =T=
admitted into =Person= (which entails =T= passing every ICL
constraint attached to =Person= — membership checking and integrity
control are the same operation, per the language specification).
Exactly *one* primitive effect exists, outside the logic, at the
edge: *commit* — advancing a branch tip (HEAD) from =S= to =S'=. As
in git: everything is pure value manipulation until the single
mutable reference moves.
** The alternatives rejected
- *Two-layer language* (pure core + imperative command shell, à la
Haskell IO): honest, but bifurcates the grammar into expressions
and commands — DML becomes a foreign sublanguage again, violating
Decision 2's uniformity premise.
- *Smalltalk message-sends with hidden effects* (=Person insert: T=
mutating in place): the surface says "message", the internals
perform a state morphism. Dishonest syntax — the construct's
surface form would not mean what the internals do. Rejected on the
syntax-honesty principle.
** The argument
- P1 (uniformity). Transitions expressed as relations use the same
application syntax, the same conjunction, the same proof-search
semantics as everything else in Sol.
- P2 (fact). Database states are already first-class Merkle values in
RNT/Sakura (content-addressed tuples, hash-identified branch
tips). State-as-value is not an invention; it is a recognition.
- P3 (honesty). =sublanguage.ml= already classifies DML/DDL/ICL/DCL
as morphisms in the category of database states. Making the states
and the morphism explicit in the surface syntax makes the language
say exactly what the semantics do.
- C. An insert *is* a relation over states.
** What this buys
Because =Insert(R, T, S, S')= is an ordinary proposition, it can be
*queried* as well as *performed*:
- provenance and audit are ordinary conjunctions over the state
chain;
- time-travel queries are membership checks against old states;
- dry-run is evaluating the transition relation without committing;
- a transaction is a composition of transition relations
=S → S' → S''=, committed atomically by moving HEAD once, to the
final state;
- DCL merge is already a ternary relation over states (two tips and
an ancestor) — Decision 3 makes the rest of the language match it.
** Acknowledged costs
- State identity and equality must be defined precisely (hash
equality of content-addressed states is the candidate, but
canonical serialization must be specified).
- Sequencing becomes conjunction over chained state variables; the
planner must order these chains. This is real planning work, though
of the same kind DCL merge already performs.
* Decision 4: Sol Is a Library; RNT Links Its Compiler and VM In-Process
** The decision
Sol — the whole pipeline: normalizer, planner, totality checker, and
VM — is built as a host-neutral OCaml library, parameterized over a
=WORLD= interface: the store that answers which relations exist,
their capabilities, how membership is checked against stored tuples,
and what commit means.
Two hosts consume it:
- *Standalone Sol*: a thin binary links the library with an
in-memory or file-backed world. This world exposes only the pure
fragment: no branches exist, so transition relations and commit are
simply absent capabilities (see Decision 5). This satisfies the
requirement that Sol be usable as a separate language for ordinary
(total) programs.
- *RNT*: the kernel links the library in-process as its execution
layer. RNT's planned split between "terminating first-order logic
and higher-order logic execution" is filled directly: the FOL core
executes the finite-plan fragment (=Plan.t=, Volcano), and the HOL
slot *is* Sol's engine — not a reimplementation, the same compiler
internals. The world is the object manager plus the
content-addressed store; commit advances a branch tip atomically
inside the kernel.
** The argument
The earlier framing — "Sol VM inside the kernel" versus "Sol VM as a
client of the kernel" — was a false dichotomy.
- P1 (requirement). Sol must run standalone, with no database
present.
- P2 (Decisions 2–3). Sol's VM is the database runtime, and commit —
the single effect — must be atomic against RNT's branch tips.
- P3. A client-process VM satisfies P1 but makes the only effect
distributed, breaking P2. A kernel-welded VM satisfies P2 but
cannot exist without the database, breaking P1.
- C. The VM must be neither: a library over an abstract world. RNT
linking it in-process preserves atomicity; the standalone host
preserves independence. One implementation, two hosts — an
embeddable runtime in the manner of SQLite or Lua, where one of
the embeddings is the database kernel itself.
The language specification already gestures at this seam: membership
criteria "constructed at the host language," capabilities as declared
operational permissions, =World= as a relation. The =WORLD= interface
is that seam made explicit.
** Acknowledged costs
- The world interface is a hard public contract. Capability
negotiation — which worlds support enumeration, solving, bounded
generation — must be specified precisely.
- Standalone-world semantics must be a strict subset of
database-world semantics, so that a program proven total against
the standalone world remains total in-kernel.
* Decision 5: A State Is a Branch's Whole Tree
** The decision
The state values =S=, =S'= in transition relations denote *branch
states*: the catalog, schemas, ICL constraints, and the extension of
every relation *as one branch sees them*, as one content-addressed
tree — exactly a git commit object. Concretely, =S= is the Merkle
root hash of the branch's tree: a snapshot handle into the
content-addressed store, cheap to hold, structurally shared with
neighboring states.
There is no global "database state" spanning branches. Transition
relations are meaningful only within a branch: a stored procedure
receives the branch's current root hash, evolves it purely — each
transition producing the successor hash — and yields the final hash,
which commit installs as the new tip.
It works like git: all value manipulation is pure; history is a chain
of whole-database states; the single effect (Decision 3) is advancing
a branch tip to a new state.
Consequently, transition relations exist only in the RNT/Sakura
world. The standalone world has no branches, hence no transitions and
no commit — standalone Sol is the pure total fragment. This is
capability negotiation (Decision 4) doing its job, not a special
case.
** The alternative rejected
Per-relation states — the database as a bag of independently
versioned relations — fail on two counts:
- P1. DDL and ICL changes are also transitions (Decision 2); a
per-relation state has no place to record "the schema changed" or
"a constraint was added."
- P2. Integrity constraints span relations (foreign keys as
membership checks against *other* relations). A transition's
validity must be judged against a consistent snapshot of all
relations, or ICL checking is unsound.
- P3 (fact). DCL already works on whole tips: a branch is one hash,
and 3-way merge operates on two tips and an ancestor.
Nothing is lost: in a content-addressed tree, per-relation hashes
still exist as internal nodes, and unchanged subtrees share
structure.
** Acknowledged costs
- Hashing must be incremental — a transition recomputes hashes along
the changed path only (O(path), not O(database)) — or commit
throughput dies. Merkle trees provide exactly this.
- Canonical serialization of states must be specified early; state
equality is hash equality only if serialization is deterministic.
* Decision 6: Sequencing Comes from Linear State Threading, Not Syntax Order
** The decision
Transition sequencing derives *solely* from state-variable sharing,
never from syntactic position:
#+BEGIN_SRC sol
[Insert relation: Person tuple: T1 before: S0 after: S1] :and
[Insert relation: Person tuple: T2 before: S1 after: S2]
#+END_SRC
=:and= remains honestly commutative: swapping the conjuncts changes
nothing, because the chain =S0 → S1 → S2= is carried by unification.
The planner topologically sorts the state chain, the same discipline
Sakura already applies when ordering joins by variable binding.
State variables obey a *linear discipline*, in the manner of
Mercury's =di=/=uo= (destructive-input / unique-output) modes on
=io.state=: within a transaction, each state value is consumed
exactly once (as =before:=) and produced exactly once (as =after:=).
The felt experience is procedural — a timely order, step after step —
but the order is implied by the dataflow, not decreed by the page.
A transaction is a relational expression whose state variables form
one linear chain from the branch tip (=S0= = HEAD) to a final state,
followed by one commit of that final state (Decision 3).
** The argument
- P1. =:and= means logical conjunction, and conjunction is
commutative.
- P2 (syntax honesty). The surface form must mean what the internals
do. If evaluation order were read off the page, =:and= would be a
lie — sequencing dressed as conjunction. This is the same sin the
language specification already rejects in "newline adjacency
secretly means conjunction."
- P3. Unification is Sol's only binding mechanism; threading state
through shared variables introduces no new primitive.
- C. Order-from-dataflow is the only admissible sequencing. The
linear mode discipline makes chain-hood a static property: a fork
(two transitions consuming the same =S=) or a reuse is a mode
error caught at admission, not a planner heuristic.
** Sugar policy
A convenience form (e.g. a =Transaction do:= that auto-threads the
state variables) is permitted *only* as sugar with a published
elaboration into the explicit chain. It must never become a
primitive with its own semantics.
** Acknowledged costs
- Verbosity until sugar lands: users name =S0=, =S1=, =S2=
explicitly.
- The mode/linearity checker must be specified as part of admission
checking, alongside schema and totality checks.
* Decision 7: Reads Are State-Scoped
** The decision
In the RNT/Sakura world, *every* read of a stored relation happens
from an explicit state. In the core language, a stored-relation
application carries the state it reads at:
#+BEGIN_SRC sol
[Person id: P age: A at: S1]
#+END_SRC
A scoping form is provided as sugar, with a published elaboration
that distributes the state over the stored-relation applications in
its body (Decision 6's sugar policy):
#+BEGIN_SRC sol
[At state: S1 body: [Person id: P age: A] :and [Adult person: P]]
#+END_SRC
At the REPL, a bare query elaborates to =at:= the current branch
tip's state — one uniform rule, not a second semantics.
Standalone Sol is untouched: it has no stored relations, hence no
=at:=.
** The argument
- P1 (Decision 6). Order on the page carries no meaning; so "read
whatever the previous statement produced" is not available — it is
positional order, the outlawed lie.
- P2. Reads must therefore name their state, or a hidden convention
decides — dishonest syntax.
- P3. The alternative — all reads pinned to the transaction's initial
=S0= — makes read-your-own-writes inexpressible: a procedure that
inserts and then validates against the result cannot be written,
even though ICL checking inside the chain already reads
intermediate states. The language would forbid users what its own
machinery does.
- C. Reads are state-scoped in the core; terseness is recovered by
sugar, never by convention.
** Acknowledged costs
- =at:= becomes a reserved label on stored-relation applications; it
cannot be a schema attribute name.
- The elaboration of =At state: body:= must be specified precisely,
including its interaction with nested =At= forms (innermost wins)
and with transition relations (which are already explicit and are
not rescoped).
* Decision 8: The Kernel Arbitrates Only the Tip; Conflict Policy Is DCL
** The decision
The only point of contention in RNT is the tip of a branch. The
kernel therefore provides exactly one concurrency primitive: *atomic
compare-and-swap on a branch tip* — install =Sn= as the tip iff the
tip still equals the =S0= the transaction started from.
Everything above that primitive is the version-control language's
domain, and DCL is a fragment of Sol (Decision 2) operating on
states as values (Decision 5):
- *fast-forward*: the tip is an ancestor of =Sn= — install directly;
- *rebase*: re-execute the procedure from the new tip — sound and
safe because a transaction is a pure, total function of its
initial state (Decisions 3, 6); nothing partial ever escaped;
- *3-way merge*: already a ternary relation over two tips and their
ancestor, with declared strategies (=PreferLeft=, =PreferRight=,
=RevertToAncestor=).
Conflict policy is thus *expressed in the language*, not hardcoded
in the kernel.
** The argument
- P1. A pure total transaction has no partial effects to undo;
re-execution from a moved tip is always safe and always
terminates. The classical difficulty of transaction retry does not
exist here.
- P2. Given P1, any policy the kernel could hardcode (retry, merge,
reject) is expressible as relations over states — and DCL already
contains the vocabulary.
- P3 (minimality). A kernel primitive should exist only where the
kernel is the sole possible arbiter. Tip installation is the one
such place; policy is not.
- C. Kernel = CAS on the tip. Policy = DCL, in Sol.
** Acknowledged costs
- Any retry/arbitration loop is unbounded under contention. It lives
outside the total language — in the commit arbiter or client,
alongside the REPL loop. Sol proves each execution terminates; the
arbiter decides how many executions happen. Partiality is confined
to that boundary and must be documented as such, with a
fairness/backoff policy.
* Decision 9: No DRL Syntax — the Plan Is Chosen by Analysis
** The decision
There is no distinguished DRL surface form. The user writes uniform
Sol; the planner decides how each subexpression executes. Since
*both* engines are total, engine choice is not a semantic
distinction and must not be a syntactic one: it changes performance,
never meaning (Codd's theorem licenses the lowering — the finite
first-order fragment and the plan algebra are the same queries).
What actually distinguishes subexpressions is what their relations
*are*:
- *stored relations* — scanned at an explicit state =S=
(Decision 7);
- *ephemeral relations* — algebraic artifacts of relational
operations, carrying provenance and lineage (Sakura's existing
notion);
- *rule- and procedure-defined relations* — unfolded, or evaluated
by fixpoint on Sol's engine.
The planner — reusing Sakura's cardinality propagation (=Finite= /
=ConstrainedFinite= / =AlephZero= / =Continuum=), constraint
propagation, boundness/mode analysis, and join ordering — identifies
maximal finite, first-order, non-recursive subexpressions and lowers
them to the plan algebra (=Plan.t=) for RNT's FOL core. Everything
else runs on Sol's engine, which pulls from lowered plans as cursors
(Volcano composes across the seam).
** The argument
- P1 (Decision 2). Sublanguages are semantic fragments, not
syntactic ones; a DRL marker would re-balkanize the language.
- P2 (totality, Decision 1). Both engines halt, so there is no
observable semantic difference for a marker to honestly denote.
- P3 (fact). Sakura already computes the needed evidence —
cardinality tags, TAKE insertion, boundness-driven join ordering.
The lowering criterion reuses existing analysis.
- C. Fragment-by-analysis. The FOL core is an invisible optimization
target; the observable contract is only the tuple stream.
** Acknowledged costs
- Each lowering must be meaning-preserving and should be checkable
(the =Plan.t= translation is a verifiable step, not a trusted
one).
- A user who needs the guarantee "this runs as a flat finite plan"
gets it as a declarable *assertion* (reject if not lowerable),
never as a separate language.
* Decision 10: Totality Is Established at Admission, Verified in Rocq
** The decision
Totality evidence is checked at *admission time*: defining a rule or
procedure is itself a DDL transition (=[DefineRule ... before: S
after: S']=), and the definition fails — the successor state does not
come to exist — unless the evidence is present. A state containing a
non-total rule is unrepresentable; queries therefore run against
states where everything is already proven total and pay nothing at
query time.
The evidence is a closed ladder; each rung is recorded in the rule's
metadata:
1. *Structural decrease* — the checker finds a strictly decreasing
argument (e.g. =Tail= < =[Head | Tail]= in =Length=). Automatic;
covers most honest recursion.
2. *Bounded quantification* — the searched space is =Finite= or
=ConstrainedFinite= by Sakura's cardinality analysis.
3. *Symbolic discharge* — algebraic properties prove the universal
or the recursion (e.g. =Plus(X, 0) = X= over all integers).
4. *Certificate* — a Rocq proof, checked before admission. Because
the certificate is verified, this rung is not a trusted escape
hatch. A merely *trusted* declaration remains possible only as a
last resort: named, auditable, and loud.
Anything fitting no rung is *rejected* — never admitted as a pending
obligation.
Two levels, not conflated:
- *Object level*: the ladder above, run by the in-engine admission
checker on each definition.
- *Metatheory*: Rocq/Coq proves the guarantees of RNT/Sakura
themselves — soundness of the admission checker ("any accepted
rule is total"), meaning-preservation of the =Plan.t= lowering
(Decision 9), soundness of ICL checking, and merge respecting its
specification. Since RNT and Sakura are OCaml, the critical
checkers should be *extracted* from Rocq to OCaml, so the thing
proven is the thing running.
** The argument
- P1 (Decision 5). States are values. A state containing an unproven
rule is a state whose queries might not halt; admitting it
falsifies the totality invariant *inside* every descendant state.
- P2. "Obligation pending" is Coq's =admit=: tolerable in an
interactive proof, poisonous in a database that other parties
query concurrently.
- P3. A checker that is itself unverified moves the trust boundary
rather than discharging it; the Rocq metatheory closes that gap.
- C. Total-or-absent at admission; verified checker; certificates as
proofs, not promises.
** Acknowledged costs
- The structural-decrease checker and the symbolic-discharge engine
must be specified precisely (the pipeline document owns this).
- Rocq extraction constrains implementation style in the affected
modules (pure, extraction-friendly OCaml).
- Proof maintenance is a real, ongoing cost paid for the guarantee
that is the project's entire premise.
* Decision 11: The Catalog Is Relations
** The decision
Everything in a state is a relation, and everything is queryable —
including the catalog itself. Relation definitions, schemas, rules,
constraints, and capabilities are tuples in catalog relations, stored
in the same content-addressed tree, read at a state like anything
else:
#+BEGIN_SRC sol
[Relation name: N schema: Sch at: S]
[Constraint name: C relation: R body: B at: S]
#+END_SRC
(A concrete catalog plan already exists on the Sakura/RNT side; this
decision binds Sol to it.)
** What follows
- DDL is DML on catalog relations: =DefineRelation= is an insert
into the catalog — one mechanism, not two (Decision 3 already made
DDL a transition; this removes its last special machinery).
- Admission checking (Decision 10) becomes ICL on the catalog: "a
rule tuple enters =Catalog.Rule= only with totality evidence" is
an ordinary integrity constraint on an ordinary relation.
- Introspection is an ordinary query at =S= — which merge,
migrations, and tooling need anyway.
** The argument
- P1 (Decision 2). A catalog reachable only through special forms is
a second interface — the SQL disease; =information_schema= is
SQL's own admission that it bolted this on too late.
- P2. Catalog-as-relations lets Decisions 3 and 10 collapse into
existing machinery instead of demanding parallel mechanisms.
- C. The catalog is stored relations, guarded by ICL, versioned in
the tree, queryable in Sol.
** Acknowledged costs
- Metacircular bootstrap: the catalog's schema must describe itself
(the fixed point every self-describing catalog has — Postgres's
=pg_class= describes =pg_class=), and some base constraints must
be primitive rather than ICL-expressed.
* Decision 12: Subtyping Is Proven Inclusion; Identity Is Intensional; Quotients Are Canonical
** The decision
Sol's type system represents subtyping, and it is *semantic*
subtyping — subtyping is relation inclusion:
#+BEGIN_EXAMPLE
S <: T ≜ ∀x. S(x) → T(x)
#+END_EXAMPLE
Subsumption is not a rule added to the logic; it is the transitivity
of membership: =x ∈ S ∧ S ⊆ T ⊢ x ∈ T=. A refinement is a subtype by
construction (it is an intersection). =Natural <: Integer= because
ℕ ⊆ ℤ.
Three clauses make this precise:
*** (1) Inclusion judgments go through the evidence ladder
=S <: T= is a universal over a possibly infinite domain —
undecidable in general. A subtyping judgment is therefore admitted
by exactly the regime of Decision 10:
- declared-and-checked facts for the base lattice (=Natural <:
Integer= lives in the catalog, queryable, per Decision 11);
- symbolic discharge for refinements (constraint implication:
=x ≥ 18 → x ≥ 0=);
- finite scan for finite relations;
- Rocq certificate otherwise.
Inclusion between arbitrary relations is never silently inferred.
*** (2) Relation identity is intensional, never structural
Two relations with identical label sets are not the same relation.
Identity comprises the schema *and* the membership criterion (the
intension) — one relation conjoined with a =GreaterThan= constraint
is semantically different from its unconstrained twin — and, for
ephemeral relations, provenance and lineage (Sakura's existing
notions). Consequently:
- shape implies nothing: no structural typing, no implicit width
subtyping;
- a tuple with more labels does not silently inhabit a
narrower-schema relation — *projection* is the explicit morphism
for forgetting attributes, and it stays explicit.
*** (3) Quotient domains use canonical minimal-shape representatives
Rationals expose the classical quotient problem: ℚ is
ℤ × (ℤ∖{0}) quotiented by =(a,b) ~ (c,d) ⟺ ad = bc=, so
={numerator: 2 denominator: 2}=, ={numerator: 1 denominator: 1}=,
and =1= all denote one value. Sol resolves quotients by *canonical
representatives*, enforced by the domain's own membership criterion,
and canonicalization picks the *minimal shape*: an integer-valued
rational normalizes to the ground integer itself
(={numerator: 2 denominator: 2}= normalizes to =1=, not to
={numerator: 1 denominator: 1}=).
Therefore ℤ ⊂ ℚ holds *literally, as membership inclusion* —
representation does not limit inclusion, and no injection or
coercion machinery exists. Non-canonical pairs are pre-values that
normalize in, via a normalization relation declared as part of the
domain's catalog definition:
#+BEGIN_SRC sol
[RationalNormalize raw: {numerator: 2 denominator: 2} canonical: 1]
#+END_SRC
The alternative — setoids, where all representatives are members and
every relation carries congruence obligations with a per-domain
=Equal= — is rejected: congruence proofs metastasize over every rule
ever defined.
** The argument
- P1 (Decision 5). States are content-addressed; state equality is
hash equality. If two representatives of one value could both be
stored, equal databases would hash differently — hash equality
would be a lie. Canonical forms are *mandated* by the Merkle
store, not merely preferred.
- P2. Given canonical forms, choosing the minimal shape as canonical
is the unique choice under which numeric-tower inclusion
(ℤ ⊂ ℚ) is true on the nose rather than simulated by coercion.
- P3. Normalization is already one third of Sol's execution model
("proof search, constraint propagation, and normalization") — no
new primitive is introduced.
- C. Subtyping as proven inclusion, intensional identity, canonical
quotients.
** Acknowledged costs
- Operations over quotient domains accept mixed shapes and
normalize at the boundary (e.g. =Plus= over =Rational= handles
ground integers and canonical pairs).
- A quotient domain without a declared normalization relation is
rejected at admission: no equivalence without a normalizer.
- The subtype lattice for base domains must be seeded in the catalog
bootstrap (Decision 11's metacircular fixed point grows slightly).
* Decision 13: OCaml for the Implementation, Rocq for the Proofs
** The decision
The Sol compiler and VM are written in OCaml. The verified checkers
of Decision 10 are written in Rocq and extracted to OCaml. Other
languages were considered and rejected for the kernel line; the
exploration appetite is spent above it: Rocq itself, Karuta on the
BEAM, and wire clients in any language.
** The argument
- P1 (Decision 4). Sol is a library that RNT links in-process, and
RNT and Sakura are OCaml. A foreign runtime inside the kernel
process reintroduces FFI seams exactly where atomicity and shared
representation of content-addressed values matter most.
- P2 (Decision 10). The extraction pipeline is load-bearing: "the
thing proven is the thing running." Rocq's mature extraction
target is OCaml; Scheme extraction is unmaintained, and no
extraction to Common Lisp exists.
- P3. The performance and correctness profile wanted here (native
compilation, memory safety, strong static types) is OCaml's exact
niche, and it is the lingua franca of compiler construction.
- C. OCaml for compiler and VM; Rocq with extraction for the
verified core.
* Decision 14: No Application in Term Position
** The decision
A block =[Relation ...]= is a proposition, never a term. Nested
application as a value, as in =[Equal left: [Plus left: X right: 0]
right: X]=, is rejected from the language. Statements about the
results of relations are written flat, as membership:
#+BEGIN_SRC sol
[Plus left: X right: 0 result: X]
#+END_SRC
** The argument
- P1 (delimiter law). Each delimiter has exactly one role. An
application that is a proposition in one position and a value in
another reintroduces the position-dependent meaning the delimiter
law exists to forbid.
- P2 (relations are not functions). Elaborating an application into
a term requires knowing which attribute is "the" result, but a
relation is a set of labeled tuples with no distinguished output;
label symmetry and mode freedom are core doctrine. The sugar would
smuggle function orientation into the semantics, and it is only
coherent at modes where the relation happens to be single valued:
a partial, mode-dependent elaboration hidden behind innocent
syntax.
- P3 (the motivation dissolves). The nested form is a functional
accent, not expressive power: =Equal(Plus(X, 0), X)= is exactly
=Plus(X, 0, X)=, which is shorter and states the law as
membership, which is what Sol says everything is.
- C. Applications are propositions, everywhere.
** The one honest future door
If ergonomic pressure ever genuinely demands nested applications,
they are admissible only as sugar over relations whose catalog
schema *declares* a principal result attribute and a single
valuedness capability at the relevant mode, with a published
elaboration (fresh variable plus flat conjunct). The privilege must
be explicit and queryable, never assumed from position. Until a real
program hurts without it, it is not built.
* Consequences for the Pending Documents
- =docs/core-design-and-pipeline.org= must treat transition relations
as first-class in normalization, planning, and totality checking.
- =docs/virtual-machine-specification.org= must specify: the state
value representation (content-addressed), the evaluation of
transition relations, and the single commit primitive as the only
effectful operation in the VM.
- Sol's DRL fragment must normalize to plans executable by RNT's FOL
core (the =Plan.t= algebra: Scan, Project, Join, Union, Rename,
Take, Materialize), with Sakura-style cardinality annotation.
