on 6d45ede help sign in
urbit.org/docs/nock/explanation.md
562 lines 15 kB history raw
1---
2navhome: /docs
3sort: 2
4next: true
5title: Explanation
6---
8# An explanation of Nock
10To make Nock make sense, let's work through the spec line by line.
11First the data model:
13## Nouns
15```
16A noun is an atom or a cell. An atom is any natural number.
17A cell is any ordered pair of nouns.
18```
20Nouns are the dumbest data model ever. Nouns make JSON look like
21XML and XML look like ASN.1. It may also remind you of Lisp's
22S-expressions - you can think of nouns as "S-expressions without
23the S."
25To be exact, a noun *is* an S-expression, except that classic
26S-expressions have multiple atom types ("S" is for "symbol").
27Since Nock is designed to be used with a higher-level type system
28(such as Hoon's), it does not need low-level types. An atom is
29just an unsigned integer of any size.
31For instance, it's common to represent strings (or even whole
32text files) as atoms, arranging them LSB first - so "foo" becomes
33`0x6f6f66`. How do we know to print this as "foo", not `0x6f6f66`?
34We need external information - such as a Hoon type. Similarly,
35other common atomic types - signed integers, floating point, etc
36- are all straightforward to map into atoms.
38It's also important to note that, unlike Lisp, Nock cannot create
39cyclical data structures. It is normal and common for nouns in a
40Nock runtime system to have acyclic structure - shared subtrees.
41But there is no Nock computation that can make a child point to
42its parent. One consequence: Nock has no garbage collector.
43(Nor can dag structure be detected, as with Lisp `eq`.)
45There is also no single syntax for nouns. If you have nouns you
46have Nock; if you have Nock you have Hoon; if you have Hoon, you
47can write whatever parser you like.
49## Reductions
51It's important to recognize that the pseudocode of the Nock spec
52is just that: pseudocode. It looks a little like Hoon. It isn't
53Hoon - it's just pseudocode. Or in other words, just English.
54At the bottom of every formal system is a system of axioms, which
55can only be written in English. (Why pseudocode, not Hoon? Since
56Hoon is defined in Nock, this would only give a false impression
57of nonexistent precision.)
59The logic of this pseudocode is a pattern-matching reduction,
60matching from the top down. To compute Nock, repeatedly reduce
61with the first line that matches. Let's jump right in!
63### Nock principles
65```
66nock(a) *a
67```
69Nock is a pure (stateless) function from noun to noun. In our
70pseudocode (and only in our pseudocode) we express this with the
71prefix operator `*`.
73This function is defined for every noun, but on many nouns it
74does nothing useful. For instance, if `a` is an atom, `*a`
75reduces to... `*a`. In theory, this means that Nock spins
76forever in an infinite loop. In other words, Nock produces no
77result - and in practice, your interpreter will stop.
79(Another way to see this is that Nock has "crash-only" semantics.
80There is no exception mechanism. The only way to catch Nock
81errors is to simulate Nock in a higher-level virtual Nock -
82which, in fact, we do all the time. A simulator (or a practical
83low-level interpreter) can report, out of band, that Nock would
84not terminate. It cannot recognize all infinite loops, of
85course, but it can catch the obvious ones - like `*42`.)
87Normally `a` in `nock(a)` is a cell `[s f]`, or as we say
89```
90[subject formula]
91```
93Intuitively, the formula is your function and the subject is
94its argument. We call them something different because Hoon,
95or any other high-level language built on Nock, will build its
96own function calling convention which *does not* map directly
97to `*[subject formula]`.
99### Noun syntax
101```
102[a b c] [a [b c]]
103```
105Ie, brackets (in our pseudocode, as in Hoon) associate to the
106right. For those with Lisp experience, it's important to note
107that Nock and Hoon use tuples or "improper lists" much more
108heavily than Lisp. The list terminator, normally 0, is never
109automatic. So the Lisp list
111```
112(a b c)
113```
115becomes the Nock noun
117```
118[a b c 0]
119```
121which is equivalent to
123```
124[a [b [c 0]]]
125```
127Note that we can and do use unnecessary brackets anyway, for
128emphasis. Let's move on to the axiomatic functions:
130### Trivial operators
132```
133?[a b] 0
134?a 1
135+[a b] +[a b]
136+a 1 + a
137=[a a] 0
138=[a b] 1
139```
141Here we define more pseudocode operators, which we'll use in
142reductions further down. So far we have four built-in functions:
143`*` meaning Nock itself, `?` testing whether a noun is a cell or
144an atom, `+` incrementing an atom, and `=` testing for equality.
145Again, no rocket science here.
147We should note that in Nock and Hoon, `0` (pronounced "yes") is
148true, and `1` ("no") is false. Why? As in Unix, using zero for
149success generalizes smoothly to multiple error codes. And it's
150strange for success not to equal truth. Or at least, this is
151our official excuse.
153### Tree addressing
155```
156/[1 a] a
157/[2 a b] a
158/[3 a b] b
159/[(a + a) b] /[2 /[a b]]
160/[(a + a + 1) b] /[3 /[a b]]
161```
163Slightly more interesting is our tree numbering. Every noun is
164of course a tree. The `/` operator - pronounced "slot" - imposes
165an address space on that tree, mapping every nonzero atom to a
166tree position.
1681 is the root. The head of every node `n` is `2n`; the tail is
169`2n+1`. Thus a simple tree:
171```
172 1
173 2 3
1744 5 6 7
175 14 15
176```
178If the value of every leaf is its tree address, this tree is
180```
181[[4 5] [6 14 15]]
182```
184and, for some examples of addressing:
186```
187/[1 [[4 5] [6 14 15]]]
188```
190is `[[4 5] [6 14 15]]`
192```
193/[2 [[4 5] [6 14 15]]]
194```
196is `[4 5]`
198```
199/[3 [[4 5] [6 14 15]]]
200```
202is `[6 14 15]`, and
204```
205/[7 [[4 5] [6 14 15]]]
206```
208is `[14 15]`
210Hopefully this isn't terribly hard to follow.
212## Instructions
214These rules define Nock itself - ie, the `*` operator.
216### `0`, slot
218```
219*[a 0 b] /[b a]
220```
222`0` is Nock's tree-addressing instruction. Let's try it out
223from the Arvo command line.
225Note that we're using Hoon syntax here. Since we do not use Nock
226from Hoon all that often (it's sort of like embedding assembly in
227C), we've left it a little cumbersome. In Hoon, instead of
228writing `*[a 0 b]`, we write
229```
230.*(a [0 b])
231```
233So, to reuse our slot example, let's try the interpreter:
235```
236~zod:dojo> .*([[4 5] [6 14 15]] [0 7])
237```
239produces `[14 15]`.
241### `1`, constant
243```
244*[a 1 b] b
245```
247`1` is the constant instruction. It produces its argument without
248reference to the subject. So
250```
251~zod:dojo> .*(42 [1 153 218])
252```
254yields `[153 218]`.
256### `2`, evaluate
258`2` is the Nock instruction:
260```
261*[a 2 b c] *[*[a b] *[a c]]
262```
264If you can compute a subject and a
265formula, you can evaluate them in the interpreter. In most
266fundamental languages, like Lisp, `eval` is a curiosity. But
267Nock has no `apply` - so all our work gets done with `2`.
269Let's convert the previous example into a stupid use of `2`,
270with constant subject and formula:
272```
273~zod:dojo> .*(77 [2 [1 42] [1 1 153 218]])
274```
276This gives the same `[153 218]`
278### `3`, `4`, and `5`, axiomatic functions
280```
281*[a 3 b] ?*[a b]
282*[a 4 b] +*[a b]
283*[a 5 b] =*[a b]
284```
286In lines 23-25, we meet our axiomatic functions again:
288For instance, if `x` is a formula that calculates some product,
289`[4 x]` calculates that product plus one. Hence:
291```
292~zod:dojo> .*(57 [0 1])
29357
294~zod:dojo> .*([132 19] [0 3])
29519
296~zod:dojo> .*(57 [4 0 1])
29758
298~zod:dojo> .*([132 19] [4 0 3])
29920
300```
302### Distribution
304```
305*[a [b c] d] [*[a b c] *[a d]]
306```
308Since Nock of an atom just crashes, the practical domain of the
309Nock function is always a cell. Conventionally, the head of this
310cell is the "subject," the tail is the "formula," and the result
311of Nocking it is the "product." Basically, the subject is your
312data and the formula is your code.
314We could write this line less formally:
316```
317*[subject [formula-x formula-y]]
318=> [*[subject formula-x] *[subject formula-y]]
319```
321In other words, if you have two Nock formulas `x` and `y`, a
322formula that computes the pair of them is just `[x y]`. We can
323recognize this because no atom is a valid formula, and
324every formula that *does not* use line 19 has an atomic head.
326If you know Lisp, you can think of this feature as a sort of
327"implicit cons." Where in Lisp you would write `(cons x y)`,
328in Nock you write `[x y]`.
330For example,
332```
333~zod:dojo> .*(42 [4 0 1])
334```
336where `42` is the subject (data) and `[4 0 1]` is the formula
337(code), happens to evaluate to `43`. Whereas
339```
340~zod:dojo> .*(42 [3 0 1])
341```
343is `1`. So if we evaluate
345```
346~zod:dojo> .*(42 [[4 0 1] [3 0 1]])
347```
349we get
351```
352[43 1]
353```
355Except for the crash defaults (lines 6, 10, 17, and 35), we've actually
356completed all the _essential_ aspects of Nock. The instructions up
357through 5 provide all necessary computational functionality.
358Nock, though very simple, is actually much more complex than it
359formally needs to be.
361Operators 6 through 10 are macros. They exist because Nock is
362not a toy, but a practical interpreter. Let's see them all
363together:
365## Macros
367```
368*[a 6 b c d] *[a 2 [0 1] 2 [1 c d] [1 0] 2 [1 2 3] [1 0] 4 4 b]
369*[a 7 b c] *[a 2 b 1 c]
370*[a 8 b c] *[a 7 [[7 [0 1] b] 0 1] c]
371*[a 9 b c] *[a 7 c 2 [0 1] 0 b]
372*[a 10 [b c] d] *[a 8 c 7 [0 3] d]
373*[a 10 b c] *[a c]
374```
376Notice that instructions `6` through `10` are macros: each just
377expands to a larger formula. Let's try to figure out what these
378macros do, simplest first:
380### `10`, hint
382```
383*[a 10 b c] *[a c]
384```
386If `x` is an atom and `y` is a formula, the formula `[10 x y]`
387appears to be equivalent to... `y`. For instance:
389```
390.*([132 19] [10 37 [4 0 3]])
391```
393Why would we want to do this? `10` is actually a hint instruction.
394The `37` in this example is discarded information - it is not
395used, formally, in the computation. It may help the interpreter
396compute the expression more efficiently, however.
398Every Nock computes the same result - but not all at the same
399speed. What hints are supported? What do they do? Hints are a
400higher-level convention which do not, and should not, appear in
401the Nock spec. Some are defined in Hoon. Indeed, a naive Nock
402interpreter not optimized for Hoon will run Hoon quite poorly.
403When it gets the product, however, the product will be right.
405There is another instruction `10` rule:
407```
408*[a 10 [b c] d] *[a 8 c 7 [0 3] d]
409```
411Once we see what `7` and `8` do, we'll see that this complex hint
412throws away an arbitrary `b`, but computes the formula `c`
413against the subject and... throws away the product. This formula
414is simply equivalent to `d`. Of course, in practice the product
415of `c` will be put to some sordid and useful use. It could even
416wind up as a side effect.
418(Why do we even care that `c` is computed? Because `c` could
419crash. A correct Nock cannot simply ignore it, and treat both
420variants of `10` as equivalent.)
422### `7`, compose
424```
425*[a 7 b c] *[a 2 b 1 c]
426```
428Suppose we have two formulas, `b` and `c`. What is the formula
429`[7 b c]`? This example will show you:
431```
432~zod:dojo> .*(42 [7 [4 0 1] [4 0 1]])
43344
434```
436Good old composition, on Nock formulas. It's easy to see how
437this is built out of `2`. The data to evaluate is simply `b`,
438and the formula is `c` quoted.
440### `8`, extend
442```
443*[a 8 b c] *[a 7 [[7 [0 1] b] 0 1] c]
444```
446`8` is `7`, except that the subject for `c` is not simply the
447product of `b`, but the ordered pair of the product of `b` and
448the original subject. Hence:
450```
451.*(42 [8 [4 0 1] [0 1]])
452[43 42]
453```
455```
456~zod:dojo> .*(42 [8 [4 0 1] [4 0 3]])
45743
458```
460Why would we want to do this? Imagine a higher-level language
461in which the programmer declares a variable. This language is
462likely to generate an `8`, because the variable is computed
463against the present subject, and used in a calculation which
464depends both on the original subject and the new variable.
466For extra credit, explain why we can't just define
468```
469*[a 8 b c] *[a 7 [b 0 1] c]
470```
472### `9`, invoke
474`9` is a calling convention:
476```
477*[a 9 b c] *[a 7 c 2 [0 1] 0 b]
478```
480With `c`, we produce a noun which contains both code and data - a
481*core*. We use this core as the subject, and evaulate the
482formula within it at slot `b`.
484### `6`, if-then-else
486This looks much scarier than it is:
488```
489*[a 6 b c d] *[a 2 [0 1] 2 [1 c d] [1 0] 2 [1 2 3] [1 0] 4 4 b]
490```
492If `b` evaluates to `0`, we produce `c`; if `b` evaluates to `1`,
493we produce `d`; otherwise, we crash.
495For instance:
497```
498~zod:dojo> .*(42 [6 [1 0] [4 0 1] [1 233]])
49943
500~zod:dojo> .*(42 [6 [1 1] [4 0 1] [1 233]])
501233
502```
504In real life, of course, the Nock implementor knows that `6` is
505"if" and implements it as such. There is no practical sense in
506reducing through this macro, or any of the others. We could have
507defined "if" as a built-in function, like increment - except that
508we can write "if" as a macro. If a funky macro.
510We can actually simplify the semantics of `6`, at the expense of
511breaking the system a little, by creating a macro that works as
512"if" only if `b` is a proper boolean and produces `0` or `1`.
513Perhaps we have a higher-level type system which checks this.
515This simpler "if" would be:
517```
518*[a 6 b c d] *[a [2 [0 1] [2 [1 c d] [[1 0] [4 4 b]]]]]
519```
521Or without so many unnecessary brackets:
523```
524*[a 6 b c d] *[a 2 [0 1] 2 [1 c d] [1 0] [4 4 b]]
525```
527How does this work? We've replaced `[6 b c d]` with the formula
528`[2 [0 1] [2 [1 c d] [[1 0] [4 4 b]]]]`. We see two uses of `2`,
529our evaluation instruction - an outer and an inner.
531Call the inner one `i`. So we have `[2 [0 1] i]`. Which means
532that, to calculate our product, we use `[0 1]` - that is, the
533original subject - as the subject; and the product of `i` as
534the formula.
536Okay, cool. So `i` is `[2 [1 c d] [[1 0] [4 4 b]]]`. We compute
537Nock with subject `[1 c d]`, formula `[[1 0] [4 4 b]]`.
539Obviously, `[1 c d]` produces just `[c d]` - that is, the ordered
540pair of the "then" and "else" formulas. `[[1 0] [4 4 b]]` is a
541line 19 cell - its head is `[1 0]`, producing just `0`, its tail
542`[4 4 b]`, producing... what? Well, if `[4 b]` is `b` plus `1`,
543`[4 4 b]` is `b` plus `2`.
545We're assuming that `b` produces either `0` or `1`. So `[4 4 b]`
546yields either `2` or `3`. `[[1 0] [4 4 b]]` is either `[0 2]` or
547`[0 3]`. Applied to the subject `[c d]`, this gives us either
548`c` or `d` - the product of our inner evaluation `i`. This is
549applied to the original subject, and the result is "if."
551But we need the full power of the funk, because if `b` produces,
552say, `7`, all kinds of weirdness will result. We'd really like
553`6` to just crash if the test product is not a boolean. How can
554we accomplish this? This is an excellent way to prove to
555yourself that you understand Nock: figure out what the real `6`
556does. Or you could just agree that `6` is "if," and move on.
558(It's worth noting that in practical, compiler-generated Nock, we
559never do anything as funky as these `6` macro internals. There's
560no reason we couldn't build formulas at runtime, but we have no
561reason to and we don't - except when actually metaprogramming.
562As in most languages, normally code is code and data is data.)