Chapter 9 Effects, Totality, and Divergence

Silo tracks what a function can do as carefully as it tracks what a function produces. Every word's signature lists the side effects it might perform, and callers inherit those effects. Effects are Silo's capability system: you don't get to read a file unless your word, transitively, has asked for the right to read files.

The other half of this chapter is about termination. Silo is total by default: a word without the +Div effect is guaranteed to return on every input. The two ideas — tracked effects and proved termination — fit the same machinery, which is why they share a chapter.

Effect annotations

A word's stack effect lists its side effects after the outputs, each with a + prefix:

:fn greet ( Str -> ) +Console
  "Hello, " swap + "!" + print
:end

greet pops a Str, pushes nothing, and declares the +Console effect. +Console is the capability that .print and .input need; without it declared, calling print would be a compile error.

A word with no effect annotations is pure: it can't touch the outside world, can't diverge, can't panic. Most of the standard library — data transformations, arithmetic, pattern matching — is pure.

The effect hierarchy

Effects form a tree rooted at IO. A sub-effect like +Console implicitly includes +IO — a word that has +Console has the right to do any I/O.

IO
├── Console      (.print .input)
├── FileSystem   (.read-file .write-file ...)
├── Net
│   ├── Http     (.http-get .http-post ...)
│   ├── Tcp      (.tcp-connect .tcp-send ...)
│   └── Udp
├── Temporal     (.now .sleep)
├── Env          (.args .get-env .exit)
├── Executor     (.spawn .await .join-all)
└── Random

Hierarchy matters because it lets you write generic code that asks for the smallest capability it needs. A word that just wants "some I/O" constrains +IO; a word that specifically needs Console constrains +Console. The host provides the leaves; code closer to the top is more portable.

Effects are capabilities

A word's effect list is a requirement — "this word needs these capabilities to run" — not a viral annotation that climbs the call graph on its own. Silo effects have more in common with the borrow-checker constraints in Rust than with Haskell's IO monad: they're demands that must be discharged somewhere, and the compiler's job is to check that they are.

A caller meets a callee's effect requirements one of two ways:

1. Re-declare it. If a calls b and b needs +Console, a can list +Console in its own signature. This passes the requirement on to whoever calls a. It might look viral at a glance, but it isn't: a is explicitly saying "I also need Console." Nothing is implicit.

   :fn shout ( Str -> ) +Console
     ascii>upper                  # pure
     "WARNING: " swap +            # pure
     greet                         # greet is +Console; shout re-declares
   :end

2. Handle it. A caller can install a handler for the effect and thereby discharge the requirement inside a scope. :with Handler :end (covered in the next chapter) does this for user-defined effects and aspects. For host-provided effects like +Console and +FileSystem, the "handler" is the host itself — provided once when the program starts, for the program's entire lifetime.

Either path satisfies the compiler. Forgetting both — calling a +Console word from a word that neither declares nor handles +Console — is a compile error, pointing at the call site rather than at the callee.

When +Console ends up listed on a lot of signatures, that's not the effect system being viral — it's the code actually needing Console throughout. The effect system just makes the demand visible in every signature where it's needed.

Polymorphic effects

Sometimes a word takes a quotation and forwards whatever effects the quotation has. You can't write a concrete effect list when you don't know what effects the caller will pass in. The solution is an effect variable, written +eff:

:fn apply ( a [a -> b +eff] -> b ) +eff
  .call
:end

apply takes a value and a quotation that takes a value, produces one, and might have any effect row +eff. apply itself declares the same +eff, meaning "I inherit whatever my input quotation has." Calling apply with a +Console quotation makes the whole thing +Console; with a pure quotation, it's pure.

This is what lets .map, .filter, .fold, .for-each, and every other higher-order word compose cleanly with effectful bodies.

Parameterised effects

A few effects take type parameters. The most important is Panic, which carries the error type that can be raised:

:fn must-parse ( Str -> Int ) +(Panic Str)
  try-parse-int
  :match
    | Ok n =>
      n
    | Err e =>
      e panic
  :end
:end

+(Panic Str) means "this word may panic with a Str payload." Callers see the specific error type in the signature; if they want to catch the panic (rather than propagate it), they know exactly what it carries.

Totality and +Div

Silo's compiler proves termination. A :fn without +Div must be provably total — guaranteed to return on every input. Two patterns the compiler recognises as total:

Structural recursion — each recursive call takes a strict subterm of the input:

:fn sum ( (List Int) -> Int )
  :match
    | Nil       => 0
    | Cons x xs =>
      xs sum x +               # xs is a subterm of input
  :end
:end

Iteration over a finite structure — iterating a (Vec … n) or a range or any other known-finite collection:

:fn print-all ( (Vec Int | n) -> ) +Console
  [ "{}" format print ] .for-each
:end

When the compiler can't prove termination, you opt into divergence by adding +Div:

:fn collatz ( Int -> Int ) +Div
  dup 1 = :if
  :else
    dup 2 mod 0 = :if 2 / collatz
    :else 3 * 1 + collatz :end
  :end
:end

The Collatz conjecture isn't proved in general, so the compiler can't prove collatz terminates. +Div acknowledges that — callers see the effect and know this word might loop forever.

Any :loop with a runtime break condition also requires +Div:

:fn find ( (Vec Int | n) Int -> (Option Int) ) +Div
  pop-> target pop-> vec
  0 pop-> i
  :loop
    i vec .len ≥ :if None :break :end
    i vec .get .unwrap target = :if i Some :break :end
    i 1 + pop-> i
  :end
:end

Omitting +Div when the compiler can't prove termination is a compile error. Like every other effect, +Div propagates — a caller of a +Div word must itself declare +Div.

+Div and +Panic are independent

A common misconception: divergence and panic are orthogonal.

• A word with +(Panic Str) and no +Div always terminates. It either returns normally or panics, but it won't loop forever. Panics are a kind of termination.
• A word with +Div and no +Panic might loop forever but, if it does return, it returns normally.
• A word with both might loop forever or might panic.
• A word with neither is fully total — returns on every input, never panics, never loops.

Most code you write should be in the last category. The compiler rewards keeping your effects small.

Handling and overriding effects

Declaring an effect says "my code needs this capability". The other side of the coin is handling an effect — providing the implementation that runs when an effect operation is invoked. Handlers live at the boundary of your program, usually in the host — the Rust runtime that embeds Silo. Console prints go to stdout via the host's Console handler; file reads go through the filesystem handler.

What your Silo code doesn't care about — and this is the important bit — is what that handler actually does. The same Silo word that declares +FileSystem can run against:

• a production host that implements the effect against the real OS filesystem,
• a sandbox host that restricts access to a single directory or makes writes go into a virtual filesystem in memory,
• a testing host that serves pre-scripted responses and records every call for later assertion,
• a replay host that serves data captured during an earlier run.

None of these require any change to the Silo source. The effect declaration is the interface; the host chooses the implementation. A "sandboxed filesystem" is just a different FileSystem handler the host installs at program start.

Host-provided effects like +Console and +FileSystem can't be overridden from inside Silo — their handlers are baked in by the host at startup — but the host itself can choose any handler it likes, including one that delegates back into user code. That's where sandboxing, mocking, and interception live: at the boundary of your program, not woven through it.

Silo-defined capabilities are a different story. The next chapter introduces aspects, which use the :with Handler … :end form to install a handler for a lexically scoped region. Aspects are how you do the swap-a-handler-in-Silo pattern — testing mocks, tracing, rate limiting — without the host having to know anything about it.

Key points

• Every word's signature lists its side effects with +Name; pure words list none.
• Effects are capabilities, not viral annotations. A callee's effect list is a requirement the caller must either re-declare in its own signature or discharge with a handler. The compiler checks this at every call site.
• Effects form a hierarchy rooted at IO. Leaves (+Console, +FileSystem, etc.) are host-provided capabilities.
• Effect variables like +eff let a generic higher-order word forward whatever effects its input quotation has.
• Silo is total by default. A word without +Div is guaranteed to terminate on every input.
• +Div and +Panic are independent. A word can terminate and panic, terminate normally, loop forever, or loop forever and eventually panic — and the signature tells you which.

Next: aspects — cross-cutting capabilities that don't need +-annotations because their handler is scoped dynamically.