host: relations-as-posts slice 5 — refinement types (schemas on the type-post)

A type-post carries its schema in a :schema slot (a list of {:block :msg} rules — a
refinement {x : T | x has these blocks}). host/blog-schema-of reads it off the post;
the hardcoded host/blog-type-schemas table is gone. A NEW refinement type is pure
data: give a type-post a :schema and its instances are validated on save — no code
(tested with a 'guide' type requiring a 'pre' block). article's schema is migrated
onto the article post at boot (host/blog--set-schema!, a single read+write).

host/blog-put! now MERGES over the previous record, so editing a post's
title/content doesn't nuke its :schema/:rel metadata (also closes the Slice 2
'edit drops :rel' gap). schema-of reads the post (a durable read) — only the SAVE
path calls it (a write request, never a render that would VmSuspend).

conformance 299/299 (+4: article h1 enforced from the post, a new refinement type
validates its instances, schema read off the post, edit preserves :schema).

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>

lib/host/blog.sx

@@ -32,10 +32,15 @@
   (fn (slug) (persist/backend-kv-get host/blog-store (host/blog--key slug))))
 (define host/blog-exists?
   (fn (slug) (persist/backend-kv-has? host/blog-store (host/blog--key slug))))
+;; A write preserves any extra slots already on the record (:rel for relation-posts,
+;; :schema for refinement types) — merging over the previous record — so editing a
+;; post's title/content/status doesn't nuke the metadata that lives alongside it.
 (define host/blog-put!
   (fn (slug title sx-content status)
-    (persist/backend-kv-put host/blog-store (host/blog--key slug)
+    (let ((prev (host/blog-get slug)))
-      {:slug slug :title title :sx-content sx-content :status status})))
+      (persist/backend-kv-put host/blog-store (host/blog--key slug)
+        (merge (if prev prev {})
+          {:slug slug :title title :sx-content sx-content :status status})))))
 (define host/blog-delete!
   (fn (slug) (persist/backend-kv-delete host/blog-store (host/blog--key slug))))
 (define host/blog-seed!
@@ -335,15 +340,26 @@
 (define host/blog-tags (fn (slug) (host/blog-out slug "tagged")))          ;; a post's tags
 (define host/blog-tagged-with (fn (tag) (host/blog-in tag "tagged")))      ;; posts with a tag
 
-;; ── gradual validation: declarative type schemas ───────────────────
+;; ── gradual validation: refinement types (schemas ON the type-post) ──
-;; A type may carry a SCHEMA: a list of rules {:block <tag> :msg <why>}, each
+;; A type-post may carry a SCHEMA in a :schema slot: a list of rules
-;; requiring the content to contain (anywhere) an element of that tag. A post is
+;; {:block <tag> :msg <why>}, each requiring the content to contain (anywhere) an
-;; checked against the schema of every type it is-a; a type with no schema imposes
+;; element of that tag — i.e. a refinement type {x : T | x has these blocks}. A post
-;; nothing (gradual). Schemas are declarative data (not opaque predicates) so they
+;; is checked against the schema of every type it is-a; a type with no schema imposes
-;; yield a specific, human error — and could later be stored ON the type-post.
+;; nothing (gradual). Schemas are declarative data (not opaque predicates), so they
-(define host/blog-type-schemas
+;; yield a specific, human error AND live on the type-post (Slice 5) — make a new
-  {:article (list {:block "h1" :msg "an article needs a heading (h1)"})})
+;; refinement type by giving its post a :schema (host/blog--set-schema!).
-(define host/blog-schema-of (fn (type-slug) (get host/blog-type-schemas type-slug)))
+;; schema-of reads the type-post; only the SAVE path calls it (a write request, where
+;; a durable read is fine — never in a render, which would VmSuspend).
+(define host/blog-schema-of (fn (type-slug) (get (host/blog-get type-slug) :schema)))
+;; attach/replace a type-post's :schema (idempotent; preserves the rest of the record).
+;; Used at boot to install schemas on type-posts — incl. migrating ones seeded before
+;; schemas lived on the post (a single read+write, not a loop, so boot-JIT-safe).
+(define host/blog--set-schema!
+  (fn (slug schema)
+    (let ((r (host/blog-get slug)))
+      (when r
+        (persist/backend-kv-put host/blog-store (host/blog--key slug)
+          (merge r {:schema schema}))))))
 
 ;; every element tag in a parsed content tree, recursively (the heads of nested
 ;; lists) — so "requires h1" matches an h1 even inside an article/section wrapper.
@@ -417,6 +433,8 @@
         "(article (h1 \"Article\") (p \"A kind of post that must have a heading. A post that is-a article is checked against this type's schema on save — gradual typing: declaring the type adds the requirement, and the next edit must satisfy it.\"))"
         "published")
       (host/blog-relate! "article" "type" "subtype-of")
+      ;; article's schema lives ON the article post now (Slice 5) — install/migrate it.
+      (host/blog--set-schema! "article" (list {:block "h1" :msg "an article needs a heading (h1)"}))
       ;; relation DECLARATIONS (see plans/relations-as-posts.md). A type-post declares
       ;; which relation it anchors at its OBJECT end ("you may point at me with R"); the
       ;; picker's candidate set is the down-closure of a relation's anchors through the

lib/host/tests/blog.sx

@@ -550,6 +550,32 @@
 (host-bl-test "nested type expression: (tag ∧ article) ∧ tag still admits ocaml"
   (host/blog-is-a-expr? "ocaml" "nested-and") true)
 
+;; -- Slice 5: refinement types — schemas live ON the type-post --
+;; article's schema (now on the article post) is still enforced for its instances.
+(host/blog-put! "art-test" "Art Test" "(p \"x\")" "published")
+(host/blog-relate! "art-test" "article" "is-a")
+(host-bl-test "article (refinement type, schema on the post) requires an h1"
+  (list (host/blog-type-valid? "art-test" "(p \"no heading\")")              ;; missing h1
+        (host/blog-type-valid? "art-test" "(article (h1 \"H\") (p \"x\"))"))  ;; has h1
+  (list false true))
+;; a NEW refinement type is pure data: give a type-post a :schema and its instances
+;; are validated against it — no code, no hardcoded table.
+(host/blog-seed! "guide" "Guide" "(article (h1 \"Guide\") (p \"A guide.\"))" "published")
+(host/blog-relate! "guide" "type" "subtype-of")
+(host/blog--set-schema! "guide" (list {:block "pre" :msg "a guide needs a code block (pre)"}))
+(host/blog-put! "g1" "G1" "(p \"x\")" "published")
+(host/blog-relate! "g1" "guide" "is-a")
+(host-bl-test "a NEW refinement type validates its instances against its :schema"
+  (list (host/blog-type-valid? "g1" "(p \"no code\")")                       ;; missing pre
+        (host/blog-type-valid? "g1" "(article (pre \"x\") (p \"y\"))"))      ;; has pre
+  (list false true))
+(host-bl-test "the schema is read off the type-post (data, not a hardcoded table)"
+  (contains? (str (host/blog-schema-of "guide")) "code block") true)
+;; editing a refinement type preserves its :schema (put! merges over the record).
+(host/blog-put! "guide" "Guide v2" "(article (h1 \"Guide\") (p \"edited\"))" "published")
+(host-bl-test "editing a type-post preserves its :schema (and metadata survives edits)"
+  (contains? (str (host/blog-schema-of "guide")) "code block") true)
+
 ;; -- Phase 3: tags as posts --  (ocaml is-a tag, from the seed-types test above)
 (host-bl-test "is-tag?: a post that is-a tag is a tag; others are not"
   (list (host/blog-is-tag? "ocaml") (host/blog-is-tag? "ppost"))

plans/relations-as-posts.md

@@ -100,11 +100,21 @@ relation-subtype closure when relations get subtyped; the boot title cache above
   with constraints-as-posts. (Process note: a sibling loop running heavy conformance saturates
   the box; host conformance can EXIT 124 purely from CPU contention — use `timeout 1200`.)
 
-### Slice 5 — constraints as posts + validation
+### Slice 5 — refinement types (schemas ON the type-post) — DONE
-- Promote the schema/`:constraint` slot to **constraint-posts** (a predicate expr +
+- A type-post carries its schema in a `:schema` slot (a list of `{:block :msg}` rules —
-  message), attachable to any type. Save-time validation evaluates the constraints of a
+  a refinement `{x : T | x has these blocks}`). `host/blog-schema-of` reads it off the
-  post's full (transitive) type set. Relation cardinality (`is-a` single-valued? `tagged`
+  post; the hardcoded `host/blog-type-schemas` table is gone. A NEW refinement type is pure
-  many?) becomes a declared constraint too.
+  data: give a type-post a `:schema` (`host/blog--set-schema!`) and its instances are
+  validated on save against it — no code. Tested with a `guide` type requiring a `pre` block.
+- Save-time validation (`type-issues`/`type-valid?`, the only callers, in the SAVE request)
+  unions the schemas of a post's full transitive type set — unchanged, just sourced from the
+  posts. `schema-of` reads the post (a durable read) — fine in the save request, never render.
+- `host/blog-put!` now MERGES over the previous record, so editing a post's title/content
+  doesn't nuke its `:schema` / `:rel` metadata (also closes the Slice 2 "edit drops :rel" gap).
+- `article`'s schema migrated onto the article post (`set-schema!` at boot — a single
+  read+write, not a loop, so boot-JIT-safe; idempotent, handles the already-seeded article).
+- FUTURE: arbitrary predicate constraints (not just required blocks); constraints as their
+  own posts; relation cardinality (`is-a` single-valued?) as a declared constraint.
 
 ## Open design questions (track as we go)
 1. **Subject-end declarations** — who may be the *source* of a relation (a root `Thing`?).