The Stack Is Already Linear: What a Borrow-Checked Concatenative Language Has to Solve

Taylor’s slap-000 introduces Slap, a concatenative language that adds borrow-checking semantics to the stack model. Most work on memory-safe systems languages reaches for either garbage collection or something Rust-adjacent. Slap reaches for a third option: linear types applied to a functional concatenative foundation. The design space here is narrower than it first appears, but the problems it exposes are genuinely instructive.

What Concatenative Languages Do Differently

In a concatenative language, a program is a sequence of words, and composition is just juxtaposition. Where most languages pass arguments to functions by name, concatenative languages route everything through an implicit stack. The word dup copies the top element; swap exchanges the top two; + pops two numbers and pushes their sum. A definition like : square dup * ; reads as “push a copy of the top, multiply them together.” No parameter names, no binding sites, just transformations on shared implicit state.

This model comes from Forth (Charles Moore, 1970), which used it for embedded systems programming. Joy (Manfred von Thun, 2001) reformulated concatenative programming in purely functional terms: every word is a function from Stack to Stack, and two programs concatenated are their composition. Factor brought that model into the practical world with a native-code compiler, a rich standard library, and stack-effect declarations like ( x y -- z ) that the type checker verifies statically. Kitten, Jon Purdy’s research language, pushed further into static safety with row-polymorphic types.

Row polymorphism is the key type-theoretic move for concatenative languages. The type of dup is not (Int -- Int Int) but (R... A -- R... A A), where R... is a row variable representing whatever else happens to be on the stack. This lets the type system reason about stack effects compositionally without forcing a fixed stack depth. Every word gets a row-polymorphic type; the checker unifies row variables to verify that adjacent words produce and consume compatible stacks. That is the baseline any modern typed concatenative language builds on.

The Natural Fit With Ownership

Stack consumption is already a move. When a word takes the top-of-stack as input, that value is gone. The word owns it. This is not a designed-in feature of concatenative languages; it is just what the operational semantics describe. Push a value, pass it to a word, the word consumes it. If you want to use the value again, you must explicitly dup it first.

That operational description maps cleanly onto Rust’s ownership model. Passing a value to a function moves it. Using a value twice requires either a Copy type or an explicit clone. The stack makes this visible in a way that variable-based languages obscure: you can see exactly how many times each value is referenced, because references are stack slots and stack slots are explicit.

This connection is not new. Henry Baker made it in 1992 in “Linear Logic and Permutation Stacks — The Forth Shall Be First”, connecting Girard’s linear logic to Forth’s stack discipline. Baker’s argument was that a Forth extended with linear types would give you deterministic memory reclamation without garbage collection: every allocation is owned, every free is implicit in the consumption of the owning word, and the type system prevents double-free and use-after-free by construction.

Where It Gets Complicated

The simple cases work cleanly. The hard cases cluster around three combinators: dup, dip, and quotations.

dup is the copying combinator. In a linear type system, dup is legal only on types that permit copying, what Rust calls Copy types. For heap-allocated owned values, dup would produce a second owner, breaking the ownership invariant. A borrow-checked concatenative language needs either to restrict dup to copyable types or to make dup produce a borrow rather than an owned copy. The second option requires the type system to track the lifetime of the borrow relative to the owned value it refers to.

dip is the combinator that applies a quotation to a value below the stack top. [f] dip temporarily hides the top value, applies f to what is underneath, then restores the top. From an ownership perspective, dip is a scoped operation: the hidden value is inaccessible to f, which provides natural containment. If f moves out of the hidden value’s memory region, that is a lifetime violation the borrow checker must catch. The dip scope is a natural place to enforce this; it functions as a borrow scope with explicit begin and end points.

Quotations are the most complex case. In Joy-style concatenative languages, a quotation like [dup *] is a deferred computation, a first-class value that can be passed around and called later. When a quotation captures values from the surrounding stack, it creates a closure, and closures are where lifetime management gets difficult. If the quotation captures a borrow of a stack value, that borrow cannot outlive the stack frame that owns the value. If the quotation is stored in a heap-allocated structure and called later, the borrow is invalid. This is the same problem Rust solves with lifetime annotations on closures, but in a concatenative language the captures are implicit in the stack state at quotation creation time, which makes them harder to reason about syntactically.

Row Polymorphism Extended With Lifetimes

The natural extension of row-polymorphic stack types to handle borrows would annotate borrowed values in stack positions with lifetime parameters, something like (R... &'a T -- R... &'a T Bool). The row variable R... would need to carry lifetime constraints: if any slot in R... has lifetime 'a, the word cannot be called in a context where 'a would escape the current frame.

This is non-trivial to infer. Rust pushes lifetime annotations to the programmer because the inference problem is undecidable in general. A concatenative language with implicit stack threading might recover more from inference, since the data flow is more constrained, but the interaction between row variables and lifetime constraints is still an open research problem. Kitten’s design has been exploring linear types for years without fully resolving quotation capture semantics.

The Clean Precedent

Clean, developed at Radboud University from the late 1980s, solved a related problem in a non-concatenative setting with uniqueness types. A unique value in Clean is a value with exactly one live reference. The type system tracks uniqueness through function calls; if a function takes a unique argument, it must consume it or return it as unique. This lets Clean update arrays in place, manage I/O state, and handle resources without garbage collection for those values, while keeping a GC for non-unique values.

Uniqueness types are a form of affine types: a unique value can be dropped or consumed but not duplicated. That maps onto the stack model in roughly the same way the stack’s “consume on use” semantics already do. Clean’s solution required uniqueness annotations throughout the type system, which adds syntactic overhead but makes the semantics precise. A stack language has the advantage that the stack position is already an implicit slot with a clear owner; the annotation burden might be lower in practice.

Idris 2’s Quantitative Type Theory goes further, giving every variable a multiplicity (0 for erased, 1 for linear, omega for unrestricted) in a dependently typed setting. The direction of travel across the field is toward more precise resource tracking, and the tools are increasingly mature.

Why This Combination Is Worth Pursuing

The combination Slap is exploring, functional concatenative style with deterministic memory management via borrow checking, would produce something that does not currently exist in well-engineered form: a GC-free systems language where the primary programming model is function composition and stack transformation rather than object mutation. Factor gets you most of the programming model but uses garbage collection. Rust gives you memory safety but pushes toward imperative, variable-based style. A borrow-checked concatenative language would sit at a distinct point in the trade-off space, one potentially well-suited to embedded targets or latency-sensitive code where GC pauses matter and the expressiveness of point-free composition is valuable.

Whether the type-theoretic problems are solvable in a way that produces a usable language is the real open question. Baker’s 1992 paper pointed the direction; thirty years of work on linear types, row polymorphism, and ownership semantics has refined the tools considerably. The question Slap is asking is whether those tools are now sharp enough to cut.