docs/spec/decisions.md · jibb

git.iko.soy/jibb

jibb/docs/spec/decisions.md

192 lines 34 kB history raw

1# Jibb decisions

3Oct 29, 2026 · @iko

5The choices behind the Language tab, made on 2026-10-23; a later date marks a revision.

7## Decisions

9This copy is the spec (review question 42). Synced says whether the doc's Decisions tab has the row as written here. A row decided by 2026-10-29 or undated was in the doc when `spec/` was copied from it on 2026-10-30, and is unchanged. A row decided on or after 2026-10-31 is only here. A row of 2026-10-30 says Check: the copy had that day's answers to the 12 grammar questions, but other rows of that day were added or edited here afterwards ([docs/README.md](../README.md#the-spec)), and nobody has compared them with the doc yet.

11Rows dated 2026-11-03 are Montelot's decisions on the [syntax review](../reviews/2026-11-02-syntax-review.md): S1 with its step 1, S2, S4 to S7, S11 to S13 and S15. S1 step 1 is decided but not built yet; the checker core that review question 5 asks for will build it.

14| --- | --- | --- | --- |

15| Syntax | Hoon's runes as keywords, and its literals; wide forms only for `\|=` and `$-`; changes take one or more record items, as `m(draft="x")`, so `m()` is an error; an item may name a wing through record fields, as `m(open.cart=x)`, every value is computed from the original record, and two items that name the same field, or one inside the other, are an error; `.` reads fields, imports and prelude groups; no name may shadow another | Decided 2026-11-03 | No |

16| Literals | Exactly Hoon's, including `%$` as a term literal and pattern: a bare decimal is a `@ud`, so `^- @dr 30` is an error and a duration is written `~s30`; `1000` is an error, `~2026.2.31` is `~2026.3.3`, and years BC and sub-second groups are dates; `print-date`'s minute form is not a literal | Decided 2026-11-03 | No |

19| Strings | Hoon's escapes: `\\`, `\"`, `\{`, and `\` with two lowercase hex digits; a string and each `{…}` close on the line they open; `::` in a string is text | Decided 2026-10-30 | Check |

20| Spacing | The parser still accepts one or more spaces between items and spaces after an opener, before a closer and at line end; faces, puns and typed path segments take no spaces. Canonical output indents by two spaces, uses two spaces after `++`/`+$` and their names, after `|=`, `^-`, `?-`, `~&` and `|$`, and between a rune's inline children, one space between ordinary items, and no inner bracket padding or automatic alignment | Decided 2026-11-04 | No |

31| Unions | No `$?`: a `+$` with its cases on the lines below is a union, so every union written in Jibb has a name; one case is just that mold; a mold that isn't a union counts as a union of one case for tags and `\|=%tag`; a generic's `\|$` comes right after the `+$`'s name; tags anywhere; constructor heads and case disjointness compare literal noun values regardless of spelling, so `%$`, `%.y` and `~` are equal and overlapping cases are errors; cases differ as nouns, with `?` treated as the two atoms `%.y` and `%.n`, disjoint from cells and overlapping constants 0 and 1, and `!!` or any cell with an empty position disjoint from every case; a tag literal or `~` waits for its union, and an unresolved one is an error | Decided 2026-10-31 | No |

33| Printed type constraints | Print an atom constraint as `$-([A A] A) where A is an atom`, an arithmetic atom constraint as `where A is an atom other than ?`, and a gate-free constraint as `$-([A A] ?) where A contains no gates`; separate multiple clauses with commas, as `where A is an atom, B contains no gates` | Decided 2026-10-31 | No |

35| Equality and negation | The gates `eq` and `not`, with Hoon's bitwise `not` exposed as `not.bit`; `eq`'s arguments and map and set keys contain no gates, even nested; the checker infers and generalizes that constraint; union matching never inspects a gate to distinguish cases | Decided 2026-10-30 | Check |

37| Inference | Hindley–Milner with aura variables; `@` is any atom, a specific atom fits `@` and a more specific aura fits an ancestor in its Hoon aura family, but each reverse needs a check, and repeated atom-constrained capitals give the same type; a decimal is a `@ud`, which fits `@u`, `@` and `*` but no other aura, except where its `++` is generic over its aura; distinct specific auras remain distinct; faces are part of record types, and an unnamed position can take a face but two different faces don't unify; a capital that meets a faced position binds only the type under the face, so `$-([A A] ?)` takes a gate with named parameters (not built yet); principal types | Decided 2026-11-03 | No |

38| Effects | The library unions `cmd` and `sub`; `raw-poke`, `ask` and `qath` are transparent types defined in the internal prelude and re-exported normally; derived gates and `pure` also construct requests; islands read agents only by watching; replies get full state, and diffs take a fold; timers carry the time; `%who` gives the owner's `@p`; nacks reach replies as text | Decided 2026-11-01 | No |

39| Poke representation | The source-backed private internal prelude module defines `raw-poke`, and the public prelude re-exports it as an ordinary transparent type. A store's local `poke` action remains an ordinary mold; derived helpers produce the runtime envelope | Decided 2026-11-01 | No |

40| Agent APIs | `/ui/api/<agent>.jibb` with `+$ poke` and `+$ paths`, over the agent's mark types; a case is a name, a path and a type, with `(facts full diff …)` for diffs, told apart by mark; an optional scry path, for pages; an island may watch a request only when the checker proves it is watchable, so a separate scry path or unknown watchability is an error; typed segments by aura | Decided 2026-10-31 | No |

42| Derived gates | API files and stores give a generic `poke` command helper taking an action and reply, and a checked request per path or store state; clashing names are errors, including a derived name that clashes with an import face | Decided 2026-11-01 | No |

43| Hoon types | A fixed translation table; `map`, `set`, `qeu`, `jar`, `jug` by name; `mop` as `(mop K V)`, read with `on`; imported `$%`, `$?` and `$^` cases must differ as nouns, and records with duplicate field names are errors where used; unused molds skipped | Decided 2026-10-30 | Check |

45| Unface | The explicit type-directed operation `unface` removes every face from its argument's type, through cells, a gate's sample and product, and containers' arguments; unions and recursive molds go by name and are kept whole; like `proj`, it is reserved and not a value; it leaves nothing behind at run time | Decided 2026-11-03 | No |

46| Record projection | The explicit type-directed operation `proj` takes a record and uses its expected result type to select its fields; no projection is inserted automatically. `proj` is reserved and cannot be defined or imported under that name. The result has exactly the fields declared by its type | Decided 2026-10-31 | No |

47| Layout | Indentation; juxtaposed calls; a bracket open at line end takes one item per line, with no closer; a block of deeper lines belongs to the line above, so a call never continues onto a deeper line; a body's final line may hand the rest of the body, at its depth, to a tall `\|=`, `^-` or `~&` that ends it, and a `?-` that begins it may take its arms at its depth | Decided 2026-11-03 | No |

48| Elements | Ordinary gates; containers take attribute lists; `stack` switches at `wide`; `el` adds attributes and wins; headings 1 to 6; `form` sends on Enter, the innermost when nested; `image` from an application path, sized from the file, or a sized URL; no focus control for now | Decided 2026-10-29 | Yes |

53| Type variables | A capital, then lowercase letters and digits, as `A` or `Msg`, printed by the name they were written with; generalized per `++`; a capital in a local `++` shares the enclosing `++`'s variable of that name if the enclosing `++` also uses it; otherwise it is introduced and generalized locally; a different type takes a different capital; a body cannot force distinct capitals to be equal, so a shared type uses the same capital; one used where an atom is required gains an inferred atom constraint, and cannot be fixed to a more specific type in its body | Decided 2026-11-03 | No |

54| Partial type annotations | `_` may appear wherever a mold may appear and marks that part of the type for inference; a hole inferred as a named type variable is resolved; an unconstrained hole is an error, and a named mold or value definition must determine its own holes without constraints from later uses | Decided 2026-10-31 | No |

60| Binding patterns | In `?-` arms; the last position binds the rest; cells of patterns nest; a bare name is an error where a case the pattern can match has there a tag the name spells, as `stop` for `%stop` | Decided 2026-11-03 | No |

61| Text | Strings are written only as `"…"` and are always cords; tapes come from `trip`; `{…}` prints by aura, a bare `@` as `@ud`, and an atom whose aura its `++` is generic over is an error; `print-date` prints Urbit-style to the minute in the theme's zone, from jibb-dev's zone table; numbers keep Hoon's form | Decided 2026-10-30 | Check |

62| Auras | Specific auras stay distinct; `@` is any atom, a more specific aura fits an ancestor in its Hoon aura family one way, with the reverse requiring a check, and shared atom-constrained type variables preserve the same aura | Decided 2026-10-30 | Check |

64| Crashes | As in Hoon; an island keeps its model and shows the standard notice; a failing page, or one rendering a control outside an island, gets Jibb's error page; no render limit, so an endless render stalls the ship | Decided 2026-10-29 | Yes |

68| Core language | A small untyped core language between the checker and both backends: Nock's operations on nouns plus a lambda calculus with names; one sample per call; s-expressions as its text form; a reference interpreter in Hoon; three rules in its tab still proposed | Decided | Yes |

70| Page loading | `load` maps route parameters, `~` for none, to one `ask` or `pure`; pages render per request from a fresh scry of the path, or of its case's scry path; nothing is watched or kept | Decided 2026-10-29 | Yes |

80| Shared state | Stores: browser agents written like API files, with `state`, a local `+$ poke` action mold and `(store init update)`; derived gates provide the generic `poke` command helper and state requests; one per page | Decided 2026-11-01 | No |

86| Theme | A prelude mold with every token required: spaces, five tones with `normal` and `background`, language, zone, `wide`, and an optional static font; optional values such as dark tones use explicit backtick unit syntax; 4.5:1 contrast enforced | Decided 2026-11-01 | No |

88| Links | All text escaped; in-app links are application paths, as `%/blog/(slug)`, with no query or fragment, checked at compile time against routes and static files; paths and unchecked `https`, `mailto` and `tel` URLs and root-relative cords such as `"/apps/groups"` have separate declarations; `link-unsafe`, `image-unsafe` and `go-unsafe` are the unchecked forms; both navigation declarations produce `[%go url=@t]`, with `go` converting the path to a cord including the app's base path; other cords render as text; a CSP on every page | Decided 2026-10-30 | Check |

90| Prelude | Hoon's standard library regrouped: all names from the listed sections except explicitly excluded groups, including all of 3g, with Hoon's `tone` exposed as `tone.hoon` and Hoon's 1c `step` as `step.hoon`; arithmetic over aura variables, units, lists, maps, sets, queues, ordered maps, function helpers, text, atom printing, a zoned date printer, time and data molds; folds take a start; jetted functions have working Jibb implementations, whose shapes the compiler recognizes to use the Hoon versions, and may take gates; private helpers and low-level primitives live in a separate internal module imported without exposing them, with public foundational gates implemented in Jibb on those primitives; `clap` takes two units of the same type and a combining gate over that type; no signed or float gates, or parser gates outside 3g except `slav` and `slaw`; signed or float auras are errors | Decided 2026-10-30 | Check |

91| `like` | The `(like A)` mold remains available; the value gate `like` maps the product of an existing `(like A)` with a gate `$-(A B)`, preserving the position and remaining input, and returns `(like B)` | Decided 2026-10-31 | No |

93| Hosting | One thin host agent on `%jibb` binds, caches and serves every Jibb desk; each desk vendors jibb-dev, names its base path in docket's `site+`, and builds and renders with its own copy through fixed entry points; install `%jibb` first; app agents stay plain Hoon; pokes only from the ship | Decided 2026-10-29 | Yes |

96| Static files | Under `/ui/static/`, committed, at hashed immutable URLs; referenced by application path, so a missing file fails to compile, and images are sized from the file; no large media, since Clay keeps every version and the cache ignores `Range` | Decided 2026-10-29 | Yes |

102| Formatter | Canonical 80-column code, counting indentation; comments and unbreakable forms may overflow. Inline what fits, otherwise break outer constructs recursively. Format short gates inline, tall `\|=` wherever valid and wide `\|=(...)` only in operand positions; remove redundant inline grouping, otherwise preserve surface forms, literal spellings and import order. Multiline bodies begin below definition/gate/arm headers, except a short cast goes below its owner and a multiline cast ends the owner's line with its expression below. Multiline calls use `(head` with one argument per deeper line; other openers stand alone and open forms have no closers. `?-` starts its own line; inline arm bodies follow exactly two spaces. Single-mold `+$` definitions stay inline and union cases go below. Output has no empty blank lines or forced separators: each internal blank run becomes one bare `::` at the surrounding indent, edge runs disappear, existing bare `::` lines remain, and comment-text lines count as declarations rather than whitespace and do not suppress conversion. Comments use canonical indentation, exactly two spaces precede a trailing `::`, the gap after `::` and the text are preserved, and comments are never wrapped or relocated; comments prevent joining their containing construct. Leave no trailing spaces; a nonempty file has exactly one final newline. This supersedes the earlier rule that documentation examples change only when necessary | Decided 2026-11-04 | No |

104

105## Settled milestone 2 questions

106

107Kept only in this copy. These were open questions in [open-questions.md](../open-questions.md) until @iko settled them; the rows above record each choice, and the questions keep their numbers there, so references to them stay valid. Questions 3 and 32 are still open there.

108

109On 2026-10-30, @iko adopted gate-free `eq` arguments and map and set keys, treating gates as opaque when distinguishing union cases, and rejecting a non-gate value that depends on itself even through a gate. The checker infers and generalizes the gate-free constraint. @iko also said jetted prelude functions may take gates.

110

111**1. Settled: how the prelude identifies jetted functions.** On 2026-10-30, @iko said the prelude functions have working Jibb implementations, and the compiler recognizes their shapes and uses the Hoon versions so jets can fire.

112

113**2. Settled: how the prelude keeps helpers private.** On 2026-10-30, @iko chose a separate internal prelude module imported by the prelude, without exposing the imported helpers.

114

115**4. Settled: a capital in a local `++`.** On 2026-10-30, @iko said it shares the enclosing `++`'s variable of that name if the enclosing `++` also uses it; otherwise the local `++` introduces and generalizes its own variable. For example, `++ inner |= y=A y` shares `A` with an enclosing gate whose sample is `x=A`, but generalizes its own `A` if the enclosing `++` does not use `A`. A different type uses a different capital. The Grammar and Decisions record this alongside the earlier aura rules.

116

117**5. Settled: cells of no items or one.** On 2026-10-30, @iko said a single-item cell is the value and `[]` is an error. The theme's `dark=[tones=[…]]`, a record of one field, must still check.

118

119**6. Settled: a change with no items.** On 2026-10-30, @iko said `m()` is an error. The parser still accepts it; the checker needs to reject it and add a golden case.

120

121**7. Settled: the doc's blocks that aren't whole modules.** On 2026-10-30, @iko agreed to check each in its intended context: the `cmd` and `sub` definitions as prelude source, the Core language tab's `update` inside the todo island, and the Grammar's imports example against fixture files.

122

123**8. Settled: tuples and records.** On 2026-10-30, @iko agreed that an unnamed position can unify with a faced position and take its face; two different explicit faces still conflict. The Grammar and Decisions record this rule.

124

125**9. Settled: values where `*` is expected.** On 2026-10-30, @iko said `*` is the noun type, not a type variable; generic positions use proper type variables. A value already known to be `@ud` can be passed where `*` is expected. The `each` and `table` signatures use `key=K`.

126

127**10. Settled: navigation commands.** On 2026-10-30, @iko chose separate declarations for application paths and unchecked cords, with `link-unsafe`, `image-unsafe` and `go-unsafe` for the unchecked forms. `image-unsafe` takes a sized URL record. Both navigation declarations produce `[%go url=@t]`; `go` converts the application path to a cord including the app's base path.

128

129**11. Settled: stores and derived gates.** On 2026-11-01, @iko said a store's local `+$ poke` is an ordinary action mold and the runtime envelope is `raw-poke`; a derived name clashes with an import face; and an island watching a request whose case has a separate `scry=` path has a type error. The todo API's request is renamed `todo-by-id` so it does not clash with `/- todo`. The checker must account for the fact that a store's kind is determined by the type of `main`.

130

131**12. Settled: how to print a union without a name.** On 2026-10-30, @iko said to print its cases separated by spaces, as `%approve %deny`. This is print-only, not Jibb syntax.

132

133**13. Settled: how to print type constraints.** On 2026-10-30, @iko chose `$-([A A] A) where A is an atom` for an atom constraint and `$-([A A] ?) where A contains no gates` for a gate-free constraint. Multiple clauses are comma-separated, as `where A is an atom, B contains no gates`.

134

135**14. Settled: how the prelude implements foundational operations.** On 2026-10-30, @iko chose private low-level primitives in the internal prelude module, with the public foundational gates implemented in Jibb on top of them.

136

137**15. Settled: unrestricted atoms and shared auras.** On 2026-10-30, @iko said `@` means any atom, independently at each occurrence, so Hoon `dime` and `pint` keep their bare-`@` fields. A specific atom such as `@ud` fits where `@` is expected; an `@` value needs a check to fit `@ud`. Shared atom types use one capital, with the atom constraint inferred from its body, as for `add` taking `[A A]` and returning `A`.

138

139**16. Settled: loobeans in union disjointness.** On 2026-10-30, @iko said `?` counts as its two atoms, `%.y` and `%.n`: it is disjoint from any cell and overlaps the constants 0 and 1.

140

141**17. Settled: empty cases in union disjointness.** On 2026-10-30, @iko said `!!` is disjoint from every case. A cell containing an empty position at any depth is itself empty and is also disjoint from every case.

142

143**18. Settled: the value gate `like`.** On 2026-10-31, @iko chose a gate `(like convert result)` that maps the product of an existing `(like A)` result with `convert=$-(A B)`, yielding `(like B)` while preserving its position and remaining input. An absent result stays absent. The `(like A)` mold remains available in the separate mold namespace. Hoon's wet `+like` instead builds a gate that constructs a result from an input noun; the chosen Jibb value gate is an adaptation of that behavior.

144

145**19. Settled: Hoon aura families and `step.hoon`.** On 2026-10-30, @iko chose `step.hoon` for Hoon 1c `step`, avoiding a clash with the Grammar example's `step`, and chose one-way widening across Hoon aura families: for example, `@ud` and `@ux` fit `@u`, and `@tD` fits `@t`. The reverse needs a check. The `step.hoon` group representation is not implemented yet.

146

147**20. Settled: the type of `clap`.** On 2026-10-30, @iko chose one shared value type for both units and the combining gate. If either unit is absent, `clap` returns the other; if both are present, it applies the gate to their values and wraps the result.

148

149**21. Settled: duplicate faces in imported Hoon records.** On 2026-10-30, @iko chose to reject an imported Hoon record with duplicate field names where its type is used. Hoon permits `[a=@ud a=@t]` and picks the first `a`; Jibb rejects it.

150

151**22. Settled: overlapping imported `$%` and `$?` cases.** On 2026-10-30, @iko confirmed that the general union disjointness rule rejects imported `$%` and `$?` cases that overlap as nouns where the type is used, as it does for `$^`. The importer rejects recognizable overlaps and fails closed when it cannot verify them.

152

153**23. Settled: converging explicit capitals.** On 2026-10-30, @iko chose that a body cannot force two separately written capitals to be equal. For `++ repeated |= x=(choice A A) x`, `++ f |= x=(choice A B) (repeated x)` is an error; use `A` in both positions when the type must be shared. This also applies across local captures and within generic mold applications.

154

155**24. Settled: how the internal prelude provides `raw-poke`.** On 2026-11-01, @iko chose to define `raw-poke` in the source-backed private internal prelude module and re-export it through the public prelude as an ordinary transparent type. Ordinary modules can construct and inspect its values, while derived API/store `poke` helpers return commands. This settles `raw-poke`; it does not decide the representation of `ask` or `qath`.

156

157**25. Settled: how the prelude provides `ask` and `qath`.** On 2026-10-31, @iko chose ordinary transparent types defined in the internal prelude and re-exported normally, as for `raw-poke`. Callers may construct and inspect their values.

158

159**26. Settled: the `step` example's `at` binder.** On 2026-10-31, @iko chose to rename the `describe` pattern binder to `sent-at`, keeping Hoon's `at` in the prelude and the no-shadowing rule.

160

161**27. Settled: duplicate fields in a Jibb-written record.** On 2026-10-31, @iko chose to reject duplicate field names, as for imported Hoon records.

162

163**28. Settled: arithmetic on loobeans.** On 2026-10-31, @iko chose to reject loobean operands for arithmetic. Comparison may still accept loobeans and returns `?`. The checker needs to retain this constraint through inference, generalization and instantiation before it exports `add` or `dec`.

164

165**29. Settled: printing the arithmetic atom constraint.** On 2026-10-31, @iko chose `where A is an atom other than ?` for a generic arithmetic type whose atom variable excludes loobeans.

166

167**30. Settled: a hole inferred as a generic variable.** On 2026-10-31, @iko said a hole resolved to an explicitly written type variable counts as inferred: in `++ id |= x=A ^- _ x`, the result hole is `A`. Named molds must determine their own holes without constraints from later uses; an unconstrained hole is an error.

168

169**31. Settled: uses of a value with a hole.** On 2026-10-31, @iko said a value definition must determine its own holes; another definition's use cannot fix an otherwise unresolved hole. For example, `++ id |= x=_ x` remains an error even if a later definition calls `id` with a cord.

170

171**33. Settled: watching a request with unknown provenance.** On 2026-10-31, @iko said an island may watch a request only if the checker proves it watchable at compile time. An unknown request, including one built or passed through a gate without sufficient evidence, is rejected rather than deferred to a runtime check.

172

173**34. Settled: constructors and equal noun literals.** On 2026-10-31, @iko said expressions with the same runtime representation count as equal, and cases that cannot be distinguished at runtime are rejected at compile time. Thus `|=%$` matches a case headed by `%$`, `%.y` or `~`: each is the noun 0. Cases with equal heads and overlapping payloads cannot coexist in a union.

174

175Review question 25, when to build `eq` and the gate-free constraint, is settled: @iko's commit 0858191 adds `eq` and infers the constraint.

176

177## Checked against the kernel

178

179- **Eyre's cache** is keyed by the exact request target, query included, one entry per URL, and counts against the ship's memory ([eyre.hoon](https://github.com/urbit/urbit/blob/50c7f5239610fc72263df7aa99b4d171cfe9d408/pkg/arvo/sys/vane/eyre.hoon#L922-L927), [vere #626](https://github.com/urbit/vere/issues/626)). An auth-flagged entry gives anyone but the owner a bare 403 before any agent sees the request ([vere http.c](https://github.com/urbit/vere/blob/510d5b7fe4ea81343f2364db081ce61f1d2c72d3/pkg/vere/io/http.c#L1141-L1146)), and entries outlive their agent ([gall.hoon](https://github.com/urbit/urbit/blob/50c7f5239610fc72263df7aa99b4d171cfe9d408/pkg/arvo/sys/vane/gall.hoon#L1382-L1409)).

180

181## Build order

182

183Each step ends in something usable.

184

1851. **Parser and mark**: the layout pass, runes, literals and patterns; the `%jibb` mark.

1862. **Types and prelude**: inference with aura variables and tag resolution; `/-`, `/%` and `/=`; the Hoon type table; the core prelude gates.

1873. **Core language**: lowering from the checked tree, the text form, the reference interpreter in Hoon, and the Nock backend.

1884. **Host and static pages**: the shared host running vendored compilers, routing and application paths, layout and theme, static files, the Eyre asset cache and the owner check. First release.

1895. **Published pages**: `load`, requests and per-request rendering.

1906. **Islands**: first a benchmark that runs the same programs as JavaScript and in a Nock interpreter, to pick the browser backend; then that backend, `cmd` and `sub`, keyed diffing, the shared library, stores, the crash notice and URL subscriptions.

1917. **Tooling**: tests, formatter, tree-sitter grammar and differential tests.

1928. **Polish**: shared island modules across pages, holes, size.