@@ -4,28 +4,56 @@ weight = 11
44template = "doc.html"
55aliases = ["docs/reference/hoon-expressions/rune/ket/"]
66+++
7−[`^-` ("kethep")](#kethep), [`^+` ("ketlus")](#ketlus), and
8−[`^=` ("kettis")](#kettis) let us adjust types without violating type
9−constraints.
107
11−The `nest` algorithm which tests subtyping is conservative;
12−it never allows invalid nests, it sometimes rejects valid nests.
8+[`^-` ("kethep")](#kethep), [`^+` ("ketlus")](#ketlus), and [`^=`
9+("kettis")](#kettis) let us adjust types without violating type constraints.
10+
11+The `nest` algorithm which tests subtyping is conservative; it never allows
12+invalid nests, it sometimes rejects valid nests.
13+
14+## `^|` "ketbar"
15+
16+Convert a gold core to an iron core (contravariant).
17+
18+#### Syntax
19+
20+One argument, fixed.
21+
22+<table>
23+<tr><th>Form</th><th>Syntax</th></tr>
24+<tr>
25+<td>Tall</td>
26+<td>
27+<pre>
28+^| p
29+</pre>
30+</td>
31+</tr>
32+<tr>
33+<td>Wide</td>
34+<td>
35+<pre>
36+^|(p)
37+</pre>
38+</td>
39+</tr>
40+<tr>
41+<td>Irregular</td>
42+<td>None.</td>
43+</tr>
44+</table>
45+
46+#### AST
1347
14−## Runes
15−
16−### `^|` "ketbar"
17−
18−`[%ktbr p=hoon]`: convert a gold core to an iron core (contravariant).
48+```hoon
49+[%ktbr p=hoon]
50+```
1951
20−##### Produces
52+#### Produces
2153
2254`p` as an iron core; crash if not a gold core.
2355
24−##### Syntax
25−
26−Regular: **1-fixed**.
27−
28−##### Discussion
56+#### Discussion
2957
3058An iron core is an opaque function (gate or door).
3159
@@ -37,7 +65,7 @@ Informally, a function fits an interface if the function has a
3765more specific result and/or a less specific argument than the
3866interface.
3967
40−##### Examples
68+#### Examples
4169
4270The prettyprinter shows the core metal (`.` gold, `|` iron):
4371
@@ -49,34 +77,68 @@ The prettyprinter shows the core metal (`.` gold, `|` iron):
4977<1|gcq [@ @n <250.yur 41.wda 374.hzt 100.kzl 1.ypj %151>]>
5078```
5179
52−### `^:` "ketcol"
80+---
81+
82+## `^:` "ketcol"
83+
84+Mold gate for type `p`.
85+
86+**Note this rune is now redundant.**
5387
54−`[%ktcl p=spec]`: mold gate for type `p`.
88+#### Syntax
5589
56−##### Produces
90+One argument, fixed.
5791
58−A gate that returns the sample value if it's of the correct type, but crashes otherwise.
92+<table>
93+<tr><th>Form</th><th>Syntax</th></tr>
94+<tr>
95+<td>Tall</td>
96+<td>
97+<pre>
98+^: p
99+</pre>
100+</td>
101+</tr>
102+<tr>
103+<td>Wide</td>
104+<td>
105+<pre>
106+^:(p)
107+</pre>
108+</td>
109+</tr>
110+<tr>
111+<td>Irregular</td>
112+<td>None.</td>
113+</tr>
114+</table>
59115
60−##### Syntax
116+#### AST
61117
62−Regular: **1-fixed**.
118+```hoon
119+[%ktcl p=spec]
120+```
121+
122+#### Produces
63123
64−##### Discussion
124+A gate that returns the sample value if it's of the correct type, but crashes
125+otherwise.
65126
66−A mold is an idempotent gate that is guaranteed to produce a noun of that type.
67−If an input value isn't of the correct type, the bunt value of that type is
68−returned. (See `^*`.)
127+#### Discussion
69128
70−`^:` is used to produce a gate that is much like a mold, except that instead of
71−producing a bunt value when the input value is of the wrong type, it crashes.
129+`^:` is used to produce a mold that crashes if its sample is of the wrong type.
130+
131+Molds used to produced their bunt value if they couldn't mold their sample. This
132+is no longer the case: molds now crash if molding fails, so **this rune is
133+redundant**.
72134
73135One may expect that `^:(path /foo)` would result in a syntax error since `^:`
74−only takes one child, but instead it will parse as `=< ^ %:(path /foo)`. Since
136+only takes one child, but instead it will parse as `=< ^ %:(path /foo)`. Since
75137`:` is the irregular syntax for `=<` this is is parsed as "get `^` (i.e. the
76138mold for cells) from a subject of `(path /foo)`", with `:` being the irregular
77139syntax for `=<`.
78140
79−##### Examples
141+#### Examples
80142
81143```
82144> ^: @
@@ -94,31 +156,60 @@ syntax for `=<`.
94156ford: %ride failed to execute:
95157```
96158
97−### `^.` "ketdot"
98−
99−`[%ktdt p=hoon q=hoon]`: typecast on value produced by passing `q` to `p`.
100−
101−##### Expands to
159+---
160+
161+## `^.` "ketdot"
162+
163+Typecast on value produced by passing `q` to `p`.
164+
165+#### Syntax
166+
167+Two arguments, fixed.
168+
169+<table>
170+<tr><th>Form</th><th>Syntax</th></tr>
171+<tr>
172+<td>Tall</td>
173+<td>
174+<pre>
175+^. p
176+q
177+</pre>
178+</td>
179+</tr>
180+<tr>
181+<td>Wide</td>
182+<td>
183+<pre>
184+^.(p q)
185+</pre>
186+</td>
187+</tr>
188+<tr>
189+<td>Irregular</td>
190+<td>None.</td>
191+</tr>
192+</table>
193+
194+#### AST
102195
103196```hoon
104−^+(%:(p q) q)
197+[%ktdt p=hoon q=hoon]
105198```
106199
107−##### Syntax
108−
109−Regular: **2-fixed**.
200+#### Expands to
110201
111202```hoon
112−^. p=hoon q=hoon
203+^+(%:(p q) q)
113204```
114205
115−##### Discussion
206+#### Discussion
116207
117208`p` produces a gate and q is any Hoon expression.
118209
119−`^.` is particularly useful when `p` is a gate that 'cleans up' the type information about some piece of data. For example, `limo` is used to turn a raw noun of the appropriate shape into a genuine list. Hence we can use `^.` to cast with `limo` and similar gates, ensuring that the product has the desired type.
210+`^.` is particularly useful when `p` is a gate that 'cleans up' the type information about some piece of data. For example, `limo` is used to turn a raw noun of the appropriate shape into a genuine list. Hence we can use `^.` to cast with `limo` and similar gates, ensuring that the product has the desired type.
120211
121−##### Examples
212+#### Examples
122213
123214```
124215> =mylist [11 22 33 ~]
@@ -135,31 +226,66 @@ mint-vain
135226~[22 33]
136227```
137228
138−### `^-` "kethep"
229+---
230+
231+## `^-` "kethep"
232+
233+Typecast by explicit type label.
234+
235+#### Syntax
236+
237+Two arguments, fixed.
238+
239+<table>
240+<tr><th>Form</th><th>Syntax</th></tr>
241+<tr>
242+<td>Tall</td>
243+<td>
244+<pre>
245+^- p
246+q
247+</pre>
248+</td>
249+</tr>
250+<tr>
251+<td>Wide</td>
252+<td>
253+<pre>
254+^-(p q)
255+</pre>
256+</td>
257+</tr>
258+<tr>
259+<td>Irregular</td>
260+<td>
261+<pre>
262+`p`q
263+</pre>
264+</td>
265+</tr>
266+</table>
267+
268+#### AST
139269
140−`[%kthp p=spec q=hoon]`: typecast by explicit type label.
270+```hoon
271+[%kthp p=spec q=hoon]
272+```
141273
142−##### Expands to
274+#### Expands to
143275
144276```hoon
145277^+(^*(p) q)
146278```
147279
148−##### Syntax
149−
150−Regular: **2-fixed**.
151−
152−Irregular: `` `foo`baz`` is `^-(foo ^-(@ baz))`.
153−
154−##### Discussion
280+#### Discussion
155281
156282It's a good practice to put a `^-` ("kethep") at the top of every arm
157−(including gates, loops, etc). This cast is strictly necessary
283+(including gates, loops, etc). This cast is strictly necessary
158284only in the presence of head recursion (otherwise you'll get a
159285`rest-loop` error, or if you really screw up spectacularly an
160286infinite loop in the compiler).
161287
162−##### Examples
288+#### Examples
163289
164290```
165291~zod:dojo> (add 90 7)
@@ -179,44 +305,103 @@ infinite loop in the compiler).
179305[~ ~.a]
180306```
181307
182−### `^+` "ketlus"
308+## `^+` "ketlus"
309+
310+Typecast by inferred type.
311+
312+#### Syntax
313+
314+Two arguments, fixed.
315+
316+<table>
317+<tr><th>Form</th><th>Syntax</th></tr>
318+<tr>
319+<td>Tall</td>
320+<td>
321+<pre>
322+^+ p
323+q
324+</pre>
325+</td>
326+</tr>
327+<tr>
328+<td>Wide</td>
329+<td>
330+<pre>
331+^+(p q)
332+</pre>
333+</td>
334+</tr>
335+<tr><td>Irregular</td><td>None.</td></tr>
336+</table>
337+
338+#### AST
183339
184−`[%ktls p=hoon q=hoon]`: typecast by inferred type.
185−
186−##### Produces
187−
188−The value of `q` with the type of `p`, if the type of `q` nests within the type of `p`. Otherwise, `nest-fail`.
340+```hoon
341+[%ktls p=hoon q=hoon]
342+```
189343
190−##### Syntax
344+#### Produces
191345
192−Regular: **2-fixed**.
346+The value of `q` with the type of `p`, if the type of `q` nests within the type
347+of `p`. Otherwise, `nest-fail`.
193348
194−##### Examples
349+#### Examples
195350
196351```
197352~zod:dojo> ^+('text' %a)
198353'a'
199354```
200355
201−### `^&` "ketpam"
356+---
202357
203−`[%ktpm p=hoon]`: convert a core to a zinc core (covariant).
358+## `^&` "ketpam"
204359
205−##### Produces
360+Convert a core to a zinc core (covariant).
206361
207−`p` as a zinc core; crash if `p` isn't a gold or zinc core.
362+#### Syntax
363+
364+One argument, fixed.
365+
366+<table>
367+<tr><th>Form</th><th>Syntax</th></tr>
368+<tr>
369+<td>Tall</td>
370+<td>
371+<pre>
372+^& p
373+</pre>
374+</td>
375+</tr>
376+<tr>
377+<td>Wide</td>
378+<td>
379+<pre>
380+^&(p)
381+</pre>
382+</td>
383+</tr>
384+<tr><td>Irregular</td><td>None.</td></tr>
385+</table>
386+
387+#### AST
208388
209−##### Syntax
389+```hoon
390+[%ktpm p=hoon]
391+```
210392
211−Regular: **1-fixed**.
393+#### Produces
394+
395+`p` as a zinc core; crash if `p` isn't a gold or zinc core.
212396
213−##### Discussion
397+#### Discussion
214398
215−A zinc core has a read-only sample and an opaque context. See [Advanced types](/docs/hoon/reference/advanced).
399+A zinc core has a read-only sample and an opaque context. See [Advanced types](/docs/hoon/reference/advanced).
216400
217−##### Examples
401+#### Examples
218402
219−The prettyprinter shows the core metal in the arm labels `1.xoz` and `1&xoz` below (`.` is gold, `&` is zinc):
403+The prettyprinter shows the core metal in the arm labels `1.xoz` and `1&xoz`
404+below (`.` is gold, `&` is zinc):
220405
221406```
222407> |=(@ 1)
@@ -251,53 +436,112 @@ ford: %slim failed:
251436ford: %ride failed to compute type:
252437```
253438
254−### `^~` "ketsig"
439+---
255440
256−`[%ktsg p=hoon]`: fold constant at compile time.
441+## `^~` "ketsig"
257442
258−##### Produces
443+Fold constant at compile time.
259444
260−`p`, folded as a constant if possible.
445+#### Syntax
261446
262−##### Syntax
447+One argument, fixed.
263448
264−Regular: **1-fixed**.
449+<table>
450+<tr><th>Form</th><th>Syntax</th></tr>
451+<tr>
452+<td>Tall</td>
453+<td>
454+<pre>
455+^~ p
456+</pre>
457+</td>
458+</tr>
459+<tr>
460+<td>Wide</td>
461+<td>
462+<pre>
463+^~(p)
464+</pre>
465+</td>
466+</tr>
467+<tr><td>Irregular</td><td>None.</td></tr>
468+</table>
265469
266−##### Examples
470+#### AST
267471
472+```hoon
473+[%ktsg p=hoon]
268474```
269−~zod:dojo> (make '|-(42)')
270−[%8 p=[%1 p=[1 42]] q=[%9 p=2 q=[%0 p=1]]]
271475
272−~zod:dojo> (make '^~(|-(42))')
273−[%1 p=42]
274−```
476+#### Produces
275477
276−### `^*` "kettar"
478+`p`, folded as a constant if possible.
277479
278−`[%kttr p=spec]`: Produce example type value.
480+#### Examples
279481
280−##### Produces
482+```
483+> (make '|-(42)')
484+[%8 p=[%1 p=[1 42]] q=[%9 p=2 q=[%0 p=1]]]
281485
282−A default value (i.e., 'bunt value') of the type `p`.
486+> (make '^~(|-(42))')
487+[%1 p=42]
488+```
283489
284−##### Syntax
490+---
491+
492+## `^*` "kettar"
493+
494+Produce example type value.
495+
496+#### Syntax
497+
498+One argument, fixed.
499+
500+<table>
501+<tr><th>Form</th><th>Syntax</th></tr>
502+<tr>
503+<td>Tall</td>
504+<td>
505+<pre>
506+^* p
507+</pre>
508+</td>
509+</tr>
510+<tr>
511+<td>Wide</td>
512+<td>
513+<pre>
514+^*(p)
515+</pre>
516+</td>
517+</tr>
518+<tr>
519+<td>Irregular</td>
520+<td>
521+<pre>
522+*p
523+</pre>
524+</td>
525+</tr>
526+</table>
527+
528+`p` is any structure expression.
285529
286−Regular: **1-fixed**.
530+#### AST
287531
288532```hoon
289−^* p=spec
533+[%kttr p=spec]
290534```
291535
292−Irregular: `*p`.
536+#### Produces
293537
294−`p` is any structure expression.
538+A default value (i.e., 'bunt value') of the type `p`.
295539
296−##### Examples
540+#### Examples
297541
298542Regular:
299543
300−```hoon
544+```
301545> ^* @
3025460
303547
@@ -313,7 +557,7 @@ Regular:
313557
314558Irregular:
315559
316−```hoon
560+```
317561> *@
3185620
319563
@@ -324,55 +568,119 @@ Irregular:
324568""
325569```
326570
327−### `^=` "kettis"
328−
329−`[%ktts p=skin q=hoon]`: Bind name to a value.
330−
331−##### Produces
332−
333−If `p` is a term, the product `q` with type `[%face p q]`. `p`
334−may also be a tuple of terms, or a term-skin pair; the type of
335−`q` must divide evenly into cells to match it.
571+---
572+
573+## `^=` "kettis"
574+
575+Bind name to a value.
576+
577+#### Syntax
578+
579+Two arguments, fixed.
580+
581+<table>
582+<tr><th>Form</th><th>Syntax</th></tr>
583+<tr>
584+<td>Tall</td>
585+<td>
586+<pre>
587+^= p
588+q
589+</pre>
590+</td>
591+</tr>
592+<tr>
593+<td>Wide</td>
594+<td>
595+<pre>
596+^=(p q)
597+</pre>
598+</td>
599+</tr>
600+<tr>
601+<td>Irregular</td>
602+<td>
603+<pre>
604+p=q
605+</pre>
606+</td>
607+</tr>
608+</table>
609+
610+#### AST
336611
337−##### Syntax
612+```hoon
613+[%ktts p=skin q=hoon]
614+```
338615
339−Regular: **2-fixed**.
616+#### Produces
340617
341−Irregular: `foo=baz` is `^=(foo baz)`.
618+If `p` is a term, the product `q` with type `[%face p q]`. `p` may also be a
619+tuple of terms, or a term-skin pair; the type of `q` must divide evenly into
620+cells to match it.
342621
343−##### Examples
622+#### Examples
344623
345624```
346−~zod:dojo> a=1
625+> a=1
347626a=1
348627
349−~zod:dojo> ^= a
350− 1
628+> ^= a
629+ 1
351630a=1
352631
353−~zod:dojo> ^=(a 1)
632+> ^=(a 1)
354633a=1
355634
356−~zod:dojo> [b c d]=[1 2 3 4]
635+> [b c d]=[1 2 3 4]
357636[b=1 c=2 d=[3 4]]
358637
359−~zod:dojo> [b c d=[x y]]=[1 2 3 4]
638+> [b c d=[x y]]=[1 2 3 4]
360639[b=1 c=2 d=[x=3 y=4]]
361640```
362641
363−### `^?` "ketwut"
642+---
364643
365−`[%ktwt p=hoon]`: convert any core to a lead core (bivariant).
644+## `^?` "ketwut"
366645
367−##### Produces
646+Convert any core to a lead core (bivariant).
368647
369−`p` as a lead core; crash if not a core.
648+#### Syntax
370649
371−##### Syntax
650+One argument, fixed.
372651
373−Regular: **1-fixed**.
652+<table>
653+<tr><th>Form</th><th>Syntax</th></tr>
654+<tr>
655+<td>Tall</td>
656+<td>
657+<pre>
658+^? p
659+</pre>
660+</td>
661+</tr>
662+<tr>
663+<td>Wide</td>
664+<td>
665+<pre>
666+^?(p)
667+</pre>
668+</td>
669+</tr>
670+<tr><td>Irregular</td><td>None.</td></tr>
671+</table>
374672
375−##### Discussion
673+#### AST
674+
675+```hoon
676+[%ktwt p=hoon]
677+```
678+
679+#### Produces
680+
681+`p` as a lead core; crash if not a core.
682+
683+#### Discussion
376684
377685A lead core is an opaque generator; the payload can't be read or
378686written.
@@ -383,14 +691,14 @@ Theorem: if type `x` nests within type `a`, a lead core producing
383691Informally, a more specific generator can be used as a less
384692specific generator.
385693
386−##### Examples
694+#### Examples
387695
388696The prettyprinter shows the core metal (`.` gold, `?` lead):
389697
390698```
391−~zod:dojo> |=(@ 1)
699+> |=(@ 1)
392700<1.gcq [@ @n <250.yur 41.wda 374.hzt 100.kzl 1.ypj %151>]>
393701
394−~zod:dojo> ^?(|=(@ 1))
702+> ^?(|=(@ 1))
395703<1?gcq [@ @n <250.yur 41.wda 374.hzt 100.kzl 1.ypj %151>]>
396704```