Add deftype and static effect system to typed-sx plan
Phase 6 (deftype): type aliases, unions, records (typed dict shapes), parameterized types. Phase 7: pragmatic static effect checking — io, dom, async, state annotations with render-mode enforcement, no algebraic handlers, zero runtime cost. Phases 1-5 marked done. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
This commit is contained in:
@@ -176,7 +176,7 @@
|
||||
(dict :label "Runtime Slicing" :href "/plans/runtime-slicing"
|
||||
:summary "Tier the client runtime by need: L0 hypermedia (~5KB), L1 DOM ops (~8KB), L2 islands (~15KB), L3 full eval (~44KB). Sliced by slice.sx, translated by js.sx.")
|
||||
(dict :label "Typed SX" :href "/plans/typed-sx"
|
||||
:summary "Gradual type system for SX. Optional annotations, checked at registration time, zero runtime cost. types.sx — specced, bootstrapped, catches composition errors.")
|
||||
:summary "Gradual type system with static effect checking. Optional type annotations, deftype (aliases, unions, records), and effect declarations — checked at registration time, zero runtime cost. types.sx — specced, bootstrapped, catches composition and boundary errors.")
|
||||
(dict :label "Nav Redesign" :href "/plans/nav-redesign"
|
||||
:summary "Replace menu bars with vertical breadcrumb navigation. Logo → section → page, arrows for siblings, children below. No dropdowns, no hamburger, infinite depth.")
|
||||
(dict :label "Fragment Protocol" :href "/plans/fragment-protocol"
|
||||
|
||||
@@ -69,7 +69,12 @@
|
||||
(~doc-subsection :title "Component types"
|
||||
(~doc-code :code (highlight ";; Component type is its keyword signature\n;; Derived automatically from defcomp — no annotation needed\n\n(comp :title string :price number &rest element)\n;; keyword args children type\n\n;; This is NOT a new syntax for defcomp.\n;; It's the TYPE that a defcomp declaration produces.\n;; The checker infers it from parse-comp-params + annotations." "lisp")))
|
||||
|
||||
(p "That's it. No generics, no higher-kinded types, no dependent types, no type classes. Just: what goes in, what comes out, can it be nil."))
|
||||
(p "That's the core. No higher-kinded types, no dependent types, no type classes. Just: what goes in, what comes out, can it be nil.")
|
||||
|
||||
(~doc-subsection :title "User-defined types"
|
||||
(~doc-code :code (highlight ";; Type alias — a name for an existing type\n(deftype price number)\n(deftype html-string string)\n\n;; Union — one of several types\n(deftype renderable (union string number nil))\n(deftype key-type (union string keyword))\n\n;; Record — typed dict shape\n(deftype card-props\n {:title string\n :subtitle string?\n :price number})\n\n;; Parameterized — generic over a type variable\n(deftype (maybe a) (union nil a))\n(deftype (list-of-pairs a b) (list-of (dict-of a b)))\n(deftype (result a e) (union (ok a) (err e)))" "lisp"))
|
||||
(p (code "deftype") " is a declaration form — zero runtime cost, purely for the checker. The type registry resolves user-defined type names during " (code "subtype?") " and " (code "infer-type") ". Records enable typed keyword args for components:")
|
||||
(~doc-code :code (highlight ";; Define a prop shape\n(deftype card-props\n {:title string\n :subtitle string?\n :price number\n :on-click (-> any nil)?})\n\n;; Use it in a component\n(defcomp ~product-card (&key (props :as card-props) &rest children)\n (div :class \"card\"\n (h2 (get props :title))\n (span (format-decimal (get props :price) 2))\n children))\n\n;; Checker validates dict literals against record shape:\n(~product-card :props {:title \"Widget\" :price \"oops\"})\n;; ^^^^^^\n;; ERROR: :price expects number, got string" "lisp"))))
|
||||
|
||||
;; -----------------------------------------------------------------------
|
||||
;; Annotation syntax
|
||||
@@ -110,9 +115,9 @@
|
||||
(~doc-subsection :title "What it does NOT check"
|
||||
(ul :class "list-disc pl-5 text-stone-700 space-y-1"
|
||||
(li (strong "Runtime values.") " " (code "(if condition 42 \"hello\")") " — the type is " (code "(or number string)") ". The checker doesn't know which branch executes.")
|
||||
(li (strong "Dict key presence.") " " (code "(get user \"name\")") " — the checker knows " (code "get") " returns " (code "any") " but doesn't track which keys a dict has. (Future: typed dicts/records.)")
|
||||
(li (strong "Dict key presence (yet).") " " (code "(get user \"name\")") " — the checker knows " (code "get") " returns " (code "any") " but doesn't track which keys a dict has. Phase 6 (" (code "deftype") " records) will enable this.")
|
||||
(li (strong "Termination.") " That's " (a :href "/plans/theorem-prover" :class "text-violet-700 underline" "prove.sx") "'s domain.")
|
||||
(li (strong "Effects.") " Purity is already enforced by " (code "deps.sx") " + boundary. Types don't duplicate it.")))
|
||||
(li (strong "Full algebraic effects.") " The effect system (Phase 7) checks static effect annotations — it does not provide algebraic effect handlers, effect polymorphism, or continuation-based effect dispatch. That door remains open for the future.")))
|
||||
|
||||
(~doc-subsection :title "Inference"
|
||||
(p "Most types are inferred, not annotated. The checker knows:")
|
||||
@@ -257,13 +262,105 @@
|
||||
|
||||
(p "Types answer: " (em "\"does this code fit together?\"") " Proofs answer: " (em "\"does this code do the right thing?\"") " Both are spec modules, both bootstrapped, both run without external tools."))
|
||||
|
||||
;; -----------------------------------------------------------------------
|
||||
;; User-defined types
|
||||
;; -----------------------------------------------------------------------
|
||||
|
||||
(~doc-section :title "User-Defined Types" :id "deftype"
|
||||
(p (code "deftype") " introduces named types — aliases, unions, records, and parameterized types. All are declaration-only, zero runtime cost, resolved at check time.")
|
||||
|
||||
(~doc-subsection :title "Type aliases"
|
||||
(~doc-code :code (highlight ";; Simple name for an existing type\n(deftype price number)\n(deftype html-string string)\n(deftype user-id (or string number))\n\n;; Use anywhere a type is expected\n(defcomp ~price-tag (&key (amount :as price) (label :as string))\n (span :class \"price\" (str label \": $\" (format-decimal amount 2))))" "lisp"))
|
||||
(p "Aliases are transparent — " (code "price") " IS " (code "number") " for all checking purposes. They exist for documentation and domain semantics."))
|
||||
|
||||
(~doc-subsection :title "Union types"
|
||||
(~doc-code :code (highlight ";; Named unions\n(deftype renderable (union string number nil component))\n(deftype key-type (union string keyword))\n(deftype falsy (union nil false))\n\n;; The checker narrows unions in branches:\n(define handle-input\n (fn ((val :as (union string number)))\n (if (string? val)\n (upper val) ;; narrowed to string — upper is valid\n (+ val 1)))) ;; narrowed to number — + is valid" "lisp"))
|
||||
(p "Union types compose with narrowing — " (code "if (string? x)") " in the then-branch narrows " (code "(union string number)") " to " (code "string") ". Same flow typing that already works for nullable."))
|
||||
|
||||
(~doc-subsection :title "Record types (typed dicts)"
|
||||
(~doc-code :code (highlight ";; Typed dict shape\n(deftype card-props\n {:title string\n :subtitle string?\n :price number\n :tags (list-of string)})\n\n;; Checker validates dict literals against shape:\n{:title \"Widget\" :price \"oops\"}\n;; ERROR: :price expects number, got string\n\n{:title \"Widget\" :price 29.99}\n;; WARNING: missing :tags (required field)\n\n;; Record types enable typed component props:\n(defcomp ~product-card (&key (props :as card-props) &rest children)\n (div :class \"card\"\n (h2 (get props :title))\n children))" "lisp"))
|
||||
(p "Records are the big win. Components pass dicts everywhere — config, props, context. A record type makes " (code "get") " on a known-shape dict return the field's type instead of " (code "any") ". This is where " (code "deftype") " pays for itself."))
|
||||
|
||||
(~doc-subsection :title "Parameterized types"
|
||||
(~doc-code :code (highlight ";; Generic over type variables\n(deftype (maybe a) (union nil a))\n(deftype (result a e) (union {:ok a} {:err e}))\n(deftype (pair a b) {:fst a :snd b})\n\n;; Used in signatures:\n(define find-user : (-> number (maybe user-record))\n (fn (id) ...))\n\n;; Checker instantiates: (maybe user-record) = (union nil user-record)\n;; So the caller must handle nil." "lisp"))
|
||||
(p "Parameterized types are substitution-based — " (code "(maybe string)") " expands to " (code "(union nil string)") " at check time. No inference of type parameters (that would require Hindley-Milner). You write " (code "(maybe string)") " explicitly, the checker substitutes and verifies.")))
|
||||
|
||||
;; -----------------------------------------------------------------------
|
||||
;; Effect system
|
||||
;; -----------------------------------------------------------------------
|
||||
|
||||
(~doc-section :title "Effect System" :id "effects"
|
||||
(p "The pragmatic middle: static effect " (em "checking") " without algebraic effect " (em "handlers") ". Functions declare what side effects they use. The checker enforces that effects don't leak across boundaries. No continuations, no runtime cost.")
|
||||
|
||||
(~doc-subsection :title "Effect declarations"
|
||||
(~doc-code :code (highlight ";; Declare named effects\n(defeffect io) ;; Database, HTTP, file system\n(defeffect dom) ;; Browser DOM manipulation\n(defeffect async) ;; Asynchronous operations\n(defeffect state) ;; Mutable state (set!, dict-set!, append!)\n\n;; Functions declare their effects in brackets\n(define fetch-user : (-> number user) [io async]\n (fn (id) (query \"SELECT * FROM users WHERE id = $1\" id)))\n\n(define toggle-class : (-> element string nil) [dom]\n (fn (el cls) (set-attr! el :class cls)))\n\n;; Pure by default — no annotation means no effects\n(define add-prices : (-> (list-of number) number)\n (fn (prices) (reduce + 0 prices)))" "lisp")))
|
||||
|
||||
(~doc-subsection :title "What it checks"
|
||||
(ol :class "list-decimal pl-5 text-stone-700 space-y-2"
|
||||
(li (strong "Pure functions can't call effectful ones.") " A function with no effect annotation calling " (code "fetch-user") " (which has " (code "[io async]") ") is an error. The IO leaked into pure code.")
|
||||
(li (strong "Components declare their effect ceiling.") " A " (code "[pure]") " component can only call pure functions. A " (code "[io]") " component can call IO but not DOM. This is the render-mode safety guarantee.")
|
||||
(li (strong "Render modes enforce effect sets.") " " (code "render-to-html") " (server) allows " (code "[io]") " but not " (code "[dom]") ". " (code "render-to-dom") " (browser) allows " (code "[dom]") " but not " (code "[io]") ". " (code "aser") " (wire format) allows " (code "[io]") " for evaluation but serializes the result.")
|
||||
(li (strong "Islands are the effect boundary.") " Server effects (" (code "io") ") can't cross into client island code. Client effects (" (code "dom") ") can't leak into server rendering. Currently this is convention — effects make it a proof.")))
|
||||
|
||||
(~doc-subsection :title "Three effect sets match three render modes"
|
||||
(div :class "overflow-x-auto rounded border border-stone-200 mb-4"
|
||||
(table :class "w-full text-left text-sm"
|
||||
(thead (tr :class "border-b border-stone-200 bg-stone-100"
|
||||
(th :class "px-3 py-2 font-medium text-stone-600" "Render mode")
|
||||
(th :class "px-3 py-2 font-medium text-stone-600" "Allowed effects")
|
||||
(th :class "px-3 py-2 font-medium text-stone-600" "Forbidden")))
|
||||
(tbody
|
||||
(tr :class "border-b border-stone-100"
|
||||
(td :class "px-3 py-2 font-mono text-sm text-violet-700" "render-to-html")
|
||||
(td :class "px-3 py-2 text-stone-700" (code "pure") ", " (code "io") ", " (code "async") ", " (code "state"))
|
||||
(td :class "px-3 py-2 text-red-600" (code "dom")))
|
||||
(tr :class "border-b border-stone-100"
|
||||
(td :class "px-3 py-2 font-mono text-sm text-violet-700" "render-to-dom")
|
||||
(td :class "px-3 py-2 text-stone-700" (code "pure") ", " (code "dom") ", " (code "state"))
|
||||
(td :class "px-3 py-2 text-red-600" (code "io") ", " (code "async")))
|
||||
(tr :class "border-b border-stone-100"
|
||||
(td :class "px-3 py-2 font-mono text-sm text-violet-700" "aser (wire)")
|
||||
(td :class "px-3 py-2 text-stone-700" (code "pure") ", " (code "io") ", " (code "async") ", " (code "state"))
|
||||
(td :class "px-3 py-2 text-red-600" (code "dom"))))))
|
||||
|
||||
(p "This is exactly the information " (code "deps.sx") " already computes — which components have IO refs. Effects promote it from a runtime classification to a static type-level property. Pure components get an ironclad guarantee: memoize, cache, SSR anywhere, serialize for client — provably safe."))
|
||||
|
||||
(~doc-subsection :title "Effect propagation"
|
||||
(~doc-code :code (highlight ";; Effects propagate through calls:\n(define fetch-prices : (-> (list-of number)) [io async]\n (fn () (query \"SELECT price FROM products\")))\n\n(define render-total : (-> element) [io async] ;; must declare, calls fetch-prices\n (fn ()\n (let ((prices (fetch-prices)))\n (span (str \"$\" (reduce + 0 prices))))))\n\n;; ERROR if you forget:\n(define render-total : (-> element) ;; no effects declared\n (fn ()\n (let ((prices (fetch-prices))) ;; ERROR: calls [io async] from pure context\n (span (str \"$\" (reduce + 0 prices))))))" "lisp"))
|
||||
(p "The checker walks call graphs and verifies that every function's declared effects are a superset of its callees' effects. This is transitive — if A calls B calls C, and C has " (code "[io]") ", then A must also declare " (code "[io]") "."))
|
||||
|
||||
(~doc-subsection :title "Gradual effects"
|
||||
(p "Like gradual types, effects are opt-in. Unannotated functions are assumed to have " (em "all") " effects — they can call anything, and anything can call them. This is safe (no false positives) but provides no guarantees. As you annotate more functions, the checker catches more violations.")
|
||||
(p "The practical sweet spot: annotate " (code "defcomp") " declarations (they're the public API) and let the checker verify that pure components don't accidentally depend on IO. Internal helpers can stay unannotated until they matter.")
|
||||
|
||||
(~doc-code :code (highlight ";; Annotated component — checker enforces purity\n(defcomp ~price-display [pure] (&key (price :as number))\n (span :class \"price\" (str \"$\" (format-decimal price 2))))\n\n;; ERROR: pure component calls IO\n(defcomp ~price-display [pure] (&key (product-id :as number))\n (let ((product (fetch-product product-id))) ;; ERROR: [io] in [pure] context\n (span :class \"price\" (str \"$\" (get product \"price\")))))" "lisp")))
|
||||
|
||||
(~doc-subsection :title "Relationship to deps.sx and boundary.sx"
|
||||
(p "Effects don't replace the existing systems — they formalize them:")
|
||||
(ul :class "list-disc pl-5 text-stone-700 space-y-1"
|
||||
(li (code "boundary.sx") " declares which primitives are IO. Effects declare which " (em "functions") " use IO.")
|
||||
(li (code "deps.sx") " computes transitive IO refs at registration time. Effects check them at type-check time — earlier, with better error messages.")
|
||||
(li "The boundary is still the source of truth for " (em "what is IO") ". Effects are the enforcement mechanism for " (em "who can use it") "."))
|
||||
(p "Long term, " (code "deps.sx") "'s IO classification can be derived from effect annotations. In the short term, both coexist — effects are checked, deps are computed, both must agree."))
|
||||
|
||||
(~doc-subsection :title "What it does NOT do"
|
||||
(ul :class "list-disc pl-5 text-stone-700 space-y-1"
|
||||
(li (strong "No algebraic effect handlers.") " You can't intercept and resume effects. This would require delimited continuations in every bootstrapper target — massive complexity for marginal UI benefit.")
|
||||
(li (strong "No effect polymorphism.") " You can't write a function generic over effects (" (code "forall e. (-> a [e] b)") "). This needs higher-kinded effect types — the same complexity as type classes.")
|
||||
(li (strong "No effect inference.") " Effects are declared, not inferred. Inference would require whole-program analysis and produce confusing error messages.")
|
||||
(li (strong "No runtime cost.") " Effects are erased after checking. The bootstrapped code has zero overhead. This is purely a static guarantee."))
|
||||
|
||||
(div :class "rounded border border-violet-200 bg-violet-50 p-4 mt-4"
|
||||
(p :class "text-violet-900 font-medium" "The door stays open.")
|
||||
(p :class "text-violet-800" "Static effect checking is the pragmatic middle — 80% of the benefit of a full effect system, 20% of the complexity. If SX ever needs algebraic handlers (e.g. for suspense, or cooperative scheduling beyond what " (code "shift") "/" (code "reset") " provides), the annotation syntax is already in place. Add handlers later without changing any existing code."))))
|
||||
|
||||
;; -----------------------------------------------------------------------
|
||||
;; Implementation
|
||||
;; -----------------------------------------------------------------------
|
||||
|
||||
(~doc-section :title "Implementation" :id "implementation"
|
||||
|
||||
(~doc-subsection :title "Phase 1: Type Registry"
|
||||
(~doc-subsection :title "Phase 1: Type Registry (done)"
|
||||
(p "Build the type registry from existing declarations.")
|
||||
(ul :class "list-disc pl-5 text-stone-700 space-y-1"
|
||||
(li "Parse " (code ":returns") " from " (code "primitives.sx") " and " (code "boundary.sx") " into a type map: " (code "primitive-name → return-type"))
|
||||
@@ -271,7 +368,7 @@
|
||||
(li "Compute component signatures from " (code "parse-comp-params") " + any type annotations")
|
||||
(li "Store in env as metadata alongside existing component/primitive objects")))
|
||||
|
||||
(~doc-subsection :title "Phase 2: Type Inference Engine"
|
||||
(~doc-subsection :title "Phase 2: Type Inference Engine (done)"
|
||||
(p "Walk AST, infer types bottom-up.")
|
||||
(ul :class "list-disc pl-5 text-stone-700 space-y-1"
|
||||
(li "Literals → concrete types")
|
||||
@@ -282,7 +379,7 @@
|
||||
(li "Lambda → " (code "(-> param-types return-type)") " from body inference")
|
||||
(li "Map/filter → propagate element types through the transform")))
|
||||
|
||||
(~doc-subsection :title "Phase 3: Type Checker"
|
||||
(~doc-subsection :title "Phase 3: Type Checker (done)"
|
||||
(p "Compare inferred types at call sites against declared types.")
|
||||
(ul :class "list-disc pl-5 text-stone-700 space-y-1"
|
||||
(li "Subtype check: " (code "number") " <: " (code "any") ", " (code "string") " <: " (code "string?") ", " (code "nil") " <: " (code "string?"))
|
||||
@@ -290,17 +387,42 @@
|
||||
(li "Warn on possible mismatch: " (code "any") " vs " (code "number") " (might work, might not)")
|
||||
(li "Component kwarg checking: required params, unknown kwargs, type mismatches")))
|
||||
|
||||
(~doc-subsection :title "Phase 4: Annotation Parsing"
|
||||
(~doc-subsection :title "Phase 4: Annotation Parsing (done)"
|
||||
(p "Extend " (code "parse-comp-params") " and " (code "sf-defcomp") " to recognize type annotations.")
|
||||
(ul :class "list-disc pl-5 text-stone-700 space-y-1"
|
||||
(li (code "(name : type)") " in param lists → extract type, store in component metadata")
|
||||
(li (code ":returns type") " in lambda/fn bodies → store as declared return type")
|
||||
(li "Backward compatible: unannotated params remain " (code "any"))))
|
||||
|
||||
(~doc-subsection :title "Phase 5: Typed Primitives"
|
||||
(~doc-subsection :title "Phase 5: Typed Primitives (done)"
|
||||
(p "Add param types to " (code "primitives.sx") " declarations.")
|
||||
(~doc-code :code (highlight ";; Current\n(define-primitive \"+\"\n :params (&rest args)\n :returns \"number\"\n :doc \"Sum all arguments.\")\n\n;; Extended\n(define-primitive \"+\"\n :params (&rest (args : number))\n :returns \"number\"\n :doc \"Sum all arguments.\")" "lisp"))
|
||||
(p "This is the biggest payoff for effort: ~80 primitives gain param types, enabling the checker to catch every mistyped primitive call across the entire codebase.")))
|
||||
(p "This is the biggest payoff for effort: ~80 primitives gain param types, enabling the checker to catch every mistyped primitive call across the entire codebase."))
|
||||
|
||||
(~doc-subsection :title "Phase 6: User-Defined Types (deftype)"
|
||||
(p "Extend the type system with named user-defined types.")
|
||||
(ul :class "list-disc pl-5 text-stone-700 space-y-1"
|
||||
(li (code "deftype") " special form — parsed by evaluator, stored in type registry")
|
||||
(li "Type aliases: " (code "(deftype price number)") " → transparent substitution")
|
||||
(li "Union types: " (code "(deftype renderable (union string number nil))") " → checked via " (code "subtype?"))
|
||||
(li "Record types: " (code "(deftype card-props {:title string :price number})") " → dict shape validation")
|
||||
(li "Parameterized types: " (code "(deftype (maybe a) (union nil a))") " → substitution-based instantiation")
|
||||
(li "Extend " (code "infer-type") " — " (code "(get d :title)") " on a known record returns the field type instead of " (code "any"))
|
||||
(li "Extend " (code "subtype?") " — resolve named types through the registry before comparing")
|
||||
(li "Test: dict literal against record shape, parameterized type instantiation, field-typed " (code "get"))))
|
||||
|
||||
(~doc-subsection :title "Phase 7: Static Effect System"
|
||||
(p "Add effect annotations and static checking. No handlers, no runtime cost.")
|
||||
(ul :class "list-disc pl-5 text-stone-700 space-y-1"
|
||||
(li (code "defeffect") " declaration form — registers named effects: " (code "io") ", " (code "dom") ", " (code "async") ", " (code "state"))
|
||||
(li "Effect annotation syntax: " (code "[io async]") " after function type or on " (code "defcomp"))
|
||||
(li "Extend " (code "check-body-walk") " — verify called functions' effects are subset of caller's declared effects")
|
||||
(li "Transitive propagation: if A calls B calls C[io], A must declare [io]")
|
||||
(li "Render mode enforcement: " (code "render-to-html") " forbids " (code "[dom]") ", " (code "render-to-dom") " forbids " (code "[io]"))
|
||||
(li "Gradual: unannotated functions assumed " (code "[all]") " — safe but unchecked. Annotations opt in.")
|
||||
(li "Integration with " (code "deps.sx") " — IO classification derived from effect annotations when available")
|
||||
(li "Integration with " (code "boundary.sx") " — IO primitives automatically carry " (code "[io]") " effect")
|
||||
(li "Test: pure calling IO = error, DOM in server render = error, island boundary enforcement"))))
|
||||
|
||||
;; -----------------------------------------------------------------------
|
||||
;; Spec module
|
||||
@@ -341,9 +463,18 @@
|
||||
(td :class "px-3 py-2 text-stone-700" "Parse a type expression from annotation syntax"))
|
||||
(tr :class "border-b border-stone-100"
|
||||
(td :class "px-3 py-2 font-mono text-sm text-violet-700" "build-type-registry")
|
||||
(td :class "px-3 py-2 text-stone-700" "Build type map from primitives.sx + boundary.sx declarations")))))
|
||||
(td :class "px-3 py-2 text-stone-700" "Build type map from primitives.sx + boundary.sx declarations"))
|
||||
(tr :class "border-b border-stone-100"
|
||||
(td :class "px-3 py-2 font-mono text-sm text-violet-700" "check-primitive-call")
|
||||
(td :class "px-3 py-2 text-stone-700" "Check a primitive call against declared param types (positional + rest)"))
|
||||
(tr :class "border-b border-stone-100"
|
||||
(td :class "px-3 py-2 font-mono text-sm text-violet-700" "resolve-type")
|
||||
(td :class "px-3 py-2 text-stone-700" "Resolve a named type through the deftype registry (Phase 6)"))
|
||||
(tr :class "border-b border-stone-100"
|
||||
(td :class "px-3 py-2 font-mono text-sm text-violet-700" "check-effects")
|
||||
(td :class "px-3 py-2 text-stone-700" "Verify effect annotations: callee effects ⊆ caller effects (Phase 7)")))))
|
||||
|
||||
(p "The checker is ~300-500 lines of SX. It's an AST walk with a type environment — structurally similar to " (code "deps.sx") " (which walks ASTs to find IO refs) and " (code "prove.sx") " (which walks ASTs to generate verification conditions). Same pattern, different question."))
|
||||
(p "The checker is a growing spec module — currently ~650 lines of SX. It's an AST walk with a type environment, structurally similar to " (code "deps.sx") " (which walks ASTs to find IO refs) and " (code "prove.sx") " (which walks ASTs to generate verification conditions). Same pattern, different question."))
|
||||
|
||||
;; -----------------------------------------------------------------------
|
||||
;; Relationships
|
||||
@@ -357,7 +488,7 @@
|
||||
(li (a :href "/plans/runtime-slicing" :class "text-violet-700 underline" "Runtime Slicing") " — types.sx is a registration-time module, not a runtime module. It doesn't ship to the client. Zero impact on bundle size."))
|
||||
|
||||
(div :class "rounded border border-amber-200 bg-amber-50 p-3 mt-2"
|
||||
(p :class "text-amber-800 text-sm" (strong "Depends on: ") "primitives.sx (return types exist), boundary.sx (IO return types exist), eval.sx (defcomp parsing). " (strong "New: ") (code "types.sx") " spec module, type annotations in " (code "parse-comp-params") "."))
|
||||
(p :class "text-amber-800 text-sm" (strong "Depends on: ") "primitives.sx (return + param types), boundary.sx (IO return types + IO classification), eval.sx (defcomp/deftype/defeffect parsing), deps.sx (IO detection — effects formalize this). " (strong "New: ") (code "types.sx") " spec module, type annotations in " (code "parse-comp-params") ", " (code "deftype") " declaration form, " (code "defeffect") " declaration form."))
|
||||
|
||||
(div :class "rounded border border-violet-200 bg-violet-50 p-4 mt-4"
|
||||
(p :class "text-violet-900 font-medium" "Why not a Haskell host?")
|
||||
|
||||
Reference in New Issue
Block a user