The Categorical Imperative

# The Categorical Imperative

There’s a particular joy to watching someone announce “I built a language” in a forum thread and then immediately try to justify their syntax with three theorems and one anecdote about how JavaScript ruined their childhood. I love that energy. It’s mess and math in equal measure. This piece is a cup of coffee with that scene — a jog through why the indie-language hobbyist ritual matters, examined through the lenses of category theory, lambda calculus, linear logic, and a few other nerdy spectacles.

## Monthly show-and-tell: a tiny agora

The ritual is predictable: weekend commit, half-baked README, and a screenshot of an REPL refusing to crash. Practically speaking, these posts are prototyping cycles made public. Theoretically, they’re social proofs — signals that someone’s still thinking about abstractions. In categorical terms, think of each project as an object and the feedback loop as morphisms: small arrows that compose into community knowledge. Not all morphisms are invertible; some feedback is brutal and unrecoverable. But composition — iterating designs, taking limits of ideas — is where novelty emerges.

## Control flow: continuations, effects, and modal logic

GOTO taught us that freedom without structure is chaos. Structured programming gave us sanity. Then exceptions, coroutines, async/await, and now algebraic effects. From a lambda-calculus standpoint, algebraic effects are continuity with control — they’re basically giving programmers first-class access to the continuation monad without the monadic ceremony. From modal logic, effects behave like modalities: “necessarily pure” vs “possibly impure.” Modal operators let you reason about when effects flow; effect systems are, in a sense, type-level modal logic.

Why the buzz? Algebraic effects promise to separate invocation from handling the way functors separate shape from content. But they complicate type inference and API design. Category theory tempers enthusiasm: functors and monads tidy up certain patterns, but adding more structure (effects-as-objects, handlers-as-morphisms) makes the category richer — and harder to reason about for everyday users. It’s the difference between owning an artisan screwdriver and a damn Swiss army knife. Both useful; one is easier to lose.

## Effect systems: promises, pragmatics, and proof theory

Effect systems wear two hats. As programmers’ annotations they’re documentation and a light-weight contract; as type systems they bootstrap optimizations and proofs. Proof theory reminds us: adding expressive tracking (like dependent types or fine-grained effects) increases the cost of proof obligations. If your team is shipping web features, every extra annotation is a tax. But in library-land, effect annotations are like axioms — they give you the ability to prove invariants about concurrency, resource usage, and testability.

So, pragmatic rule: use effect systems where their theorems buy you something clear (noninterference, deterministic scheduling, easier testing). Otherwise, they’re lovely academic jewelry.

## Pryzma and the joy of bricolage

Projects like Pryzma exist to try shit in public. They’re laboratories where syntactic whimsy meets type-theoretic curiosity. These experiments are valuable not because they immediately dethrone mainstream languages but because they propose new morphisms for the community category. They teach us which compositions fail and which survive.

Ship early. Document goals. Expect to be roasted. If you did something genuinely new, congrats; if you reinvented an existing abstraction with prettier syntax, congrats anyway — you learned the landscape.

## Memory without GC: linear logic, separation logic, and the last-use dream

The fantasy of inserting free() at the precise last-use point is seductive. Linear logic is the formal spirit here: resources that must be used exactly once. In concurrency, session types say similar things about protocols: use, then close. But real programs are full of aliases, callbacks, callbacks of callbacks, and polymorphic dispatch that hides uses behind interfaces.

Domain theory and separation logic give us tools: abstract garbage collection as a fixed-point over program states; reason about disjointness and ownership. Ownership types and region-based memory can approximate last-use frees in constrained settings. But whole-program last-use analysis collides with dynamic linking and modular deployment. In short: if you constrain the problem (embedded systems, safe subsets), you can approach the ideal. For general-purpose computing, GC and borrow-checkers are pragmatic compromises that make the proof obligations tractable.

## Formal glue: category theory, order, and semantics

Want to translate rhetoric into rigor? Category theory offers a lingua franca. Monads for effects, adjunctions for free/forgetful constructions, functorial semantics for DSLs. Order theory and domain theory provide the partial orders we need to model recursion and termination. Proof theory and model theory give you the theorems to say whether an optimization preserves semantics.

But here’s the human bit: formal elegance doesn’t equal ergonomic success. Haskell is mathematically tidy; TypeScript is pragmatically ubiquitous. Sometimes the best thing a language can offer is boring predictability and a story executives can understand.

## How to participate without getting rekt

– Prototype fast. A toy interpreter teaches more than thought experiments.
– State tradeoffs. Explain ergonomics, interop, and performance goals.
– Benchmark and test. Demonstrate where your idea helps.
– Solicit feedback early. The community can be bitchy and brilliant.
– Don’t fetishize novelty. Many innovations are recombinations.

These are the homely heuristics that turn aesthetic preferences into engineering wins.

## Parting thought

Indie language design sits at a crossroads of ego and epistemology: a field where theorems meet taste. Math disciplines give us tools to reason about these systems, but the ultimate arbiter is human friction — how a team writes, reads, and maintains code. So here’s my categorical imperative for language designers: make something that provably helps a class of real programs, and make it easy enough that people will actually use it.

And now I’ll leave you with a question I enjoy posing at conferences and coffee shops: which compromises would you make — more formal guarantees or more developer comfort — if you had to pick one constraint for the next decade of your language’s life?