diff --git a/lib/host/blog.sx b/lib/host/blog.sx index 947f38d7..add90e83 100644 --- a/lib/host/blog.sx +++ b/lib/host/blog.sx @@ -177,10 +177,14 @@ (tail (substr body (+ p1 1)))) (let ((p2 (index-of tail "|"))) (when (>= p2 0) - (relations/relate - (host/blog--node src) - (host/blog--node (substr tail (+ p2 1))) - (string->symbol (substr tail 0 p2)))))))))) + (let ((ek (substr tail 0 p2))) + ;; conj/disj are structural (type-algebra operands) — KV-only, + ;; never replayed into the Datalog graph (it re-saturates per query). + (when (not (or (= ek "conj") (= ek "disj"))) + (relations/relate + (host/blog--node src) + (host/blog--node (substr tail (+ p2 1))) + (string->symbol ek))))))))))) (filter (fn (k) (starts-with? k "edge:")) (persist/backend-kv-keys host/blog-store))))) @@ -277,6 +281,55 @@ (host/blog--uniq (reduce (fn (acc t) (concat acc (host/blog-in t "is-a"))) (list) subtypes))))) +;; ── Slice 4: type ALGEBRA — intersection (∧) and union (∨) types ───── +;; An algebraic type is a post with operand edges: a `conj` edge per intersection +;; member, a `disj` edge per union member. Its EXTENT is its operands' extents combined +;; by set intersection / union, recursively — so types compose into an algebra in the +;; same graph (meta-circular: an algebraic type is just another post). Binary today +;; (nth 0/1, no fold over operands — robust on the serving JIT); n-ary is a follow-up. +;; is-a-expr? generalises is-a? to type expressions. +(define host/blog--set-intersect + (fn (xs ys) (filter (fn (x) (contains? ys x)) xs))) +;; operand edges live in the KV ONLY (read back via host/blog-out), NOT in lib/relations: +;; conj/disj are structural, and feeding extra kinds into the Datalog graph blows up its +;; per-query re-saturation. host/blog-load-edges! skips them on replay for the same reason. +(define host/blog--add-edge-kv! + (fn (src dst kind) + (persist/backend-kv-put host/blog-store (host/blog--edge-key src kind dst) 1))) +(define host/blog-make-and! + (fn (t a b) + (begin + (host/blog-seed! t t + (str "(article (h1 \"" t "\") (p \"An intersection type (" a " ∧ " b ") — its instances are exactly those that are instances of BOTH.\"))") + "published") + (host/blog--add-edge-kv! t a "conj") + (host/blog--add-edge-kv! t b "conj")))) +(define host/blog-make-or! + (fn (t a b) + (begin + (host/blog-seed! t t + (str "(article (h1 \"" t "\") (p \"A union type (" a " ∨ " b ") — its instances are those that are instances of EITHER.\"))") + "published") + (host/blog--add-edge-kv! t a "disj") + (host/blog--add-edge-kv! t b "disj")))) +;; the EXTENT of a type expression: operands' extents combined by set ops (recursive). +;; A plain type (no operands) falls through to its instances. +(define host/blog-instances-of-expr + (fn (t) + (let ((conj (host/blog-out t "conj")) + (disj (host/blog-out t "disj"))) + (cond + ((>= (len conj) 2) + (host/blog--set-intersect (host/blog-instances-of-expr (nth conj 0)) + (host/blog-instances-of-expr (nth conj 1)))) + ((>= (len disj) 2) + (host/blog--uniq (concat (host/blog-instances-of-expr (nth disj 0)) + (host/blog-instances-of-expr (nth disj 1))))) + (else (host/blog-instances-of t)))))) +;; is `slug` a member of the type expression `t`? Generalises is-a? to the algebra. +(define host/blog-is-a-expr? + (fn (slug t) (contains? (host/blog-instances-of-expr t) slug))) + ;; ── tags (a tag is a post that is-a tag) ──────────────────────────── (define host/blog-is-tag? (fn (slug) (host/blog-is-a? slug "tag"))) (define host/blog-tags (fn (slug) (host/blog-out slug "tagged"))) ;; a post's tags diff --git a/lib/host/tests/blog.sx b/lib/host/tests/blog.sx index 94e25225..a290fc9c 100644 --- a/lib/host/tests/blog.sx +++ b/lib/host/tests/blog.sx @@ -527,6 +527,29 @@ (contains? (host/blog-out "alpha-post" "is-a") "beta-post")) false) +;; -- Slice 4: type ALGEBRA — intersection (∧) and union (∨) types -- +;; ocaml is-a tag (seeded above); make it is-a article too, so it's in BOTH extents. +(host/blog-relate! "ocaml" "article" "is-a") +(host/blog-make-and! "taggy-article" "tag" "article") ;; tag ∧ article +(host/blog-make-or! "tag-or-article" "tag" "article") ;; tag ∨ article +(host-bl-test "intersection (∧): a member iff it's an instance of BOTH operands" + (list (host/blog-is-a-expr? "ocaml" "taggy-article") ;; is-a tag AND is-a article + (host/blog-is-a-expr? "ppost" "taggy-article")) ;; neither + (list true false)) +(host-bl-test "union (∨): a member iff it's an instance of EITHER operand" + (list (host/blog-is-a-expr? "ocaml" "tag-or-article") ;; is-a tag (and article) + (host/blog-is-a-expr? "ppost" "tag-or-article")) ;; neither tag nor article + (list true false)) +(host-bl-test "the extent is the set intersection of the operands' extents" + (let ((ext (host/blog-instances-of-expr "taggy-article"))) + (list (contains? ext "ocaml") ;; in tag ∩ article + (contains? ext "ppost"))) ;; in neither + (list true false)) +;; algebra is META-CIRCULAR: an operand can itself be an algebraic type. +(host/blog-make-and! "nested-and" "taggy-article" "tag") ;; (tag ∧ article) ∧ tag +(host-bl-test "nested type expression: (tag ∧ article) ∧ tag still admits ocaml" + (host/blog-is-a-expr? "ocaml" "nested-and") 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")) diff --git a/plans/relations-as-posts.md b/plans/relations-as-posts.md index 4529253a..e1ab9c58 100644 --- a/plans/relations-as-posts.md +++ b/plans/relations-as-posts.md @@ -85,16 +85,20 @@ relation-subtype closure when relations get subtyped; the boot title cache above - NOTE: `host/blog-relate!` (direct/seed) stays UNVALIDATED — the seed needs to write `X is-a relation` where `relation` isn't under `type`. Validation is a *handler* boundary. -### Slice 4 — type algebra -Types are posts + `subtype-of` is a partial order ⇒ a **lattice**, and `is-a?` is transitive -set-membership ⇒ extents have set semantics. So algebra is expressible as posts: -- **Intersection** `A ∧ B` — a type-post whose membership predicate is `is-a? A ∧ is-a? B` - (meet / GLB in the lattice). **Union** `A ∨ B` — `is-a? A ∨ is-a? B` (join / LUB). -- **Refinement** `{x : T | φ(x)}` — a type-post with a `:constraint` predicate over a post - (generalises today's `article` schema "must have a heading"). Gradual: declaring the type - adds the obligation; the next save must satisfy it. -- Algebraic types are *themselves posts* with edges to their operands — `is-a?` recurses on - the expression. Meta-circular: the algebra lives in the graph it describes. +### Slice 4 — type algebra — DONE (intersection ∧ union) +- An algebraic type is a post with operand edges: `conj` edges (intersection members), + `disj` edges (union members). `host/blog-instances-of-expr` computes its EXTENT from the + operands' extents by set intersection / union, RECURSIVELY — so operands can themselves be + algebraic (meta-circular; tested with `(tag ∧ article) ∧ tag`). `host/blog-is-a-expr?` + generalises `is-a?` to type expressions. `host/blog-make-and!` / `make-or!` build them. +- Binary today (`nth 0/1`, no fold over operands — robust on the serving JIT); n-ary fold is + a follow-up once iteration-with-perform is JIT-reliable. +- **Operand edges are KV-only** (`host/blog--add-edge-kv!`, read via `host/blog-out`), NOT in + lib/relations — feeding extra kinds into the Datalog graph blows up its per-query + re-saturation; `load-edges!` skips `conj`/`disj` on replay for the same reason. +- **Refinement** `{x : T | φ(x)}` (a type-post with a `:constraint` predicate) → Slice 5, + 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 - Promote the schema/`:constraint` slot to **constraint-posts** (a predicate expr +