Source guide/effects.simd

1# Effects, Totality, and Divergence
2
3Silo tracks **what a function can do** as carefully as it tracks
4what a function produces. Every word's signature lists the side
5effects it might perform, and callers inherit those effects.
6Effects are Silo's capability system: you don't get to read a file
7unless your word, transitively, has asked for the right to read
8files.
9
10The other half of this chapter is about termination. Silo is
11**:gloss[total by default](./A1-glossary.simd#total)**: a word without
12the `+Div` effect is guaranteed to return on every input. The
13two ideas — tracked effects and proved termination — fit the same
14machinery, which is why they share a chapter.
15
16## Effect annotations
17
18A word's stack effect lists its side effects after the outputs,
19each with a `+` prefix:
20
21```silo
22:fn greet ( Str -> ) +Console
23  "Hello, " swap + "!" + print
24:end
25```
26
27`greet` pops a `Str`, pushes nothing, and declares the
28`+Console` effect. `+Console` is the capability that `.print`
29and `.input` need; without it declared, calling `print` would be
30a compile error.
31
32A word with no effect annotations is **pure**: it can't touch
33the outside world, can't diverge, can't panic. Most of the
34standard library — data transformations, arithmetic, pattern
35matching — is pure.
36
37## The effect hierarchy
38
39Effects form a tree rooted at `IO`. A sub-effect like `+Console`
40implicitly includes `+IO` — a word that has `+Console` has the
41right to do any I/O.
42
43```
44IO
45├── Console      (.print .input)
46├── FileSystem   (.read-file .write-file ...)
47├── Net
48│   ├── Http     (.http-get .http-post ...)
49│   ├── Tcp      (.tcp-connect .tcp-send ...)
50│   └── Udp
51├── Temporal     (.now .sleep)
52├── Env          (.args .get-env .exit)
53├── Executor     (.spawn .await .join-all)
54└── Random
55```
56
57Hierarchy matters because it lets you write generic code that
58asks for the smallest capability it needs. A word that just
59wants "some I/O" constrains `+IO`; a word that specifically
60needs Console constrains `+Console`. The host provides the
61leaves; code closer to the top is more portable.
62
63## Effects are capabilities
64
65A word's effect list is a **requirement** — "this word needs these
66capabilities to run" — not a viral annotation that climbs the call
67graph on its own. Silo effects have more in common with the
68borrow-checker constraints in Rust than with Haskell's `IO` monad:
69they're demands that must be discharged somewhere, and the
70compiler's job is to check that they are.
71
72A caller meets a callee's effect requirements one of two ways:
73
741. **Re-declare it.** If `a` calls `b` and `b` needs `+Console`,
75   `a` can list `+Console` in its own signature. This passes the
76   requirement on to whoever calls `a`. It might *look* viral at
77   a glance, but it isn't: `a` is explicitly saying "I also need
78   Console." Nothing is implicit.
79
80   ```silo
81   :fn shout ( Str -> ) +Console
82     ascii>upper                  # pure
83     "WARNING: " swap +            # pure
84     greet                         # greet is +Console; shout re-declares
85   :end
86   ```
87
882. **Handle it.** A caller can install a handler for the effect and
89   thereby discharge the requirement inside a scope. `:with
90   Handler :end` (covered in [the next chapter](./11-aspects.simd))
91   does this for user-defined effects and aspects. For host-provided
92   effects like `+Console` and `+FileSystem`, the "handler" is the
93   host itself — provided once when the program starts, for the
94   program's entire lifetime.
95
96Either path satisfies the compiler. Forgetting both — calling a
97`+Console` word from a word that neither declares nor handles
98`+Console` — is a compile error, pointing at the call site rather
99than at the callee.
100
101When `+Console` ends up listed on a lot of signatures, that's not
102the effect system being viral — it's the code actually needing
103Console throughout. The effect system just makes the demand
104visible in every signature where it's needed.
105
106## Polymorphic effects
107
108Sometimes a word takes a quotation and forwards whatever effects
109the quotation has. You can't write a concrete effect list when
110you don't know what effects the caller will pass in. The
111solution is an **effect variable**, written `+eff`:
112
113```silo
114:fn apply ( a [a -> b +eff] -> b ) +eff
115  .call
116:end
117```
118
119`apply` takes a value and a quotation that takes a value,
120produces one, and might have any effect row `+eff`. `apply`
121itself declares the same `+eff`, meaning "I inherit whatever my
122input quotation has." Calling `apply` with a `+Console`
123quotation makes the whole thing `+Console`; with a pure
124quotation, it's pure.
125
126This is what lets `.map`, `.filter`, `.fold`, `.for-each`, and
127every other higher-order word compose cleanly with effectful
128bodies.
129
130## Parameterised effects
131
132A few effects take type parameters. The most important is
133`Panic`, which carries the error type that can be raised:
134
135```silo
136:fn must-parse ( Str -> Int ) +(Panic Str)
137  try-parse-int
138  :match
139    | Ok n =>
140      n
141    | Err e =>
142      e panic
143  :end
144:end
145```
146
147`+(Panic Str)` means "this word may panic with a `Str` payload."
148Callers see the specific error type in the signature; if they
149want to catch the panic (rather than propagate it), they know
150exactly what it carries.
151
152## Totality and `+Div`
153
154Silo's compiler proves termination. A `:fn` without `+Div`
155must be provably total — guaranteed to return on every input.
156Two patterns the compiler recognises as total:
157
158**Structural recursion** — each recursive call takes a strict
159subterm of the input:
160
161```silo
162:fn sum ( (List Int) -> Int )
163  :match
164    | Nil       => 0
165    | Cons x xs =>
166      xs sum x +               # xs is a subterm of input
167  :end
168:end
169```
170
171**Iteration over a finite structure** — iterating a `(Vec … n)`
172or a range or any other known-finite collection:
173
174```silo
175:fn print-all ( (Vec Int | n) -> ) +Console
176  [ "{}" format print ] .for-each
177:end
178```
179
180When the compiler can't prove termination, you opt into
181divergence by adding `+Div`:
182
183```silo
184:fn collatz ( Int -> Int ) +Div
185  dup 1 = :if
186  :else
187    dup 2 mod 0 = :if 2 / collatz
188    :else 3 * 1 + collatz :end
189  :end
190:end
191```
192
193The Collatz conjecture isn't proved in general, so the compiler
194can't prove `collatz` terminates. `+Div` acknowledges that —
195callers see the effect and know this word might loop forever.
196
197Any `:loop` with a runtime break condition also requires `+Div`:
198
199```silo
200:fn find ( (Vec Int | n) Int -> (Option Int) ) +Div
201  pop-> target pop-> vec
202  0 pop-> i
203  :loop
204    i vec .len ≥ :if None :break :end
205    i vec .get .unwrap target = :if i Some :break :end
206    i 1 + pop-> i
207  :end
208:end
209```
210
211Omitting `+Div` when the compiler can't prove termination is a
212compile error. Like every other effect, `+Div` propagates — a
213caller of a `+Div` word must itself declare `+Div`.
214
215## `+Div` and `+Panic` are independent
216
217A common misconception: divergence and panic are orthogonal.
218
219- A word with `+(Panic Str)` and no `+Div` **always
220  terminates**. It either returns normally or panics, but it
221  won't loop forever. Panics are a kind of termination.
222- A word with `+Div` and no `+Panic` might loop forever but, if
223  it does return, it returns normally.
224- A word with both might loop forever or might panic.
225- A word with neither is fully total — returns on every input,
226  never panics, never loops.
227
228Most code you write should be in the last category. The
229compiler rewards keeping your effects small.
230
231## Handling and overriding effects
232
233Declaring an effect says "my code needs this capability". The
234other side of the coin is **handling** an effect — providing the
235implementation that runs when an effect operation is invoked.
236Handlers live at the boundary of your program, usually in the
237:gloss[host](./A1-glossary.simd#host) — the Rust runtime that embeds
238Silo. Console prints go to stdout via the host's `Console`
239handler; file reads go through the filesystem handler.
240
241What your Silo code *doesn't* care about — and this is the
242important bit — is **what that handler actually does**. The same
243Silo word that declares `+FileSystem` can run against:
244
245- a production host that implements the effect against the real
246  OS filesystem,
247- a sandbox host that restricts access to a single directory or
248  makes writes go into a virtual filesystem in memory,
249- a testing host that serves pre-scripted responses and records
250  every call for later assertion,
251- a replay host that serves data captured during an earlier run.
252
253None of these require any change to the Silo source. The effect
254declaration is the interface; the host chooses the implementation.
255A "sandboxed filesystem" is just a different `FileSystem` handler
256the host installs at program start.
257
258Host-provided effects like `+Console` and `+FileSystem` can't be
259overridden from inside Silo — their handlers are baked in by the
260host at startup — but the host itself can choose any handler it
261likes, including one that delegates back into user code. That's
262where sandboxing, mocking, and interception live: at the boundary
263of your program, not woven through it.
264
265Silo-defined capabilities are a different story. The
266[next chapter](./11-aspects.simd) introduces **aspects**, which
267use the `:with Handler … :end` form to install a handler for a
268lexically scoped region. Aspects are how you do the
269swap-a-handler-in-Silo pattern — testing mocks, tracing, rate
270limiting — without the host having to know anything about it.
271
272## Key points
273
274- Every word's signature lists its side effects with `+Name`;
275  pure words list none.
276- Effects are capabilities, not viral annotations. A callee's
277  effect list is a requirement the caller must either re-declare
278  in its own signature or discharge with a handler. The compiler
279  checks this at every call site.
280- Effects form a hierarchy rooted at `IO`. Leaves
281  (`+Console`, `+FileSystem`, etc.) are host-provided
282  capabilities.
283- Effect variables like `+eff` let a generic higher-order word
284  forward whatever effects its input quotation has.
285- Silo is :gloss[total](./A1-glossary.simd#total) by default. A word
286  without :gloss[`+Div`](./A1-glossary.simd#divergence) is guaranteed
287  to terminate on every input.
288- `+Div` and `+Panic` are independent. A word can terminate
289  and panic, terminate normally, loop forever, or loop forever
290  and eventually panic — and the signature tells you which.
291
292Next: [aspects](./11-aspects.simd) — cross-cutting
293capabilities that don't need `+`-annotations because their
294handler is scoped dynamically.