@@ -0,0 +1,1045 @@
1+---
2+sort: 2
3+next: true
4+title: Tutorial
5+---
6+
7+# Nock tutorial
8+
9+So let's learn Nock! But wait - why learn Nock? After all,
10+we're going to be programming in Hoon, not Nock.
11+
12+Like JVM bytecode, Nock is as inscrutable as assembly language.
13+In fact, you can think of it as a sort of "functional assembly
14+language." There are sometimes reasons to program in real
15+assembly language. There is never a reason to program in Nock.
16+Except to learn Nock.
17+
18+Indeed, it is not necessary for the Hoon programmer to learn
19+Nock. We recommend it strongly, however, because Hoon has a very
20+special relationship with Nock - not unlike the relationship
21+between C and assembly language.
22+
23+Just as C is a very shallow layer over the raw CPU, Hoon is a
24+very shallow layer over raw Nock - often little more than a
25+macro. If you try to learn C without understanding the CPU under
26+it, you will be forever bemused by why it works the way it does.
27+
28+So let's learn Nock! But wait - which Nock? Nock, though more
29+frozen than Walt Disney, does have versions. Nock versions are
30+measured by integer degrees Kelvin, newer being colder. The
31+newest, Nock 5K - roughly the temperature of Neptune. No change
32+is anticipated between 5K and absolute zero, though you never
33+know. Any such change would certainly be quite painful.
34+
35+#1.1 Definition#
36+
37+The best way to learn Nock is to read the spec and write your own
38+naive interpreter. Here is Nock 5K:
39+
40+**1. Structures**
41+
42+ A noun is an atom or a cell. An atom is a natural number.
43+ A cell is an ordered pair of nouns.
44+
45+**2. Pseudocode**
46+
47+ 1 :: nock(a) *a
48+ 2 :: [a b c] [a [b c]]
49+ 3 ::
50+ 4 :: ?[a b] 0
51+ 5 :: ?a 1
52+ 6 :: +[a b] +[a b]
53+ 7 :: +a 1 + a
54+ 8 :: =[a a] 0
55+ 9 :: =[a b] 1
56+ 10 :: =a =a
57+ 11 ::
58+ 12 :: /[1 a] a
59+ 13 :: /[2 [a b]] a
60+ 14 :: /[3 [a b]] b
61+ 15 :: /[(a + a) b] /[2 /[a b]]
62+ 16 :: /[(a + a + 1) b] /[3 /[a b]]
63+ 17 :: /a /a
64+ 18 ::
65+ 19 :: *[a [[b c] d]] [*[a [b c]] *[a d]]
66+ 20 ::
67+ 21 :: *[a [0 b]] /[b a]
68+ 22 :: *[a [1 b]] b
69+ 23 :: *[a [2 [b c]]] *[*[a b] *[a c]]
70+ 24 :: *[a [3 b]] ?*[a b]
71+ 25 :: *[a [4 b]] +*[a b]
72+ 26 :: *[a [5 b]] =*[a b]
73+ 27 ::
74+ 28 :: *[a [6 [b [c d]]]] *[a 2 [0 1] 2 [1 c d] [1 0] 2 [1 2 3] [1 0] 4 4 b]
75+ 29 :: *[a [7 [b c]]] *[a 2 b 1 c]
76+ 30 :: *[a [8 [b c]]] *[a 7 [[7 [0 1] b] 0 1] c]
77+ 31 :: *[a [9 [b c]]] *[a 7 c 2 [0 1] 0 b]
78+ 32 :: *[a [10 [[b c] d]]] *[a 8 c 7 [0 3] d]
79+ 33 :: *[a [10 [b c]]] *[a c]
80+ 34 ::
81+ 35 :: *a *a
82+
83+Your interpreter should be no more than a page of code in
84+any language. For extra credit, `6`-`10` are macros; implement
85+them directly. For extra extra credit, optimize tail calls.
86+To test your code, write a decrement formula b such that
87+`*[a b]` is `a - 1` for any atomic nonzero `a`.
88+
89+#1.2 Installation#
90+
91+The second best way to learn Nock is to boot up your own Arvo
92+virtual computer. See the Arvo tutorial for instructions.
93+
94+#1.3 Nock#
95+
96+To make Nock make sense, let's work through Nock 5K line by line.
97+First the data model:
98+
99+##1. Structures##
100+
101+ A noun is an atom or a cell. An atom is any natural number.
102+ A cell is any ordered pair of nouns.
103+
104+Nouns are the dumbest data model ever. Nouns make JSON look like
105+XML and XML look like ASN.1. It may also remind you of Lisp's
106+S-expressions - you can think of nouns as "S-expressions without
107+the S."
108+
109+To be exact, a noun _is_ an S-expression, except that classic
110+S-expressions have multiple atom types ("S" is for "symbol").
111+Since Nock is designed to be used with a higher-level type system
112+(such as Hoon's), it does not need low-level types. An atom is
113+just an unsigned integer of any size.
114+
115+For instance, it's common to represent strings (or even whole
116+text files) as atoms, arranging them LSB first - so "foo" becomes
117+`0x6f6f66`. How do we know to print this as "foo", not `0x6f6f66`?
118+We need external information - such as a Hoon type. Similarly,
119+other common atomic types - signed integers, floating point, etc
120+- are all straightforward to map into atoms.
121+
122+It's also important to note that, unlike Lisp, Nock cannot create
123+cyclical data structures. It is normal and common for nouns in a
124+Nock runtime system to have acyclic structure - shared subtrees.
125+But there is no Nock computation that can make a child point to
126+its parent. One consequence: Nock has no garbage collector.
127+(Nor can dag structure be detected, as with Lisp `eq`.)
128+
129+There is also no single syntax for nouns. If you have nouns you
130+have Nock; if you have Nock you have Hoon; if you have Hoon, you
131+can write whatever parser you like.
132+
133+Let's continue:
134+
135+##2. Pseudocode##
136+
137+It's important to recognize that the pseudocode of the Nock spec
138+is just that: pseudocode. It looks a little like Hoon. It isn't
139+Hoon - it's just pseudocode. Or in other words, just English.
140+At the bottom of every formal system is a system of axioms, which
141+can only be written in English. (Why pseudocode, not Hoon? Since
142+Hoon is defined in Nock, this would only give a false impression
143+of nonexistent precision.)
144+
145+The logic of this pseudocode is a pattern-matching reduction,
146+matching from the top down. To compute Nock, repeatedly reduce
147+with the first line that matches. Let's jump right in!
148+
149+##Line 1:##
150+
151+ 1 :: nock(a) *a
152+
153+Nock is a pure (stateless) function from noun to noun. In our
154+pseudocode (and only in our pseudocode) we express this with the
155+prefix operator `*`.
156+
157+This function is defined for every noun, but on many nouns it
158+does nothing useful. For instance, if `a` is an atom, `*a`
159+reduces to... `*a`. In theory, this means that Nock spins
160+forever in an infinite loop. In other words, Nock produces no
161+result - and in practice, your interpreter will stop.
162+
163+(Another way to see this is that Nock has "crash-only" semantics.
164+There is no exception mechanism. The only way to catch Nock
165+errors is to simulate Nock in a higher-level virtual Nock -
166+which, in fact, we do all the time. A simulator (or a practical
167+low-level interpreter) can report, out of band, that Nock would
168+not terminate. It cannot recognize all infinite loops, of
169+course, but it can catch the obvious ones - like `*42`.)
170+
171+Normally `a` in `nock(a)` is a cell `[s f]`, or as we say
172+
173+ [subject formula]
174+
175+Intuitively, the formula is your function and the subject is
176+its argument. We call them something different because Hoon,
177+or any other high-level language built on Nock, will build its
178+own function calling convention which *does not* map directly
179+to `*[subject formula]`.
180+
181+##Line 2:##
182+
183+ 2 :: [a b c] [a [b c]]
184+
185+Ie, brackets (in our pseudocode, as in Hoon) associate to the
186+right. For those with Lisp experience, it's important to note
187+that Nock and Hoon use tuples or "improper lists" much more
188+heavily than Lisp. The list terminator, normally 0, is never
189+automatic. So the Lisp list
190+
191+ (a b c)
192+
193+becomes the Nock noun
194+
195+ [a b c 0]
196+
197+which is equivalent to
198+
199+ [a [b [c 0]]]
200+
201+Note that we can and do use unnecessary brackets anyway, for
202+emphasis.
203+
204+Let's move on to the axiomatic functions.
205+
206+##Lines 4-10:##
207+
208+ 4 :: ?[a b] 0
209+ 5 :: ?a 1
210+ 6 :: +[a b] +[a b]
211+ 7 :: +a 1 + a
212+ 8 :: =[a a] 0
213+ 9 :: =[a b] 1
214+
215+Here we define more pseudocode operators, which we'll use in
216+reductions further down. So far we have four built-in functions:
217+`*` meaning Nock itself, `?` testing whether a noun is a cell or
218+an atom, `+` incrementing an atom, and `=` testing for equality.
219+Again, no rocket science here.
220+
221+We should note that in Nock and Hoon, `0` (pronounced "yes") is
222+true, and `1` ("no") is false. Why? It's fresh, it's different,
223+it's new. And it's annoying. And it keeps you on your toes.
224+And it's also just intuitively right.
225+
226+
227+##Lines 12-16:##
228+
229+ 12 :: /[1 a] a
230+ 13 :: /[2 a b] a
231+ 14 :: /[3 a b] b
232+ 15 :: /[(a + a) b] /[2 /[a b]]
233+ 16 :: /[(a + a + 1) b] /[3 /[a b]]
234+
235+Slightly more interesting is our tree numbering. Every noun is of course a tree. The `/` operator - pronounced
236+"slot" - imposes an address space on that tree, mapping every
237+nonzero atom to a tree position.
238+
239+1 is the root. The head of every node `n` is `2n`; the tail is
240+`2n+1`. Thus a simple tree:
241+
242+ 1
243+ 2 3
244+ 4 5 6 7
245+ 14 15
246+
247+If the value of every leaf is its tree address, this tree is
248+
249+ [[4 5] [6 14 15]]
250+
251+and, for some examples of addressing:
252+
253+ /[1 [[4 5] [6 14 15]]]
254+
255+is `[[4 5] [6 14 15]]`
256+
257+ /[2 [[4 5] [6 14 15]]]
258+
259+is `[4 5]`
260+
261+ /[3 [[4 5] [6 14 15]]]
262+
263+is `[6 14 15]`, and
264+
265+ /[7 [[4 5] [6 14 15]]]
266+
267+is `[14 15]`
268+
269+I do hope this isn't so terribly hard to follow.
270+
271+##Line 21:##
272+
273+Now we enter the definition of Nock itself - ie, the `*`
274+operator.
275+
276+ 21 :: *[a 0 b] /[b a]
277+
278+`0` is simply Nock's tree-addressing operator. Let's try it out
279+from the Arvo command line.
280+
281+Note that we're using Hoon syntax here. Since we do not use Nock
282+from Hoon all that often (it's sort of like embedding assembly in
283+C), we've left it a little cumbersome. In Hoon, instead of
284+writing `*[a 0 b]`, we write
285+
286+ .*(a [0 b])
287+
288+So, to reuse our slot example, let's try the interpreter:
289+
290+ ~tasfyn-partyv> .*([[4 5] [6 14 15]] [0 7])
291+
292+gives, while the sky remains blue and the sun rises in the east:
293+
294+ [14 15]
295+
296+Even stupider is line 21:
297+
298+##Line 21:##
299+
300+ 21 :: *[a 1 b] b
301+
302+`1` is the constant operator. It produces its argument without
303+reference to the subject. So
304+
305+ ~tasfyn-partyv> .*(42 [1 153 218])
306+
307+yields
308+
309+ [153 218]
310+
311+
312+##Line 23:##
313+
314+ 23 :: *[a 2 b c] *[*[a b] *[a c]]
315+
316+Line 22 brings us the essential magic of recursion.
317+`2` is the Nock operator. If you can compute a subject and a
318+formula, you can evaluate them in the interpreter. In most
319+fundamental languages, like Lisp, `eval` is a curiosity. But
320+Nock has no `apply` - so all our work gets done with `2`.
321+
322+Let's convert the previous example into a stupid use of `2`:
323+
324+ ~tasfyn-partyv> .*(77 [2 [1 42] [1 1 153 218]])
325+
326+with a constant subject and a constant formula, gives the same
327+
328+ [153 218]
329+
330+Like so:
331+
332+ *[77 [2 [1 42] [1 1 153 218]]]
333+
334+ 22 :: *[a 2 b c] *[*[a b] *[a c]]
335+
336+ *[*[77 [1 42]] *[77 [1 1 153 218]]]
337+
338+ 21 :: *[a 1 b] b
339+
340+ *[42 *[77 [1 1 153 218]]]
341+
342+ *[42 1 153 218]
343+
344+ [153 218]
345+
346+##Lines 24-26:##
347+
348+ 24 :: *[a 3 b] ?*[a b]
349+ 25 :: *[a 4 b] +*[a b]
350+ 26 :: *[a 5 b] =*[a b]
351+
352+In lines 23-25, we meet our axiomatic functions again:
353+
354+For instance, if `x` is a formula that calculates some product,
355+`[4 x]` calculates that product plus one. Hence:
356+
357+ ~tasfyn-partyv> .*(57 [0 1])
358+ 57
359+
360+and
361+
362+ ~tasfyn-partyv> .*([132 19] [0 3])
363+ 19
364+
365+and
366+
367+ ~tasfyn-partyv> .*(57 [4 0 1])
368+ 58
369+
370+and
371+
372+ ~tasfyn-partyv> .*([132 19] [4 0 3])
373+ 20
374+
375+If this seems obvious, you're doin' good. Finally, we jump back up
376+to line 18, the trickiest in the spec:
377+
378+##Line 19:##
379+
380+ 19 :: *[a [b c] d] [*[a b c] *[a d]]
381+
382+Um, what?
383+
384+Since Nock of an atom just crashes, the practical domain of the
385+Nock function is always a cell. Conventionally, the head of this
386+cell is the "subject," the tail is the "formula," and the result
387+of Nocking it is the "product." Basically, the subject is your
388+data and the formula is your code.
389+
390+We could write line 19 less formally:
391+
392+ *[subject [formula-x formula-y]]
393+ => [*[subject formula-x] *[subject formula-y]]
394+
395+In other words, if you have two Nock formulas `x` and `y`, a
396+formula that computes the pair of them is just `[x y]`. We can
397+recognize this because no atom is a valid formula, and
398+every formula that _does not_ use line 19 has an atomic head.
399+
400+If you know Lisp, you can think of this feature as a sort of
401+"implicit cons." Where in Lisp you would write `(cons x y)`,
402+in Nock you write `[x y]`.
403+
404+For example,
405+
406+ ~tasfyn-partyv> .*(42 [4 0 1])
407+
408+where `42` is the subject (data) and `[4 0 1]` is the formula
409+(code), happens to evaluate to `43`. Whereas
410+
411+ ~tasfyn-partyv> .*(42 [3 0 1])
412+
413+is `1`. So if we evaluate
414+
415+ ~tasfyn-partyv> .*(42 [[4 0 1] [3 0 1]])
416+
417+we get
418+
419+ [43 1]
420+
421+Except for the crash defaults (lines 6, 10, 17, and 35), we've actually
422+completed all the _essential_ aspects of Nock. The operators up
423+through 5 provide all necessary computational functionality.
424+Nock, though very simple, is actually much more complex than it
425+formally needs to be.
426+
427+Operators 6 through 10 are macros. They exist because Nock is
428+not a toy, but a practical interpreter. Let's see them all
429+together:
430+
431+##Lines 28-33:##
432+
433+ 28 :: *[a 6 b c d] *[a 2 [0 1] 2 [1 c d] [1 0] 2 [1 2 3] [1 0] 4 4 b]
434+ 29 :: *[a 7 b c] *[a 2 b 1 c]
435+ 30 :: *[a 8 b c] *[a 7 [[7 [0 1] b] 0 1] c]
436+ 31 :: *[a 9 b c] *[a 7 c 2 [0 1] 0 b]
437+ 32 :: *[a 10 [b c] d] *[a 8 c 7 [0 3] d]
438+ 33 :: *[a 10 b c] *[a c]
439+
440+Whoa! Have we entered rocket-science territory? Let's try to
441+figure out what these strange formulas do - simplest first.
442+The simplest is clearly line 33:
443+
444+ 33 :: *[a 10 b c] *[a c]
445+
446+If `x` is an atom and `y` is a formula, the formula `[10 x y]`
447+appears to be equivalent to... `y`. For instance:
448+
449+ ~tasfyn-partyv> .*([132 19] [10 37 [4 0 3]])
450+ 20
451+
452+Why would we want to do this? `10` is actually a hint operator.
453+The `37` in this example is discarded information - it is not
454+used, formally, in the computation. It may help the interpreter
455+compute the expression more efficiently, however.
456+
457+Every Nock computes the same result - but not all at the same
458+speed. What hints are supported? What do they do? Hints are a
459+higher-level convention which do not, and should not, appear in
460+the Nock spec. Some are defined in Hoon. Indeed, a naive Nock
461+interpreter not optimized for Hoon will run Hoon quite poorly.
462+When it gets the product, however, the product will be right.
463+
464+There is another reduction for hints - line 32:
465+
466+ 32 :: *[a 10 [b c] d] *[a 8 c 7 [0 3] d]
467+
468+Once we see what `7` and `8` do, we'll see that this complex hint
469+throws away an arbitrary `b`, but computes the formula `c`
470+against the subject and... throws away the product. This formula
471+is simply equivalent to `d`. Of course, in practice the product
472+of `c` will be put to some sordid and useful use. It could even
473+wind up as a side effect, though we try not to get _that_ sordid.
474+
475+(Why do we even care that `c` is computed? Because `c` could
476+crash. A correct Nock cannot simply ignore it, and treat both
477+variants of `10` as equivalent.)
478+
479+We move on to the next simplest operator, `7`. Line 29:
480+
481+ 29 :: *[a 7 b c] *[a 2 b 1 c]
482+
483+Suppose we have two formulas, `b` and `c`. What is the formula
484+`[7 b c]`? This example will show you:
485+
486+ ~tasfyn-partyv> .*(42 [7 [4 0 1] [4 0 1]])
487+ 44
488+
489+`7` is an old mathematical friend, function composition. It's
490+easy to see how this is built out of `2`. The data to evaluate
491+is simply `b`, and the formula is `c` quoted.
492+
493+Line 30 looks very similar:
494+
495+ 30 :: *[a 8 b c] *[a 7 [[7 [0 1] b] 0 1] c]
496+
497+Indeed, `8` is `7`, except that the subject for `c` is not simply
498+the product of `b`, but the ordered pair of the product of `b`
499+and the original subject. Hence:
500+
501+ ~tasfyn-partyv> .*(42 [8 [4 0 1] [0 1]])
502+ [43 42]
503+
504+and
505+
506+ ~tasfyn-partyv> .*(42 [8 [4 0 1] [4 0 3]])
507+ 43
508+
509+Why would we want to do this? Imagine a higher-level language
510+in which the programmer declares a variable. This language is
511+likely to generate an `8`, because the variable is computed
512+against the present subject, and used in a calculation which
513+depends both on the original subject and the new variable.
514+
515+For extra credit, explain why we can't just define
516+
517+ *[a 8 b c] *[a 7 [b 0 1] c]
518+
519+Another simple macro is line 31:
520+
521+ 31 :: *[a 9 b c] *[a 7 c 2 [0 1] 0 b]
522+
523+`9` is a calling convention. With `c`, we produce a noun which
524+contains both code and data - a _core_. We use this core as the
525+subject, and apply the formula within it at slot `b`.
526+
527+And finally, we come to the piece de resistance - line 28:
528+
529+ 28 :: *[a 6 b c d] *[a 2 [0 1] 2 [1 c d] [1 0] 2 [1 2 3] [1 0] 4 4 b]
530+
531+Great giblets! WTF is this doing? It seems we've finally
532+arrived at some real rocket science.
533+
534+Actually, `6` is a primitive known to every programmer - good old
535+"if." If `b` evaluates to `0`, we produce `c`; if `b` evaluates
536+to `1`, we produce `d`; otherwise, we crash.
537+
538+For instance:
539+
540+ ~tasfyn-partyv> .*(42 [6 [1 0] [4 0 1] [1 233]])
541+ 43
542+
543+and
544+
545+ ~tasfyn-partyv> .*(42 [6 [1 1] [4 0 1] [1 233]])
546+ 233
547+
548+In real life, of course, the Nock implementor knows that `6` is
549+"if" and implements it as such. There is no practical sense in
550+reducing through this macro, or any of the others. We could have
551+defined "if" as a built-in function, like increment - except that
552+we can write "if" as a macro. If a funky macro.
553+
554+It's a good exercise, however, to peek inside the funk.
555+
556+We can actually simplify the semantics of `6`, at the expense of
557+breaking the system a little, by creating a macro that works as
558+"if" only if `b` is a proper boolean and produces `0` or `1`.
559+Perhaps we have a higher-level type system which checks this.
560+
561+This simpler "if" would be:
562+
563+ *[a 6 b c d] *[a [2 [0 1] [2 [1 c d] [[1 0] [4 4 b]]]]]
564+
565+Or without so many unnecessary brackets:
566+
567+ *[a 6 b c d] *[a 2 [0 1] 2 [1 c d] [1 0] [4 4 b]]
568+
569+How does this work? We've replaced `[6 b c d]` with the formula
570+`[2 [0 1] [2 [1 c d] [[1 0] [4 4 b]]]]`. We see two uses of `2`,
571+our evaluation operator - an outer and an inner.
572+
573+Call the inner one `i`. So we have `[2 [0 1] i]`. Which means
574+that, to calculate our product, we use `[0 1]` - that is, the
575+original subject - as the subject; and the product of `i` as
576+the formula.
577+
578+Okay, cool. So `i` is `[2 [1 c d] [[1 0] [4 4 b]]]`. We compute
579+Nock with subject `[1 c d]`, formula `[[1 0] [4 4 b]]`.
580+
581+Obviously, `[1 c d]` produces just `[c d]` - that is, the ordered
582+pair of the "then" and "else" formulas. `[[1 0] [4 4 b]]` is a
583+line 19 cell - its head is `[1 0]`, producing just `0`, its tail
584+`[4 4 b]`, producing... what? Well, if `[4 b]` is `b` plus `1`,
585+`[4 4 b]` is `b` plus `2`.
586+
587+We're assuming that `b` produces either `0` or `1`. So `[4 4 b]`
588+yields either `2` or `3`. `[[1 0] [4 4 b]]` is either `[0 2]` or
589+`[0 3]`. Applied to the subject `[c d]`, this gives us either
590+`c` or `d` - the product of our inner evaluation `i`. This is
591+applied to the original subject, and the result is "if."
592+
593+But we need the full power of the funk, because if `b` produces,
594+say, `7`, all kinds of weirdness will result. We'd really like
595+`6` to just crash if the test product is not a boolean. How can
596+we accomplish this? This is an excellent way to prove to
597+yourself that you understand Nock: figure out what the real `6`
598+does. Or you could just agree that `6` is "if," and move on.
599+
600+(It's worth noting that in practical, compiler-generated Nock, we
601+never do anything as funky as these `6` macro internals. There's
602+no reason we couldn't build formulas at runtime, but we have no
603+reason to and we don't - except when actually metaprogramming.
604+As in most languages, normally code is code and data is data.)
605+
606+#1.4 Decrement in Nock#
607+
608+A good practice exercise for Nock is a decrement formula. Ie, a
609+formula `f` which implements the partial function that produces
610+`(s - 1)` if `s` is a nonzero atom, and otherwise does not
611+terminate.
612+
613+The normal Hoon programmer has written one Nock formula: this
614+one. Since decrement uses all the Nock techniques the Hoon
615+compiler uses, the exercise is a good foundation. After you
616+write decrement (or just follow this example), you'll never need
617+to deal with Nock again.
618+
619+As we know, the equivalent formula for increment is
620+
621+ [4 0 1]
622+
623+Thus:
624+
625+ ~>tasfyn-partyv .*(42 [4 0 1])
626+ 43
627+
628+Of course, increment is built into Nock. So, ha, that's easy.
629+
630+How do we decrement? A good way to start is to gaze fondly on
631+how we'd do it if we actually had a real language, ie, Hoon.
632+Here is a minimal decrement in Hoon:
633+
634+ => a=. :: line 1
635+ =+ b=0 :: line 2
636+ |- :: line 3
637+ ?: =(a +(b)) :: line 4
638+ b :: line 5
639+ $(b +(b)) :: line 6
640+
641+Or for fun, on one line:
642+
643+ =>(a=. =+(b=0 |-(?:(=(a +(b)) b $(b +(b))))))
644+
645+Does Hoon actually work?
646+
647+ ~tasfyn-partyv> =>(42 =>(a=. =+(b=0 |-(?:(=(a +(b)) b $(b +(b)))))))
648+ 41
649+
650+Let's translate this into English. How do we decrement the
651+subject? First (line 1), we rename the subject `a`. Second
652+(line 2), we add a variable, `b`, an atom with value `0`.
653+Third (line 3), we loop. Fourth, we test if `a` equals `b` plus
654+1 (line 4), produce `b` if it does (line 5), repeat the loop with
655+`b` set to `b` plus 1 (line 6) if it doesn't. Obviously, while
656+the syntax is unusual, the algorithm is anything but deep. We
657+are calculating `b` minus one by counting up from `0`.
658+
659+(Obviously, this is an O(n) algorithm. Is there a better way?
660+There is not. Do we actually do this in practice? Yes and no.)
661+
662+Unfortunately we are missing a third of our Rosetta stone. We
663+have decrement in Hoon and we have it in English. How do we
664+express this in Nock? What will the Hoon compiler generate from
665+the code above? Let's work through it line by line.
666+
667+Nock has no types, variable names, etc. So line 1 is a no-op.
668+
669+How do we add a variable (line 2)? We compute a new subject,
670+which is a cell of the present subject and the variable. With
671+this new subject, we execute another formula.
672+
673+Since `0` is a constant, a formula that produces it is
674+
675+ [1 0]
676+
677+To combine `0` with the subject, we compute
678+
679+ [[1 0] [0 1]]
680+
681+which, if our subject is 42, gives us
682+
683+ [0 42]
684+
685+which we can use as the subject for an inner formula, `g`.
686+Composing our new variable with `g`, we have `f` as
687+
688+ [2 [[1 0] [0 1]] [1 g]]
689+
690+which seems a little funky for something so simple. But we
691+can simplify it with the composition macro, `7`:
692+
693+ [7 [[1 0] [0 1]] g]
694+
695+and still further with the augmentation macro, `8`:
696+
697+ [8 [1 0] g]
698+
699+If you refer back to the Nock definition, you'll see that all
700+these formulas are semantically equivalent.
701+
702+Let's continue with our decrement. So what's `g`? We seem to
703+loop. Does Nock have a loop operator? It most certainly does
704+not. So what do we do?
705+
706+We build a noun called a _core_ - a construct which is behind any
707+kind of interesting control flow in Hoon. Of course, the Nock
708+programmer is not constrained to use the same techniques as the
709+Hoon compiler, but it is probably a good idea.
710+
711+In Hoon, all the flow structures from your old life as an Earth
712+programmer become cores. Functions and/or closures are cores,
713+objects are cores modules are cores, even loops are cores.
714+
715+The core is just a cell whose tail is data (possibly containing
716+other cores) and whose head is code (containing one or more
717+formulas). The tail is the _payload_ and the head is the
718+_battery_. Hence your core is
719+
720+ [bat pay]
721+
722+To activate a core, pick a formula out of the battery, and use
723+the entire core (_not_ just the payload) as the subject.
724+
725+(A core formula is called an _arm_. An arm is almost like an
726+object-oriented method, but not quite - a method would be an arm
727+that produces a function on an argument. The arm is just a
728+function of the core, ie, a computed attribute.)
729+
730+Of course, because we feed it the entire core, our arm can
731+invoke itself (or any other formula in the battery). Hence, it
732+can loop. And this is what a loop is - the simplest of cores.
733+
734+We need to do two things with this core: create it, and activate
735+it. To be precise, we need two formulas: a formula which
736+produces the core, and one which activates its subject. We can
737+compose these functions with the handy `7` operator:
738+
739+ [8 [1 0] [7 p a]]
740+
741+`p` produces our core, `a` activates it. Let's take these in
742+reverse order. How do we activate a core?
743+
744+Since we have only one formula, it's the battery itself.
745+Thus we want to execute Nock with the whole core (already the
746+subject, and the entire battery (slot `2`). Hence, `a` is
747+
748+ [2 [0 1] [0 2]]
749+
750+We could also use the handy `9` macro - which almost seems
751+designed for firing arms on cores:
752+
753+ [9 2 [0 1]]
754+
755+Which leaves us seeking
756+
757+ [8 [1 0] [7 p [9 2 0 1]]]
758+
759+And all we have to do is build the core, `p`. How do we build a
760+core? We add code to the subject, just as we added a variable
761+above. The initial value of our counter was a constant, `0`.
762+The initial (and permanent) value of our battery is a constant,
763+the loop formula `l`. So `p` is
764+
765+ [8 [1 l] [0 1]]
766+
767+Which would leave us seeking
768+
769+ [8 [1 0] [7 [8 [1 l] [0 1]] [9 2 0 1]]]
770+
771+except that we have duplicated the `8` pattern again, since we
772+know
773+
774+ [7 [8 [1 l] [0 1]] [9 2 0 1]]
775+
776+is equivalent to
777+
778+ [8 [1 l] [9 2 0 1]]
779+
780+so the full value of `f` is
781+
782+ [8 [1 0] [8 [1 l] [9 2 0 1]]]
783+
784+Thus our only formula to compose is the loop body, `l`.
785+Its subject is the loop core:
786+
787+ [bat pay]
788+
789+where `bat` is just the loop formula, and `pay` is the pair `[a
790+b]`, `a` being the input subject, and `b` the counter. Thus we
791+could also write this subject as
792+
793+ [l b a]
794+
795+and we see readily that `a` is at slot `7`, `b` `6`, `l` `2`.
796+With this subject, we need to express the Hoon loop body
797+
798+ ?: =(a +(b)) :: line 4
799+ b :: line 5
800+ $(b +(b)) :: line 6
801+
802+This is obviously an if statement, and it calls for `6`. Ie:
803+
804+ [6 t y n]
805+
806+Giving our decrement program as:
807+
808+ [8 [1 0] [8 [1 6 t y n] [9 2 0 1]]]
809+
810+For `t`, how do we compute a flag that is yes (`0`) if `a` equals
811+`b` plus one? Equals, we recall, is `5`. So `t` can only be
812+
813+ [5 [0 7] [4 0 6]]
814+
815+If so, our product `y` is just the counter `b`:
816+
817+ [0 6]
818+
819+And if not? We have to re-execute the loop with the counter
820+incremented. If we were executing it with the same counter,
821+obviously an infinite loop, we could use the same core:
822+
823+ [9 2 0 1]
824+
825+But instead we need to construct a new core with the counter
826+incremented:
827+
828+ [l +(b) a]
829+
830+ie,
831+
832+ [[0 2] [4 0 6] [0 7]]
833+
834+and `n` is:
835+
836+ [9 2 [[0 2] [4 0 6] [0 7]]]
837+
838+Hence our complete decrement. Let's reformat vertically so we
839+can actually read it:
840+
841+ [8
842+ [1 0]
843+ [ 8
844+ [ 1
845+ [ 6
846+ t
847+ y
848+ n
849+ ]
850+ ]
851+ [9 2 0 1]
852+ ]
853+ ]
854+
855+which becomes
856+
857+ [8
858+ [1 0]
859+ [ 8
860+ [ 1
861+ [ 6
862+ [5 [0 7] [4 0 6]]
863+ [0 6]
864+ [9 2 [[0 2] [4 0 6] [0 7]]]
865+ ]
866+ ]
867+ [9 2 0 1]
868+ ]
869+ ]
870+
871+or, on one line without superfluous brackets:
872+
873+ [8 [1 0] 8 [1 6 [5 [0 7] 4 0 6] [0 6] 9 2 [0 2] [4 0 6] 0 7] 9 2 0 1]
874+
875+which works for the important special case, 42:
876+
877+ ~tasfyn-partyv> .*(42 [8 [1 0] 8 [1 6 [5 [0 7] 4 0 6] [0 6] 9 2 [0 2] [4 0 6] 0 7] 9 2 0 1])
878+ 41
879+
880+If you understood this, you understand Nock. At least in principle!
881+
882+If you want to play around more with Nock, the command line will
883+start getting unwieldy. Fortunately, the standard install
884+contains the above Nock decrement packaged as an Arvo app, which
885+you can edit and change if you'd like to get ambitious. Just run
886+
887+ ~tasfyn-partyv> :toy/ndec 19
888+ 18
889+
890+The file driving this is
891+
892+ hub/$seat/toy/app/ndec.holw
893+
894+Edit this file, ignoring everything above the Nock formula, and
895+hit return in the console to see it update:
896+
897+ ~tasfyn-partyv>
898+ : ~tasfyn-partyv/toy/app/ndec/holw/
899+
900+If decrement seems fun - why not write add? I wrote a Nock adder
901+a long, long time ago. But I've forgotten where I put it. There
902+is absolutely no use in this exercise, except to prove to
903+yourself that you've mastered Nock.
904+
905+#Appendix A: Operator Reductions#
906+
907+##`6` Reduction:##
908+
909+ 28 :: *[a 6 b c d] *[a 2 [0 1] 2 [1 c d] [1 0] 2 [1 2 3] [1 0] 4 4 b]
910+
911+ *[a 2 [0 1] 2 [1 c d] [1 0] 2 [1 2 3] [1 0] 4 4 b]
912+
913+ 23 :: *[a 2 b c] *[*[a b] *[a c]]
914+
915+ *[*[a 0 1] *[a 2 [1 c d] [1 0] 2 [1 2 3] [1 0] 4 4 b]]
916+
917+ 21 :: *[a 0 b] /[b a]
918+
919+ *[a *[a 2 [1 c d] [1 0] 2 [1 2 3] [1 0] 4 4 b]]
920+
921+ 23 :: *[a 2 b c] *[*[a b] *[a c]]
922+
923+ *[a *[*[a [1 c d]] *[a [1 0] 2 [1 2 3] [1 0] 4 4 b]]]
924+
925+ 22 :: *[a 1 b] b
926+
927+ 19 :: *[a [b c] d] [*[a b c] *[a d]]
928+
929+ *[a *[[c d] [*[a 1 0] *[a 2 [1 2 3] [1 0] 4 4 b]]]]
930+
931+ 22 :: *[a 1 b] b
932+
933+ *[a *[[c d] [0 *[a 2 [1 2 3] [1 0] 4 4 b]]]]
934+
935+ 23 :: *[a 2 b c] *[*[a b] *[a c]]
936+
937+ *[a *[[c d] [0 *[*[a [1 2 3]] *[a [1 0] 4 4 b]]]]]
938+
939+ 22 :: *[a 1 b] b
940+
941+ *[a *[[c d] [0 *[[2 3] *[a [1 0] 4 4 b]]]]]
942+
943+ 19 :: *[a [b c] d] [*[a b c] *[a d]]
944+
945+ *[a *[[c d] [0 *[[2 3] [*[a [1 0]] *[a 4 4 b]]]]]]
946+
947+ 22 :: *[a 1 b] b
948+
949+ *[a *[[c d] [0 *[[2 3] [0 *[a 4 4 b]]]]]]
950+
951+ 25 :: *[a 4 b] +*[a b]
952+
953+ *[a *[[c d] [0 *[[2 3] [0 ++*[a b]]]]]]
954+
955+**`6` Reduced:**
956+
957+ 6r :: *[a 6 b c d] *[a *[[c d] [0 *[[2 3] [0 ++*[a b]]]]]]
958+
959+##`7` Reduction:##
960+
961+ 29 :: *[a 7 b c] *[a 2 b 1 c]
962+
963+ *[a 2 b 1 c]
964+
965+ 23 :: *[a 2 b c] *[*[a b] *[a c]]
966+
967+ *[*[a b] *[a 1 c]]
968+
969+ 22: *[a 1 b] b
970+
971+ *[*[a b] c]
972+
973+**`7` Reduced:**
974+
975+ 7r :: *[a 7 b c] *[*[a b] c]
976+
977+##`8` Reduction:##
978+
979+ 30 :: *[a 8 b c] *[a 7 [[7 [0 1] b] 0 1] c]
980+
981+ *[a 7 [[7 [0 1] b] 0 1] c]
982+
983+ 7r :: *[a 7 b c] *[*[a b] c]
984+
985+ *[*[a [7 [0 1] b] 0 1]] c]
986+
987+ 19 :: *[a [b c] d] [*[a b c] *[a d]]
988+
989+ *[[*[a [7 [0 1] b]] *[a 0 1]] c]
990+
991+ 21 :: *[a 0 b] /[b a]
992+
993+ *[[*[a [7 [0 1] b]] /[1 a]] c]
994+
995+ 12 :: /[1 a] a
996+
997+ *[[*[a [7 [0 1] b]] a] c]
998+
999+ 7r :: *[a 7 b c] *[*[a b] c]
1000+
1001+ *[[*[*[a 0 1]] b] a] c]
1002+
1003+**`8` Reduced:**
1004+
1005+ 8r :: *[a 8 b c] *[[*[a b] a] c]
1006+
1007+
1008+##`9` Reduction:##
1009+
1010+ 31 :: *[a 9 b c] *[a 7 c [2 [0 1] [0 b]]]
1011+
1012+ *[a 7 c [2 [0 1] [0 b]]]
1013+
1014+ 7r :: *[a 7 b c] *[*[a b] c]
1015+
1016+ *[*[a c] [2 [0 1] [0 b]]]
1017+
1018+ 23 :: *[a 2 b c] *[*[a b] *[a c]]
1019+
1020+ *[*[*[a c] [0 1]] *[*[a c] [0 b]]]
1021+
1022+ 21 :: *[a 0 b] /[b a]
1023+
1024+**`9` Reduced:**
1025+
1026+ 9r :: *[a 9 b c] *[*[a c] *[*[a c] 0 b]]
1027+
1028+
1029+##`10` Reduction:##
1030+
1031+ *[a 10 [b c] d] *[a 8 c 7 [0 3] d]
1032+
1033+ 8r :: *[a 8 b c] [[*[a b] a] c]
1034+
1035+ *[[*[a c] a] 7 [0 2] d]
1036+
1037+ 7r :: *[a 7 b c] *[*[a b] c]
1038+
1039+ *[*[[*[a c] a] 0 3] d]
1040+
1041+ 21 :: *[a 0 b] /[b a]
1042+
1043+**`10` reduced:**
1044+
1045+ 10r :: *[a 10 [b c] d] *[a d]