a8dd227 · jibb · git.iko.soy

git.iko.soy/jibb

on master help sign in

Record the rules for gates generic over auras

a8dd227Claude1 day ago

docs/README.md+1−1

compare with master

unifiedsplit

@@ -14,7 +14,7 @@ Jibb's spec is a design doc by @iko, [Jibb — an Elm-architecture UI language f

15## The spec

17−`spec/` began as a snapshot of the doc taken on 2026-10-30, after @iko's answers to the 12 grammar questions that day. It has since been edited to record the decision to drop `$?`; the Claude document still needs those edits. Each file corresponds to one tab:

17+`spec/` began as a snapshot of the doc taken on 2026-10-30, after @iko's answers to the 12 grammar questions that day. It has since been edited to record the decision to drop `$?`; the Claude document still needs those edits. It also has the doc's rules of the same day for gates generic over auras. Each file corresponds to one tab:

19| File | Tab |

20| --- | --- |

docs/open-questions.md+3−3

@@ -19,12 +19,12 @@ The three core-language rules are in [spec/core-language.md](spec/core-language.

20## Questions milestone 2 raises

22−Found while writing [prompts/milestone-2.md](prompts/milestone-2.md) and checking it against the doc's examples. The type checker needs an answer to each; none has been put to @iko yet.

22+Found while writing [prompts/milestone-2.md](prompts/milestone-2.md) and checking it against the doc's examples. The type checker needs an answer to each. @iko settled most of question 4 on 2026-10-30; the others haven't been put to @iko yet.

24−1. **How the prelude declares natives.** The overview's Prelude section says the prelude is "written in Jibb and vendored as `/lib/jibb/prelude`", and that "Only the prelude declares natives, Jibb's jets, and private helpers". The Core language tab gives each native "a Jibb type, a Hoon gate in `/lib/jibb` … and a JavaScript function in the runtime". The Grammar has no syntax for declaring a native, so how does the prelude say that `add` is a native of type `$-([@ @] @)`?

24+1. **How the prelude declares natives.** The overview's Prelude section says the prelude is "written in Jibb and vendored as `/lib/jibb/prelude`", and that "Only the prelude declares natives, Jibb's jets, and private helpers". The Core language tab gives each native "a Jibb type, a Hoon gate in `/lib/jibb` … and a JavaScript function in the runtime". The Grammar has no syntax for declaring a native, so how does the prelude say that `add` is a native of type `$-([@ @] @)`? The rules of 2026-10-30 make it sharper: outside a `+$` each bare `@` is its own aura variable, and a capital becomes an aura variable only by meeting an atom in a body, which a native doesn't have. So the declaration needs some way to say that `add`'s three atoms share one aura.

252. **How the prelude marks its private names.** Modules: "Everything is exported and read through the import's face, as `card.card`. Only the prelude has private names." The Grammar has no syntax for privacy either.

263. **What the prelude holds, and how much of it milestone 2 writes.** The Prelude table names groups and examples, "such as `(get.by m k)`", and for the data molds says "and the rest", so which names and types make up the prelude? Its list probably belongs in the doc. The plan's milestone 2 builds "the prelude's types", while the Decisions tab's Build order puts "the core prelude gates" in the same step. And which list gates are natives depends on the plan's first open question, "natives that take gates". The prelude must name every union its elements and attributes take, such as spaces, roles and tones; no module may use those names, since no name may shadow the prelude's.

27−4. **Aura and type variables in a gate's molds.** Molds: "`add` takes `[@ @]` and returns `@`, all one aura" and "A bare `@` in a `+$` is one aura variable per module, `@ud` if unfixed." Is every bare `@` in one `++`'s molds, its samples and casts, the same aura variable, as in `add`'s type, or is each `@` its own, and is it generalized per `++` as type variables are? With it: must a capital stay general, so that `++ f |= x=A (add x 1)` is an error, or may its body fix it? Is a capital in a local `++` the enclosing `++`'s? And does a number's `@ud` default apply to an aura variable its `++` would generalize, which would make `++ inc |= n=@ (add n 1)` a `$-(@ud @ud)`?

27+4. **A capital in a local `++`.** @iko settled the rest of this question on 2026-10-30, in the Grammar's Molds and Literals by context and the Decisions rows Inference, Type variables and Text: outside a `+$` each bare `@` is its own aura variable, generalized per `++` if nothing fixes it; a capital that meets an atom becomes an aura variable, and nothing more specific; a number takes `@ud` only if its `++` isn't generic over its aura; and printing an atom whose aura its `++` is generic over is an error. Still open: is a capital in a local `++` the enclosing `++`'s, so that a local helper can name its parent's types, or a fresh one? The proposed reading is the enclosing one's.

285. **Cells of no items or one.** The parser takes `[]` and `[a]` as tuples, as the EBNF's `"[" { item } "]"` allows, and leaves them to the checker. The Literals section may already answer it: "Every literal reads exactly as Hoon reads it", and its table lists Cell. Hoon reads `[a]` as `a` and rejects `[]`. The proposed reading is Hoon's. Whatever the answer, the theme's `dark=[tones=[…]]`, a record of one field, must still check.

296. **A change with no items.** `m()` parses as a change with no edits, as `wing "(" { item } ")"` allows. Is it an error?

307. **The doc's blocks that aren't whole modules.** The plan's "Done when" for milestone 2 says "the doc's examples typecheck, except those written as errors". Three `jibb` blocks need context to check. The overview's `cmd` and `sub` molds (`doc-overview-01-cmd-sub`) are what the Effects decision calls "the library unions", so in a module of their own they would shadow the prelude's. The Core language tab's `update` (`doc-core-02-update`) is a part of the todo list island. And the Grammar's imports (`doc-grammar-01-imports`) import `/sur/todo.hoon` and `/ui/components/card`, which the doc doesn't show, and the `%todo-action` mark, which the overview shows but which imports `/sur/todo.hoon` itself. The proposed reading is to check each in its context: the first as prelude source, the second inside the island, the third against fixture files.

docs/prompts/milestone-2.md+6−6

@@ -53,7 +53,7 @@ And from the plan's Risks:

53 1. how the prelude declares natives;

54 2. how it marks private names;

55 3. what the prelude holds, and whether milestone 2 writes "the prelude's types", as the plan says, or "the core prelude gates", as the Decisions tab's Build order says;

56− 4. aura and type variables in a gate's molds;

56+ 4. whether a capital in a local `++` is the enclosing `++`'s (the rest of that question was settled on 2026-10-30);

57 5. `[]` and `[a]`;

58 6. `m()`;

59 7. how to check the doc's blocks that aren't whole modules;

@@ -72,9 +72,9 @@ The rules are scattered across the tabs. This is a map of them, not a replacemen

73**Types and inference** (Grammar: Molds, Modules, Runes, Expressions; Decisions: Inference, Type variables, Sample names, Inline gates)

74- Hindley–Milner with aura variables: "every expression has a principal type, and there is no subtyping".

75−- "`@` is an atom whose aura isn't known yet, fixed by what it meets": `add` takes `[@ @]` and returns `@`, all one aura. "Different auras never unify." "A bare `@` in a `+$` is one aura variable per module, `@ud` if unfixed."

75+- "`@` is an atom whose aura isn't known yet, fixed by what it meets": `add` takes `[@ @]` and returns `@`, all one aura. "Different auras never unify." "A bare `@` in a `+$` is one aura variable per module, `@ud` if unfixed." Elsewhere, "as in a gate's sample or a cast, each bare `@` is its own aura variable, generalized per `++` if nothing fixes it; atoms that must share an aura take one capital".

76- Faces are part of record types: `[a=@ b=@]` and `[x=@ y=@]` don't unify. Whether a tuple meets a record is open question 8.

77−- Type variables are capitals, "generalized per `++`". Names "may refer to each other in any order", so infer `++` definitions in dependency order, a group of mutually recursive ones together.

77+- Type variables are capitals, "generalized per `++`". "A type variable that meets an atom becomes an aura variable", so `++ clamp |= [lo=A hi=A n=A]`, calling `gth` and `max`, works on any one aura; "It can become nothing more specific: a body that makes `A` a `@ud` or a list is an error." Whether a capital in a local `++` is the enclosing one's is open question 4. Names "may refer to each other in any order", so infer `++` definitions in dependency order, a group of mutually recursive ones together.

78- "Gates may call themselves and their siblings; other values can't refer to themselves, so `++ title (trim title)` is an error." Molds may be recursive, and "recursive molds go by name and module".

79- A sample's mold may be left out: every bare name in a sample binds, at any depth, as in `|=(p title.p)` "when the call fixes the type", `|= [a=@ b]` and `|=(m ~)`.

80- Generic molds: `+$ result |$ [V E]` with cases below, applied as `(result V E)`; `|$` goes right after a `+$`'s name, and the prelude's `cmd` and `sub` use `|$ [M]`.

@@ -87,8 +87,8 @@ The rules are scattered across the tabs. This is a map of them, not a replacemen

87- `|=%typed` is a case's constructor: "against `$-(@t M)` it is `|=(t [%typed t])`, requiring `M` to have a case `[%typed @t]`. It works for cases tagged at their head; a bare tag is always a value."

88- "A constrained variable, and any it mentions, doesn't generalize; it stays open until something in the module fixes it. An island's `main` fixes its messages." A constraint still open when the module is checked "is an error asking for a `^-`; the checker never guesses".

89- "Wing access, changes and `?-` on a type not yet known wait the same way." Patterns don't: they're checked against the subject's type.

90−- Number and cell literals each "takes a default when its `++` is checked": a number `@ud`, a cell a tuple. A cell can also become a record or, where a list is expected, a cons.

90+- Number and cell literals each "takes a default when its `++` is checked": a number `@ud`, a cell a tuple. But "A number takes `@ud` only if nothing fixes its aura and its `++` isn't generic over it", so `++ inc |= n=A (add n 1)` stays generic: unlike a tag's, a number's variable doesn't stop its `++` from generalizing. A cell can also become a record or, where a list is expected, a cons.

91−- In `{…}`, atoms print by aura, a bare `@` as `@ud`; `@t`, `@ta`, `@tas` and tapes splice as text; "any other cell is an error asking for a printer". String literals are always cords.

91+- In `{…}`, atoms print by aura, a bare `@` as `@ud`; `@t`, `@ta`, `@tas` and tapes splice as text; "any other cell is an error asking for a printer". "Printers are picked when compiling", so an atom whose aura its `++` is generic over "is an error asking for an aura", in `{…}` and in a `(…)` segment of an application path. String literals are always cords.

93**Unions** (Grammar: Molds, Runes; Decisions: Unions)

94- Every union written in Jibb is a named `+$` with its cases below. One case is just that mold; a mold that isn't a union counts as a union of one case for tags and `|=%tag`. Imported types can contain unnamed unions.

@@ -130,7 +130,7 @@ The rules are scattered across the tabs. This is a map of them, not a replacemen

130- Element signatures are in the Layout and styling table; what `link`, `image` and `go` take is open question 10. "The same attribute twice in a literal list is an error."

131

132**Errors**

133−- Each one the Grammar tab describes needs a golden case with its message. A start on the list: an aura mismatch; mismatched faces; "msg has no case %submitt"; an unresolved tag, as the Grammar's `add-button` ("nothing fixes the union of %add"); an open constraint at the end of a module; a `|=%tag` whose union has no such case tagged at its head; a union whose cases overlap; a missing `?-` case, named; an arm that earlier arms cover; a value that refers to itself; a shadowed name, including a prelude or imported one; a cell in `{…}` with no printer; `~[text "hi"]`, where the checker suggests `~[(text "hi")]`; clashing derived names; an import cycle; from an import, a signed or float aura, a core, gate or vase, or a `$^` whose cases don't differ as nouns, each where used; a `(facts …)` outside an API file's `paths`; a gate in island data or a model, naming the field; a repeated attribute in a literal list. Read the Grammar tab, and the other tabs' mentions of "error" and "the checker", and make the list complete.

133+- Each one the Grammar tab describes needs a golden case with its message. A start on the list: an aura mismatch; mismatched faces; "msg has no case %submitt"; an unresolved tag, as the Grammar's `add-button` ("nothing fixes the union of %add"); an open constraint at the end of a module; a `|=%tag` whose union has no such case tagged at its head; a union whose cases overlap; a missing `?-` case, named; an arm that earlier arms cover; a value that refers to itself; a shadowed name, including a prelude or imported one; a cell in `{…}` with no printer; an atom of a generic aura in `{…}` or a path's `(…)`; a capital that a body makes a `@ud` or a list; `~[text "hi"]`, where the checker suggests `~[(text "hi")]`; clashing derived names; an import cycle; from an import, a signed or float aura, a core, gate or vase, or a `$^` whose cases don't differ as nouns, each where used; a `(facts …)` outside an API file's `paths`; a gate in island data or a model, naming the field; a repeated attribute in a literal list. Read the Grammar tab, and the other tabs' mentions of "error" and "the checker", and make the list complete.

134- For a `+$` whose cases overlap or do not fit, suggest that a record or tuple leaves its `[` open on the `+$` line. `+$ pt` above `@t` and `[@ud @ud]` is a valid union.

135- "Each error names both conflicting sites, with excerpts." Today's `error` is `[file line col msg]`, a start only; spans keep each node's end so that a type error can underline both sites.

136- Messages name things in the doc's words and quote the code they're about in backticks, as milestone 1's do. Their wording is fixed by the golden tests once written.

docs/spec/decisions.md+3−3

@@ -26,7 +26,7 @@ The choices behind the Language tab, made on 2026-10-23; a later date marks a re

26| Branching | `?-` only, loobeans included; exhaustive, with explicit catch-alls; covered arms are errors; failures say `!!` | Decided 2026-10-29 |

27| Equality and negation | The gates `eq` and `not` | Decided |

28| Special rules | No built-ins; type-directed rules are welcome, each listed in the Grammar tab | Decided 2026-10-29 |

29−| Inference | Hindley–Milner with aura variables; a bare `@` in a `+$` is one per module, `@ud` if unfixed; different auras never unify; faces are part of record types; principal types | Decided 2026-10-29 |

29+| Inference | Hindley–Milner with aura variables; a bare `@` in a `+$` is one per module, `@ud` if unfixed, and elsewhere each is its own, generalized per `++`; a number takes `@ud` only where its `++` isn't generic over its aura; different auras never unify; faces are part of record types; principal types | Decided 2026-10-30 |

30| Effects | The library unions `cmd` and `sub`; pokes and requests are opaque, from derived gates and `pure`; 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-10-29 |

31| 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; typed segments by aura | Decided 2026-10-29 |

32| Mark names | Any name: `/%` names types after marks, and constructors poke with their type's mark; no alias marks | Decided 2026-10-26 |

@@ -37,14 +37,14 @@ The choices behind the Language tab, made on 2026-10-23; a later date marks a re

37| Long calls | One argument per line inside parentheses | Decided |

39| Empty mold | `!!`, with no values; the expression has any type; pages are `(element !!)`, which keeps islands out of islands | Decided 2026-10-29 |

40−| Type variables | Capitals, generalized per `++` | Decided 2026-10-29 |

40+| Type variables | Capitals, generalized per `++`; one that meets an atom becomes an aura variable, and nothing more specific | Decided 2026-10-30 |

41| Loobean mold | `?`, switched with `?-` | Decided 2026-10-26 |

42| Defaults | None | Decided |

43| Modules | Records, not cores | Decided |

44| Kinds | The type of `main`: `(element !!)`, `(page R D)`, `(program D X M)` or `(store S)`; other names by file kind, in the Grammar tab | Decided 2026-10-29 |

45| Type identity | Recursive molds by name and module | Decided 2026-10-29 |

46| Binding patterns | In `?-` arms; the last position binds the rest | Decided 2026-10-29 |

47−| Text | Strings are written only as `"…"` and are always cords; tapes come from `trip`; `{…}` prints by aura, a bare `@` as `@ud`; `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-29 |

47+| 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 |

48| Auras | Soft, through aura variables | Decided 2026-10-29 |

49| 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 |

50| Refinement types | None | Decided |

docs/spec/grammar.md+4−4

@@ -120,12 +120,12 @@ Every other name is free.

120

121A mold is only a type: never called on a noun, and with no default. Types are inferred, Hindley–Milner with aura variables: every expression has a principal type, and there is no subtyping.

122

123−- **Atoms**: `@` and auras such as `@ud`, `@t`, `@p`, `@da`; `?` is a loobean. `@` is an atom whose aura isn't known yet, fixed by what it meets: `add` takes `[@ @]` and returns `@`, all one aura, so `(add n 1)` with `n=@ud` is a `@ud`. Different auras never unify. A bare `@` in a `+$` is one aura variable per module, `@ud` if unfixed.

123+- **Atoms**: `@` and auras such as `@ud`, `@t`, `@p`, `@da`; `?` is a loobean. `@` is an atom whose aura isn't known yet, fixed by what it meets: `add` takes `[@ @]` and returns `@`, all one aura, so `(add n 1)` with `n=@ud` is a `@ud`. Different auras never unify. A bare `@` in a `+$` is one aura variable per module, `@ud` if unfixed. Elsewhere, as in a gate's sample or a cast, each bare `@` is its own aura variable, generalized per `++` if nothing fixes it; atoms that must share an aura take one capital, as `[lo=A hi=A]`.

124- **Constants**: `%add`, `~` and the loobeans have one value each.

125- **Records and tuples**: `[text=@t done=?]`, `[@t ?]`. Faces are part of the type, so `[a=@ b=@]` and `[x=@ y=@]` don't unify. A record too long for one line can leave its `[` open, with one field per deeper line, as an expression's bracket does.

126- **Unions**: a `+$` with several cases below it. Every union written in Jibb has a name, so one used in a field, a sample, a cast, a gate's mold or an argument gets its own `+$`; only imports bring in unions without one. Tags take their union from context, as Tag resolution describes. Cases must differ as nouns: at some position of their right-nested cells, one is an atom and the other a cell, or both are different constants. `*`, type variables and molds that can be either, such as `(list A)` or `?`, overlap both. A union whose cases don't all differ is rejected.

127- **Containers**: `(list A)`, `(unit A)`, `(set A)`, `(map K V)`, `(mop K V)`, `(qeu A)`, `(jar K V)`, `(jug K V)`.

128−- **Gates**: `$-(A B)`. Type variables are capitals, generalized per `++`.

128+- **Gates**: `$-(A B)`. Type variables are capitals, generalized per `++`. A type variable that meets an atom becomes an aura variable, so `++ clamp |= [lo=A hi=A n=A]`, whose body calls `gth` and `max`, works on any one aura. It can become nothing more specific: a body that makes `A` a `@ud` or a list is an error.

129- **Paths**: `/todos` is constant, `/` empty, and `/todo/[id=@ud]` typed by aura. `%/blog/(slug)` is an `qath`, checked against routes and static files.

130- **Generic molds**: `+$ result |$ [V E]` with cases below; `|$` goes only right after a `+$`'s name.

131- **Any noun**: `*`. **Empty**: `!!`.

@@ -155,7 +155,7 @@ A tag literal or `~` gets a fresh type variable and a pending constraint: the va

155

156## Literals by context

157

158−Number and cell literals resolve like tags: each waits for its context and takes a default when its `++` is checked.

158+Number and cell literals resolve like tags: each waits for its context and takes a default when its `++` is checked. A number takes `@ud` only if nothing fixes its aura and its `++` isn't generic over it, so `++ inc |= n=A (add n 1)` stays generic, while the sum in `"{(add 1 2)}"` is a `@ud`.

159

160| Literal | Can become | Default |

161| --- | --- | --- |

@@ -163,7 +163,7 @@ Number and cell literals resolve like tags: each waits for its context and takes

163| Number `5` | Any aura | `@ud` |

164| Cell `[x xs]` | A tuple, a record, a cons | A tuple |

165

166−- In `{…}`, an atom prints by its aura: `@ud` as `1.000`, `@da` as a UTC date with sub-seconds, `@p` as a ship, and a bare `@` as `@ud`. `@t`, `@ta`, `@tas` and tapes splice as text; any other cell is an error asking for a printer. For readers, `print-date` prints in the theme's zone, Urbit-style, to the minute, as `~2026.10.29..14.30`; numbers keep Hoon's form.

166+- In `{…}`, an atom prints by its aura: `@ud` as `1.000`, `@da` as a UTC date with sub-seconds, `@p` as a ship, and a bare `@` as `@ud`. `@t`, `@ta`, `@tas` and tapes splice as text; any other cell is an error asking for a printer. Printers are picked when compiling, so an atom whose aura its `++` is generic over, as `n` in `|= n=A` or in a `|= n=@` that nothing fixes, is an error asking for an aura, here and in a `(…)` segment of an application path. For readers, `print-date` prints in the theme's zone, Urbit-style, to the minute, as `~2026.10.29..14.30`; numbers keep Hoon's form.

167- String literals are always cords, so an element needs `text`, as `(text "{n} items")`.

168- Where a list is expected, `[x xs]` is `x` in front of `xs`.

169- A typed segment prints and parses by aura, whether `[id=@ud]` in an agent's paths, a `_` route parameter typed by `load`'s sample, or a `(…)` segment of an application path; `@ta` and `@tas` are raw text.