Future Directions: Parsing as a Nondeterministic Effect

The previous post walked through a complete Spine program. The series has covered the language as it is being built: facts, effects, processes, space, resources, universes, verification, and compilation.

This post looks ahead — at a design direction that has not yet been fully realized, but that follows naturally from the ideas already in place.

It starts with a simple observation: parsing is an effect.

The Conventional View of Parsing

In most languages, the parser is a fixed, separate phase. The grammar is defined once — in a BNF specification, a parser combinator library, or a hand-written recursive descent parser. The grammar does not change based on what has been parsed so far. It does not depend on what facts exist in the system or what universe the program operates in.

This separation is practical but limiting. Consider:

• A domain-specific notation where the valid syntax depends on which entities have been declared earlier in the file.
• A configuration language where the available keywords change based on the loaded modules.
• A protocol description where the valid next message depends on the current state of the conversation.

In each case, the grammar is not static. What you can say depends on what you have said — or on the context in which you are speaking.

Traditional parsers handle this through ad-hoc mechanisms: symbol tables consulted during parsing, context-sensitive hacks grafted onto context-free grammars, or multiple parsing passes. These work, but they are bolted on. The grammar formalism does not account for them.

Parsing as an Effect

Spine already has a precise notion of effects: structured operations with preconditions and postconditions that transform the state of the world.

Parsing fits this description exactly:

• The state is the input stream plus whatever has been recognized so far.
• A parse step consumes input (a resource) and produces structure (a fact).
• The precondition determines what is valid to parse next — which depends on the current state.
• The postcondition describes what the world looks like after a successful parse: new facts exist, new entities are in scope, new syntax may have become available.

Once parsing is an effect, it participates in the same machinery as every other effect in Spine: it has typed pre- and postconditions, it is subject to resource tracking, and it can be verified.

Nondeterminism

Parsing is inherently nondeterministic. When the parser encounters an input token, there may be multiple valid ways to proceed. A traditional parser resolves this through lookahead, backtracking, or grammar restrictions (LL, LR, PEG priority). The nondeterminism is managed — squeezed into deterministic control flow.

Spine takes a different view. Nondeterminism is not a problem to be eliminated. It is a nondeterministic effect.

A nondeterministic effect is one that can produce multiple possible outcomes. The system explores all of them — or, more precisely, the system represents all of them as a structured space of possibilities.

This is not new territory for Spine. We have already seen:

• Probabilistic effects — where outcomes have associated probabilities.
• Nondeterministic choice in processes — where a process may take one of several paths.
• Verification of nondeterministic systems — where tools like PRISM and mCRL2 analyze all possible behaviors.

Modeling parsing as a nondeterministic effect means the parser does not need to commit to a single interpretation prematurely. It explores the space of valid parses, constrained by the current state, and produces all valid readings.

What This Gives Us: Dynamic Grammar

When parsing is a nondeterministic effect with state-dependent preconditions, the grammar becomes dynamic.

Not dynamic in the sense of being unpredictable or chaotic. Dynamic in the sense that the set of valid productions — the things that can be said — evolves as the parse progresses. Each successfully parsed construct can introduce new facts, and those facts can enable new syntax.

Consider a concrete scenario:

1. The parser encounters a universe declaration. After parsing it, the universe's vocabulary — its fact types, its effect signatures — becomes available as syntax.
2. The parser encounters an entity declaration. After parsing it, that entity name becomes a valid token in subsequent expressions.
3. The parser encounters a capability definition. After parsing it, rules that reference that capability become syntactically valid.

At each step, the postcondition of one parse effect becomes the precondition of the next. The grammar grows as the program is read.

This is not a special mechanism. It is a consequence of treating parsing as an effect in a system that already tracks state, resources, and preconditions.

How It Works Structurally

At a technical level, a Spine parser built this way is a composition of nondeterministic effectful operations:

• Each production rule is an effect: it consumes input tokens (linear resources), checks preconditions against the current parse state, and produces parsed structure as new facts.
• Alternatives are nondeterministic choices: when multiple productions could apply, the parser branches. Each branch has its own state and its own continuation.
• Sequencing is effect composition: parsing A then B means the postcondition of A feeds the precondition of B.
• The grammar is the set of effects whose preconditions are currently satisfiable. As facts accumulate, more effects become available — the grammar expands.

Because all of this lives within Spine's effect system, the compiler represents the parser as a composition of effects — with sequential composition for sequencing, alternatives for independent parse branches, and recursion for recursive grammars.

Resource Tracking in Parsing

One detail deserves emphasis: input tokens are linear resources.

A token, once consumed, is gone. It cannot be consumed again by a different branch. This is enforced by the same QTT resource discipline that tracks ownership in the asset system.

This has a practical consequence: the parser cannot accidentally read the same input twice, and it cannot silently drop input. Resource tracking makes the parser's relationship with its input stream explicit and verifiable.

Backtracking, in this model, is not rewinding an input pointer. It is exploring an alternative branch that consumes the same tokens differently — a nondeterministic choice, not an imperative undo.

Universes and Grammar

The connection to universes is natural.

If the grammar depends on the current state, and the state includes which universe is active, then the grammar is universe-dependent. Different universes may enable different syntax:

• A General universe provides the base grammar — core Spine syntax.
• A domain-specific universe extends it — adding notation for that domain's concepts.
• An embedded DSL is just a universe that introduces its own vocabulary and grammar rules as effects.

There is no separate macro system, no preprocessor, no template language. Domain-specific syntax is a consequence of domain-specific universes and the dynamic grammar that falls out of treating parsing as an effect.

Verification of Parsers

Because the parser is built from the same effects as the rest of the system, it is subject to the same verification pipeline.

• Z3 can check that the grammar is unambiguous under a given set of preconditions — that for any input, there is at most one valid parse.
• TLA+ can check that the parser always makes progress — that no input causes it to loop indefinitely.
• mCRL2 can verify properties of the parser as a process — determinism, deadlock-freedom, confluence.

These are not hypothetical applications. They follow directly from the fact that the parser is an effectful process, and effectful processes are what the verification pipeline is designed to analyze.

Self-Hosting Implications

There is a recursive consequence worth noting.

If Spine's parser is itself a Spine program — a composition of nondeterministic effects — then Spine's syntax is defined in the same language it parses. The grammar is not an external specification. It is a Spine program that describes how to read Spine programs.

This is the natural endpoint of treating parsing as an effect: the language becomes self-describing. Extensions to the language are extensions to the parser, written in the language itself, verified by the same pipeline, compiled by the same backend.

What Remains

This is a future direction, not a shipped feature. The pieces are in place — nondeterministic effects, state-dependent preconditions, linear resource tracking, universe-polymorphic contexts — but the specific design of the parsing effect interface, the resolution strategy for ambiguity, and the performance characteristics of nondeterministic parse exploration are active areas of work.

What we can say now is this: the decision to model effects as structured, verifiable, composable operations — made early in Spine's design — opens a door that most languages never approach. Parsing does not need to be a special case. It does not need its own formalism. It is just another effect, subject to the same rules as everything else.

And when parsing is just another effect, the boundary between the language and its syntax dissolves. What you can say becomes part of what the program defines.