@@ -4,28 +4,56 @@ weight = 11
4template = "doc.html"
4template = "doc.html"
5aliases = ["docs/reference/hoon-expressions/rune/ket/"]
5aliases = ["docs/reference/hoon-expressions/rune/ket/"]
7−[`^-` ("kethep")](#kethep), [`^+` ("ketlus")](#ketlus), and
8−[`^=` ("kettis")](#kettis) let us adjust types without violating type
8+[`^-` ("kethep")](#kethep), [`^+` ("ketlus")](#ketlus), and [`^=`
9+("kettis")](#kettis) let us adjust types without violating type constraints.
11−The `nest` algorithm which tests subtyping is conservative;
11+The `nest` algorithm which tests subtyping is conservative; it never allows
12−it never allows invalid nests, it sometimes rejects valid nests.
12+invalid nests, it sometimes rejects valid nests.
16+Convert a gold core to an iron core (contravariant).
23+<tr><th>Form</th><th>Syntax</th></tr>
16−### `^|` "ketbar"
50+```
18−`[%ktbr p=hoon]`: convert a gold core to an iron core (contravariant).
20−##### Produces
52+#### Produces
22`p` as an iron core; crash if not a gold core.
54`p` as an iron core; crash if not a gold core.
28−##### Discussion
56+#### Discussion
30An iron core is an opaque function (gate or door).
58An iron core is an opaque function (gate or door).
@@ -37,7 +65,7 @@ Informally, a function fits an interface if the function has a
37more specific result and/or a less specific argument than the
65more specific result and/or a less specific argument than the
40−##### Examples
68+#### Examples
42The prettyprinter shows the core metal (`.` gold, `|` iron):
70The prettyprinter shows the core metal (`.` gold, `|` iron):
@@ -49,34 +77,68 @@ The prettyprinter shows the core metal (`.` gold, `|` iron):
49<1|gcq [@ @n <250.yur 41.wda 374.hzt 100.kzl 1.ypj %151>]>
77<1|gcq [@ @n <250.yur 41.wda 374.hzt 100.kzl 1.ypj %151>]>
52−### `^:` "ketcol"
82+## `^:` "ketcol"
84+Mold gate for type `p`.
86+**Note this rune is now redundant.**
54−`[%ktcl p=spec]`: mold gate for type `p`.
88+#### Syntax
56−##### Produces
90+One argument, fixed.
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>
60−##### Syntax
116+#### AST
62−Regular: **1-fixed**.
118+```hoon
64−##### Discussion
124+A gate that returns the sample value if it's of the correct type, but crashes
66−A mold is an idempotent gate that is guaranteed to produce a noun of that type.
127+#### Discussion
67−If an input value isn't of the correct type, the bunt value of that type is
70−`^:` is used to produce a gate that is much like a mold, except that instead of
129+`^:` is used to produce a mold that crashes if its sample is of the wrong type.
71−producing a bunt value when the input value is of the wrong type, it crashes.
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
73One may expect that `^:(path /foo)` would result in a syntax error since `^:`
135One 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
75`:` is the irregular syntax for `=<` this is is parsed as "get `^` (i.e. the
137`:` is the irregular syntax for `=<` this is is parsed as "get `^` (i.e. the
76mold for cells) from a subject of `(path /foo)`", with `:` being the irregular
138mold for cells) from a subject of `(path /foo)`", with `:` being the irregular
77syntax for `=<`.
139syntax for `=<`.
79−##### Examples
141+#### Examples
@@ -94,31 +156,60 @@ syntax for `=<`.
94ford: %ride failed to execute:
156ford: %ride failed to execute:
97−### `^.` "ketdot"
161+## `^.` "ketdot"
99−`[%ktdt p=hoon q=hoon]`: typecast on value produced by passing `q` to `p`.
163+Typecast on value produced by passing `q` to `p`.
101−##### Expands to
165+#### Syntax
167+Two arguments, fixed.
170+<tr><th>Form</th><th>Syntax</th></tr>
104−^+(%:(p q) q)
197+[%ktdt p=hoon q=hoon]
107−##### Syntax
200+#### Expands to
109−Regular: **2-fixed**.
112−^. p=hoon q=hoon
203+^+(%:(p q) q)
115−##### Discussion
206+#### Discussion
117`p` produces a gate and q is any Hoon expression.
208`p` produces a gate and q is any Hoon expression.
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.
121−##### Examples
212+#### Examples
124> =mylist [11 22 33 ~]
215> =mylist [11 22 33 ~]
@@ -135,31 +226,66 @@ mint-vain
138−### `^-` "kethep"
231+## `^-` "kethep"
233+Typecast by explicit type label.
237+Two arguments, fixed.
240+<tr><th>Form</th><th>Syntax</th></tr>
140−`[%kthp p=spec q=hoon]`: typecast by explicit type label.
271+[%kthp p=spec q=hoon]
142−##### Expands to
274+#### Expands to
145^+(^*(p) q)
277^+(^*(p) q)
150−Regular: **2-fixed**.
152−Irregular: `` `foo`baz`` is `^-(foo ^-(@ baz))`.
154−##### Discussion
280+#### Discussion
156It's a good practice to put a `^-` ("kethep") at the top of every arm
282It'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
158only in the presence of head recursion (otherwise you'll get a
284only in the presence of head recursion (otherwise you'll get a
159`rest-loop` error, or if you really screw up spectacularly an
285`rest-loop` error, or if you really screw up spectacularly an
160infinite loop in the compiler).
286infinite loop in the compiler).
162−##### Examples
288+#### Examples
165~zod:dojo> (add 90 7)
291~zod:dojo> (add 90 7)
@@ -179,44 +305,103 @@ infinite loop in the compiler).
182−### `^+` "ketlus"
308+## `^+` "ketlus"
310+Typecast by inferred type.
314+Two arguments, fixed.
317+<tr><th>Form</th><th>Syntax</th></tr>
335+<tr><td>Irregular</td><td>None.</td></tr>
184−`[%ktls p=hoon q=hoon]`: typecast by inferred type.
341+[%ktls p=hoon q=hoon]
188−The value of `q` with the type of `p`, if the type of `q` nests within the type of `p`. Otherwise, `nest-fail`.
190−##### Syntax
344+#### Produces
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`.
194−##### Examples
349+#### Examples
197~zod:dojo> ^+('text' %a)
352~zod:dojo> ^+('text' %a)
201−### `^&` "ketpam"
356+---
203−`[%ktpm p=hoon]`: convert a core to a zinc core (covariant).
358+## `^&` "ketpam"
205−##### Produces
360+Convert a core to a zinc core (covariant).
207−`p` as a zinc core; crash if `p` isn't a gold or zinc core.
362+#### Syntax
367+<tr><th>Form</th><th>Syntax</th></tr>
384+<tr><td>Irregular</td><td>None.</td></tr>
209−##### Syntax
389+```hoon
211−Regular: **1-fixed**.
393+#### Produces
395+`p` as a zinc core; crash if `p` isn't a gold or zinc core.
213−##### Discussion
397+#### Discussion
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).
217−##### Examples
401+#### Examples
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):
@@ -251,53 +436,112 @@ ford: %slim failed:
251ford: %ride failed to compute type:
436ford: %ride failed to compute type:
254−### `^~` "ketsig"
439+---
256−`[%ktsg p=hoon]`: fold constant at compile time.
441+## `^~` "ketsig"
258−##### Produces
443+Fold constant at compile time.
260−`p`, folded as a constant if possible.
445+#### Syntax
262−##### Syntax
447+One argument, fixed.
264−Regular: **1-fixed**.
449+<table>
450+<tr><th>Form</th><th>Syntax</th></tr>
467+<tr><td>Irregular</td><td>None.</td></tr>
266−##### Examples
470+#### AST
269−~zod:dojo> (make '|-(42)')
270−[%8 p=[%1 p=[1 42]] q=[%9 p=2 q=[%0 p=1]]]
272−~zod:dojo> (make '^~(|-(42))')
476+#### Produces
276−### `^*` "kettar"
478+`p`, folded as a constant if possible.
278−`[%kttr p=spec]`: Produce example type value.
480+#### Examples
280−##### Produces
482+```
484+[%8 p=[%1 p=[1 42]] q=[%9 p=2 q=[%0 p=1]]]
282−A default value (i.e., 'bunt value') of the type `p`.
486+> (make '^~(|-(42))')
494+Produce example type value.
284−##### Syntax
496+#### Syntax
501+<tr><th>Form</th><th>Syntax</th></tr>
528+`p` is any structure expression.
286−Regular: **1-fixed**.
530+#### AST
289−^* p=spec
533+[%kttr p=spec]
292−Irregular: `*p`.
536+#### Produces
294−`p` is any structure expression.
538+A default value (i.e., 'bunt value') of the type `p`.
296−##### Examples
540+#### Examples
@@ -313,7 +557,7 @@ Regular:
314Irregular:
558Irregular:
@@ -324,55 +568,119 @@ Irregular:
327−### `^=` "kettis"
573+## `^=` "kettis"
329−`[%ktts p=skin q=hoon]`: Bind name to a value.
575+Bind name to a value.
331−##### Produces
577+#### Syntax
333−If `p` is a term, the product `q` with type `[%face p q]`. `p`
579+Two arguments, fixed.
334−may also be a tuple of terms, or a term-skin pair; the type of
580+
335−`q` must divide evenly into cells to match it.
581+<table>
582+<tr><th>Form</th><th>Syntax</th></tr>
337−##### Syntax
612+```hoon
613+[%ktts p=skin q=hoon]
339−Regular: **2-fixed**.
616+#### Produces
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
343−##### Examples
622+#### Examples
346−~zod:dojo> a=1
625+> a=1
349−~zod:dojo> ^= a
628+> ^= a
353−~zod:dojo> ^=(a 1)
632+> ^=(a 1)
356−~zod:dojo> [b c d]=[1 2 3 4]
635+> [b c d]=[1 2 3 4]
357[b=1 c=2 d=[3 4]]
636[b=1 c=2 d=[3 4]]
359−~zod:dojo> [b c d=[x y]]=[1 2 3 4]
638+> [b c d=[x y]]=[1 2 3 4]
360[b=1 c=2 d=[x=3 y=4]]
639[b=1 c=2 d=[x=3 y=4]]
363−### `^?` "ketwut"
642+---
365−`[%ktwt p=hoon]`: convert any core to a lead core (bivariant).
644+## `^?` "ketwut"
367−##### Produces
646+Convert any core to a lead core (bivariant).
369−`p` as a lead core; crash if not a core.
648+#### Syntax
371−##### Syntax
650+One argument, fixed.
373−Regular: **1-fixed**.
652+<table>
653+<tr><th>Form</th><th>Syntax</th></tr>
670+<tr><td>Irregular</td><td>None.</td></tr>
681+`p` as a lead core; crash if not a core.
375−##### Discussion
683+#### Discussion
377A lead core is an opaque generator; the payload can't be read or
685A lead core is an opaque generator; the payload can't be read or
@@ -383,14 +691,14 @@ Theorem: if type `x` nests within type `a`, a lead core producing
383Informally, a more specific generator can be used as a less
691Informally, a more specific generator can be used as a less
384specific generator.
692specific generator.
386−##### Examples
694+#### Examples
388The prettyprinter shows the core metal (`.` gold, `?` lead):
696The prettyprinter shows the core metal (`.` gold, `?` lead):
391−~zod:dojo> |=(@ 1)
699+> |=(@ 1)
392<1.gcq [@ @n <250.yur 41.wda 374.hzt 100.kzl 1.ypj %151>]>
700<1.gcq [@ @n <250.yur 41.wda 374.hzt 100.kzl 1.ypj %151>]>
394−~zod:dojo> ^?(|=(@ 1))
702+> ^?(|=(@ 1))
395<1?gcq [@ @n <250.yur 41.wda 374.hzt 100.kzl 1.ypj %151>]>
703<1?gcq [@ @n <250.yur 41.wda 374.hzt 100.kzl 1.ypj %151>]>