rose-ash/plans/linear-on-sx.md

Linear-on-SX: resource model

Linear and affine type systems track consumption — values used at most once, references handed off rather than copied. Currently SX has no notion of "this value cannot be duplicated"; adding it changes the value space fundamentally. Granule (Eyers, Gaboardi, Orchard et al.) is the cleanest research target — graded modal types extending HM with linearity. Alternative: a Linear Haskell fragment (Bernardy et al.). Both are more principled than Rust's borrow checker for the chiseling purpose, since they isolate linearity from the borrow/lifetime story.

The chisel: consumption. Asks the substrate to articulate its aliasing and ownership semantics. SX values are currently fully duplicable — every let-binding can copy, every closure capture is implicit, every reference is shareable. Linear types force the substrate to honour at-most-one-use as a first-class property.

What this exposes about the substrate:

• Whether SX can statically track at-most-once consumption without runtime overhead (compile-time check).
• Whether closures can be linearly typed — capturing a linear value should make the closure itself linear.
• Whether substrate primitives (make-ref, set-ref!, deref-ref) can be exposed with linear interfaces alongside the duplicable defaults.
• Whether handlers (effects) compose with linearity — does using a capability consume it?
• Whether the macro system handles linear binding hygienically.

End-state goal: Granule core — linear arrows A ⊸ B, unrestricted modality !A (Box A in some treatments), graded modalities □_n A (n-uses), linear pattern matching, integration with HM. Standard library demonstrating linear file handles, linear channels, linear references. Practical relevance: artdag — content-addressed values, IPFS pins, file handles, network sockets all want "use exactly once" or "use exactly N times" semantics.

Ground rules

• Scope: lib/linear/** and plans/linear-on-sx.md only. Substrate gaps → sx-improvements.md.
• Consumes from lib/guest/: core/lex, core/pratt, core/ast, core/match, typed/hm.sx (extended with linear type variables and modalities).
• Will propose a new sub-layer lib/guest/linear/ — linearity tracking infrastructure, modality bookkeeping, separation logic primitives. Second consumer: a Rust-fragment, a Linear Haskell fragment, ATS-on-SX, or a future capability-secure language.
• Branch: loops/linear. Standard worktree pattern.

Architecture sketch

Linear source text (Granule-flavoured: HM + linear arrows + modalities)
    │
    ▼
lib/linear/parser.sx       — Haskell-ish syntax with -o for linear arrow,
    │                        ![A] for unrestricted, [n]A for graded
    ▼
lib/linear/elaborate.sx    — surface → core: explicit modality coercions,
    │                        let-binding linearity inference
    ▼
lib/linear/check.sx        — bidirectional type checker tracking BOTH
    │                        types AND usage counts per binding
    ▼
lib/linear/typed/          — extends lib/guest/typed/hm.sx with:
    │                        linear arrow types, modality types, grade algebra
    ▼
lib/linear/runtime.sx      — runtime is plain SX (linearity erased after check)
                             standard library: linear refs, linear channels,
                             linear file handles

Semantic mappings

Linear construct	SX mapping
A -o B	linear arrow type {:type :arrow :linear true :domain A :codomain B}
A -> B	unrestricted arrow (sugar for !A -o B)
!A	unrestricted (duplicable) modality on type A
[n] A	graded: usable exactly n times
let !x = e in body	unbox an unrestricted value (allow duplication)
let x = e in body	linear binding — x must appear exactly once in body
case x of !y -> body	match-and-unbox
dup x in body	duplicate (only on unrestricted values; type error otherwise)
share x	turn a linear value into unrestricted (under specific guarantees)

The key novel substrate property: every binding has a grade — how many times it's used. The type checker computes grades, complains if usage doesn't match the declared grade. Runtime is plain SX — linearity is erased after type checking.

Roadmap

Phase 1 — Parser

• Granule-flavoured syntax: HM core plus linear arrows, modality annotations.
• Reuse lib/guest/lex, lib/guest/pratt.
• Tests in lib/linear/tests/parse.sx.

Phase 2 — Type system: linear vs unrestricted base

• Two type "worlds": linear (A -o B) and unrestricted (!A, A -> B).
• Type checker tracks usage count per variable.
• Reject programs that use a linear variable zero or twice times in a context.
• Tests: programs that violate linearity get rejected with clear errors.

Phase 3 — Linear functions + linear pattern matching

• Linear lambda: \x -> body — x consumed exactly once in body.
• Linear pair (x, y) — both components consumed if pair is consumed.
• let (x, y) = pair in body — destructure (consume) pair, both x and y are linear.
• Tests: linear list manipulation, linear pair swapping.

Phase 4 — Modalities (! and graded)

• !A — unrestricted modality, can be duplicated/discarded freely.
• Promotion: [e] lifts linear e : A to unrestricted !A (only if e uses only unrestricted values).
• Graded modalities [n] A for n-times use; algebra over grades (semiring with +, *).
• Tests: graded programs (use-twice, use-three-times patterns).

Phase 5 — Linear references + standard library

• LinearRef A — write-once or in-place-update with type-tracked transitions.
• LinearChannel A — send-and-consume.
• LinearFile — open returns linear handle, read/write consume + return new handle, close consumes terminally.
• Tests: linear file API usage, channel send/receive, in-place-mutation patterns.

Phase 6 — Effects + linearity

• When linear values flow through perform/handlers, the handler must consume them linearly too.
• Capabilities as linear values: Cap consumed when capability is exercised.
• Tests: handler that takes a linear capability and uses it once.

Phase 7 — Borrowing (lightweight)

• borrow x as y in body — temporarily allow non-consuming use of a linear value.
• Borrow ends at end of body; original x still linear after.
• No lifetime regions à la Rust — just lexical borrow scopes.
• Tests: read a linear file handle without consuming it.

Phase 8 — Integration with artdag idioms

• Demo: artdag-style pipeline where each effect node holds a linear CID, transforms it, returns a new linear CID.
• Demo: IPFS pin operations as linear capability transitions.
• Tests: end-to-end pipeline that compiles iff linearity is honoured.

Phase 9 — Propose lib/guest/linear/

• Extract linearity-tracking type-checker infrastructure.
• Extract grade algebra primitives (semiring operations).
• Extract modality coercion machinery.
• Wait for second consumer before extracting (Rust-fragment is the natural pair).

lib/guest feedback loop

Consumes: core/lex, core/pratt, core/ast, core/match, typed/hm.sx (extended).

Stresses substrate: value duplicability assumptions throughout — does the SX evaluator implicitly duplicate values anywhere (caching? memoisation? structural sharing)? Those become bugs under linearity.

May propose: lib/guest/linear/ sub-layer — usage tracking (grades), modality coercions, linear arrows. Also might motivate lib/guest/typed/hm.sx to grow a "type-system-extension" interface so linearity, refinement types, and effect rows can all extend HM uniformly.

What it teaches: whether SX's value model is paradigm-agnostic or quietly assumes duplicability. If the substrate has any "values are duplicable for free" assumptions baked in, linearity surfaces them. If linearity composes cleanly, it's strong evidence for substrate paradigm-neutrality.

Practical artdag connection

Artdag (the federated content-addressed media processing engine) has natural linearity:

• A CID is conceptually unique; pinning + unpinning has a linear-resource shape.
• File handles, network sockets, IPFS connections all want at-most-once-close semantics.
• L1↔L2 token transfer (scoped JWT) has at-most-once-use semantics.

If linear-on-sx works, artdag could rewrite its resource-handling layer in linear-typed code, getting compile-time guarantees of resource discipline. That's a real-world payoff that justifies more than the "chisel" framing.

References

• Bernardy et al., "Linear Haskell: Practical Linearity in a Higher-Order Polymorphic Language" (POPL 2018).
• Orchard, Liepelt, Eades, "Quantitative program reasoning with graded modal types" (ICFP 2019) — Granule.
• Wadler, "Linear types can change the world!" (1990) — foundational.
• Pierce (TAPL), Ch. 14 — linear and affine types.
• Granule source: https://github.com/granule-project/granule

Progress log

(awaiting Phase 1 — depends on lib/guest/typed/hm.sx maturity)

Blockers

(none yet — main risk is type-checker complexity for graded modalities)