decision 14: no application in term position, spec example rewritten flat

1 files changed, 43 insertions, 0 deletions

diff --git a/docs/sakura-RNT-integration.org b/docs/sakura-RNT-integration.org
index 145c01e..8207ee5 100644
--- a/docs/sakura-RNT-integration.org
+++ b/docs/sakura-RNT-integration.org
@@ -735,6 +735,49 @@ BEAM, and wire clients in any language.
 - 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