diff options
Diffstat (limited to 'docs/sakura-RNT-integration.org')
| -rw-r--r-- | docs/sakura-RNT-integration.org | 43 |
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 |