on 98c19cd help sign in
jibb/docs/spec/core-language.md
175 lines 11 kB history raw
1# Core language
3Oct 29, 2026 · @iko
5After checking, every Jibb module lowers to the core language: Nock's operations on nouns, plus a lambda calculus with names. The Nock and JavaScript backends both compile it, and an interpreter for it, written in Hoon, is the reference both are tested against. Rules marked *proposed* aren't decided yet.
7## Nodes
9Fifteen kinds of node: seven that build and test nouns, each one Nock operation; five for control; and natives, crashes and traces.
11| Node | Value |
12| --- | --- |
13| `42`, `%add`, `"milk"` | The atom written, in Jibb's literal syntax |
14| `x` | The value bound to `x` |
15| `(cons e f)` | The cell of `e` and `f` |
16| `(slot n e)` | The value at axis `n` of `e`; crashes if there is none, as Nock 0 does |
17| `(edit n e v)` | `e` with axis `n` replaced by `v`; crashes if `e` has no axis `n`, as Nock 10 does |
18| `(cell? e)` | `%.y` if `e` is a cell, else `%.n`, as Nock 3 |
19| `(eq e f)` | `%.y` if the two nouns are equal, else `%.n`, as Nock 5 |
20| `(if c t f)` | `t` if `c` is `%.y`, `f` if it's `%.n`; crashes on anything else, as Nock 6 does |
21| `(let x e b)` | `b`, with `x` bound to `e` |
22| `(rec ((f l) …) b)` | `b`, with each `f` bound to its `lam`, all visible to each other |
23| `(lam x b)` | A function of one sample, bound to `x` in `b` |
24| `(app f e)` | `f` called with `e` as its sample |
25| `(native n)` | The native function `n` |
26| `(crash)` | A crash, as `!!` |
27| `(trace m b)` | Prints the cord `m`, then is `b`, as `~&` |
29Literals keep the aura they were written with, but only for printing and as a hint to the JavaScript backend. A call with several arguments passes one cell, as Nock's gates take one sample.
31## Values and invariants
33A value is a noun or a function. A function can sit inside a cell, but it isn't a noun: each backend represents it its own way, and it never crosses between ship and browser.
35The front end guarantees the backends:
37- **No shadowing.** No binding hides another: Jibb forbids it, and generated names start with `_`, which Jibb names can't.
38- **`rec` binds functions.** Every right side of a `rec` is a `lam`.
39- **Functions aren't taken apart.** `cell?`, `eq`, `slot` and `edit` never get a function itself, and `eq` never compares nouns that contain one. Island data and models are already first-order. So are `eq`'s arguments and map and set keys, and a gate never tells a union's cases apart.
40- **Strict evaluation.** A call's sample is evaluated before the call, and a node's parts in text order; `if` evaluates only the branch it takes. Only `trace` and `crash` can observe the order, and differential tests compare results and whether a program crashes, not traces. So the backends may evaluate a node's parts in another order, as Nock 10 does with edit's v and e.
41- **Crashes stay crashes.** Where types already guarantee a test, the backends still crash on a violation, as Nock does, instead of carrying on.
43## Text form
45S-expressions, so each stage's output can be printed, read back and tested on its own, and backend work can start on hand-written programs.
47```
48expr = literal | name
49 | "(" "cons" expr expr ")"
50 | "(" "slot" axis expr ")"
51 | "(" "edit" axis expr expr ")"
52 | "(" "cell?" expr ")"
53 | "(" "eq" expr expr ")"
54 | "(" "if" expr expr expr ")"
55 | "(" "let" name expr expr ")"
56 | "(" "rec" "(" { "(" name lam ")" } ")" expr ")"
57 | lam
58 | "(" "app" expr expr ")"
59 | "(" "native" name ")"
60 | "(" "crash" ")"
61 | "(" "trace" expr expr ")" ;
62lam = "(" "lam" name expr ")" ;
63module = "(" "module" path { "(" "def" name expr ")" } ")" ;
64name = jname | path ":" jname | "_" ( letter | digit ) { letter | digit } ; (* own or prelude, imported, generated *)
65axis = digit { digit } ; (* at least 1 *)
66```
68- `literal` is Jibb's literal syntax, and the form a literal was written in is the aura the printer writes it back with.
69- `jname` is a Jibb name; `path` is a module's path under `/ui`, as in `api/todo:todo-action`.
70- Whitespace separates items, and `::` starts a comment. Source positions aren't written, so golden tests don't change when lines move; the printer can add them as comments.
72## Lowering from Jibb
74Types, faces and casts leave nothing behind; everything else lowers by these rules.
76| Jibb | Core language |
77| --- | --- |
78| A number, ship, date, term, loobean, `~`, or a string without `{…}` | An atom literal, keeping its aura |
79| `"Since {day}"` | `(app (native join) …)` on a list of the pieces, each atom printed first by its aura's native |
80| `` `x `` | `(cons ~ x)` |
81| `[a b c]`, `[x=a y=b]`, `~[a b]` | Right-nested `cons` in field order; a list ends in `~` |
82| `gap+%s2` | `(cons %gap %s2)` |
83| `/posts/~zod`, `%/blog/(slug)` | A list of knots, typed segments printed by their aura's native; the runtime adds the base path to an application path |
84| `title.p`, `space.theme.theme` | `slot` at the field's axis, nested for longer wings |
85| `card.card`, an import | The qualified name `components/card:card` |
86| `m(draft=t error=~)` | One `edit` per item, in order: `(edit 7 (edit 6 m t) ~)` |
87| `f a b c` | `(app f (cons a (cons b c)))`: the arguments are the sample |
88| `\|= [a=@ b=@] body` | `(lam _1 (let a (slot 2 _1) (let b (slot 3 _1) body)))`; a single face, as in `\|= m=model`, names the `lam` itself |
89| `\|=%got` | `(lam _1 (cons %got _1))` |
90| `++` definitions, at top level or in a gate | A `rec` per group of gates that call each other; a `let` per other value, in dependency order |
91| `?- s` | `(let _1 s …)` around a decision tree of `if`, `cell?`, `eq` and `slot`, built by the usual pattern-matrix algorithm; binders become `let`s, and tests the types make redundant are left out |
92| `?-` on a loobean | `(if s yes no)` |
93| `^- t e` | `e` |
94| `~& v body` | `(trace (app _p v) body)`, where `_p` is a printer derived from `v`'s type |
95| `!!` | `(crash)` |
96| Derived gates and `pure` | `lam`s that build the cells the runtime reads |
97| Checks on incoming facts | A validator derived from the path's type, which the runtime runs on each fact |
99## Example
101The todo island's `update`, from worked example 3:
103```jibb
104++ update |= [=msg m=model]
105 ?- msg
106 [%typed t]
107 ?- (gth (lent (tuba (trip t))) 80)
108 %.y [m(draft=t error=`"Too long") ~]
109 %.n [m(draft=t error=~) ~]
110 %submit [m(draft="") ~[[%poke (todo-action.todo [%add draft.m]) |=%acked]]]
111 [%toggled id] [m ~[[%poke (todo-action.todo [%toggle id]) |=%acked]]]
112 [%got ts] [m(todos=ts) ~]
113 [%acked err] [m(error=err) ~]
114```
116lowers to the program below. The model `[todos draft error]` puts `todos` at axis 2, `draft` at 6 and `error` at 7, and `%submit`, the only atom case, needs no test once `cell?` fails.
118```
119(def update
120 (lam _1
121 (let msg (slot 2 _1)
122 (let m (slot 3 _1)
123 (if (cell? msg)
124 (let _2 (slot 2 msg)
125 (if (eq _2 %typed)
126 (let t (slot 3 msg)
127 (if (app (native gth) (cons (app (native lent) (app (native tuba) (app (native trip) t))) 80))
128 (cons (edit 7 (edit 6 m t) (cons ~ "Too long")) ~)
129 (cons (edit 7 (edit 6 m t) ~) ~)))
130 (if (eq _2 %toggled)
131 (let id (slot 3 msg)
132 (cons m (cons (cons %poke (cons (app api/todo:todo-action (cons %toggle id)) (lam _3 (cons %acked _3)))) ~)))
133 (if (eq _2 %got)
134 (let ts (slot 3 msg) (cons (edit 2 m ts) ~))
135 (let err (slot 3 msg) (cons (edit 7 m err) ~))))))
136 (cons (edit 6 m "")
137 (cons (cons %poke (cons (app api/todo:todo-action (cons %add (slot 6 m))) (lam _4 (cons %acked _4)))) ~)))))))
138```
140## Programs and linking
142- Each module lowers to `(module <path> (def name e) …)`, in source order. Its own and the prelude's definitions are named plainly, since no name may shadow another; imports are qualified, as in `api/todo:todo-action`.
143- The linker builds one program per entry: on the ship, each page; in the browser, each island's `update`, `view` and `subs`, and each store. It keeps only the definitions the entry reaches, sorts them by dependency into `let`s and `rec`s, and ends with the entry.
144- Values that aren't gates are computed once per program, before anything calls them; the Nock backend may compute them at build time. A value that depends on itself, even through a gate, is an error.
145- A module used as a whole value is a cell of its definitions, in name order.
147## Natives
149- Jetted prelude functions have working Jibb implementations. Foundational gates use private low-level primitives from the internal prelude module. The compiler recognizes the functions' shapes and uses the corresponding Hoon versions, so their jets can fire. The JavaScript runtime supplies corresponding implementations; differential tests check their behavior.
150- The lowering uses a few private ones: `join` for interpolation, a printer per aura, and the map and set checks in validators.
151- Jetted prelude functions may take gates. On the ship a Jibb gate is shaped like Hoon's, so functions such as `turn`, `sort` and `skim` can call it. In JavaScript native implementations can use loops, which keeps long lists off the stack. Such a function only calls the gate and never takes it apart, so the invariant above still holds.
153## Backends
155Each node becomes a few Nock operations, or a few lines of JavaScript calling the runtime.
157| Node | Nock | JavaScript |
158| --- | --- | --- |
159| Literal | `[1 a]` | A number or a constant atom; a cord also keeps its string |
160| `x` | `[0 a]`, at `x`'s axis in the subject; a name bound by `rec` is an arm of its core, `[9 a 0 c]` with `c` the core's axis | A variable |
161| `cons` | A cell of the two formulas | `cell(e, f)` |
162| `slot` | `[7 e 0 n]` | `slot(n, e)` |
163| `edit` | `[10 [n v] e]` | `edit(n, e, v)` |
164| `cell?` | `[3 e]` | `isCell(e)` |
165| `eq` | `[5 e f]` | `same(e, f)` |
166| `if` | `[6 c t f]` | A conditional that crashes on anything but 0 or 1 |
167| `let` | `[8 e b]`, pushing the value onto the subject | `const` |
168| `rec` | A core with an arm per function, as `\|%` builds | Function declarations |
169| `lam` | A gate shaped like Hoon's: `$` at axis 2, sample at 6 | A closure of one argument |
170| `app` | `[9 2 10 [6 e] f]` | `f(e)`; a self call in tail position becomes a loop |
171| `native` | The native's Hoon gate | The native's runtime function |
172| `crash` | `[0 0]` | A thrown crash |
173| `trace` | A `%slog` hint, Nock 11, carrying `[0 leaf+(trip m)]`, since `%slog` takes a priority and a tank, not a cord | `console.log`, then `b` |
175Gates are shaped like Hoon's, so `app` calls a Jibb gate and a native's Hoon gate the same way, and Hoon code can call Jibb gates.