host: relations-as-posts slice 4 — type ALGEBRA (intersection ∧ union)
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 25s
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 25s
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 — operands can themselves be algebraic (meta-circular; tested with (tag ∧ article) ∧ tag). host/blog-is-a-expr? generalises is-a? to type expressions; make-and!/make-or! build them. Binary today (nth 0/1, no fold over operands — robust on the serving JIT). 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 too. conformance 295/295 (+4: intersection/union membership, extent = set op, nested expr). (NB: host conformance can EXIT 124 purely from a sibling loop's CPU contention — ran with timeout 1200.) Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
This commit is contained in:
@@ -177,10 +177,14 @@
|
|||||||
(tail (substr body (+ p1 1))))
|
(tail (substr body (+ p1 1))))
|
||||||
(let ((p2 (index-of tail "|")))
|
(let ((p2 (index-of tail "|")))
|
||||||
(when (>= p2 0)
|
(when (>= p2 0)
|
||||||
|
(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
|
(relations/relate
|
||||||
(host/blog--node src)
|
(host/blog--node src)
|
||||||
(host/blog--node (substr tail (+ p2 1)))
|
(host/blog--node (substr tail (+ p2 1)))
|
||||||
(string->symbol (substr tail 0 p2))))))))))
|
(string->symbol ek)))))))))))
|
||||||
(filter (fn (k) (starts-with? k "edge:"))
|
(filter (fn (k) (starts-with? k "edge:"))
|
||||||
(persist/backend-kv-keys host/blog-store)))))
|
(persist/backend-kv-keys host/blog-store)))))
|
||||||
|
|
||||||
@@ -277,6 +281,55 @@
|
|||||||
(host/blog--uniq
|
(host/blog--uniq
|
||||||
(reduce (fn (acc t) (concat acc (host/blog-in t "is-a"))) (list) subtypes)))))
|
(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) ────────────────────────────
|
;; ── 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-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
|
(define host/blog-tags (fn (slug) (host/blog-out slug "tagged"))) ;; a post's tags
|
||||||
|
|||||||
@@ -527,6 +527,29 @@
|
|||||||
(contains? (host/blog-out "alpha-post" "is-a") "beta-post"))
|
(contains? (host/blog-out "alpha-post" "is-a") "beta-post"))
|
||||||
false)
|
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)
|
;; -- 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"
|
(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"))
|
(list (host/blog-is-tag? "ocaml") (host/blog-is-tag? "ppost"))
|
||||||
|
|||||||
@@ -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
|
- 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.
|
`X is-a relation` where `relation` isn't under `type`. Validation is a *handler* boundary.
|
||||||
|
|
||||||
### Slice 4 — type algebra
|
### Slice 4 — type algebra — DONE (intersection ∧ union)
|
||||||
Types are posts + `subtype-of` is a partial order ⇒ a **lattice**, and `is-a?` is transitive
|
- An algebraic type is a post with operand edges: `conj` edges (intersection members),
|
||||||
set-membership ⇒ extents have set semantics. So algebra is expressible as posts:
|
`disj` edges (union members). `host/blog-instances-of-expr` computes its EXTENT from the
|
||||||
- **Intersection** `A ∧ B` — a type-post whose membership predicate is `is-a? A ∧ is-a? B`
|
operands' extents by set intersection / union, RECURSIVELY — so operands can themselves be
|
||||||
(meet / GLB in the lattice). **Union** `A ∨ B` — `is-a? A ∨ is-a? B` (join / LUB).
|
algebraic (meta-circular; tested with `(tag ∧ article) ∧ tag`). `host/blog-is-a-expr?`
|
||||||
- **Refinement** `{x : T | φ(x)}` — a type-post with a `:constraint` predicate over a post
|
generalises `is-a?` to type expressions. `host/blog-make-and!` / `make-or!` build them.
|
||||||
(generalises today's `article` schema "must have a heading"). Gradual: declaring the type
|
- Binary today (`nth 0/1`, no fold over operands — robust on the serving JIT); n-ary fold is
|
||||||
adds the obligation; the next save must satisfy it.
|
a follow-up once iteration-with-perform is JIT-reliable.
|
||||||
- Algebraic types are *themselves posts* with edges to their operands — `is-a?` recurses on
|
- **Operand edges are KV-only** (`host/blog--add-edge-kv!`, read via `host/blog-out`), NOT in
|
||||||
the expression. Meta-circular: the algebra lives in the graph it describes.
|
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
|
### Slice 5 — constraints as posts + validation
|
||||||
- Promote the schema/`:constraint` slot to **constraint-posts** (a predicate expr +
|
- Promote the schema/`:constraint` slot to **constraint-posts** (a predicate expr +
|
||||||
|
|||||||
Reference in New Issue
Block a user