@@ -12,9 +12,9 @@ defining the data type of a Hoon expression. Instead, the compiler
12infers the type of a Hoon expression by calculating the range of
12infers the type of a Hoon expression by calculating the range of
13possible values of that expression.
13possible values of that expression.
15−Working with a type in Hoon requires the use of a `mold`. Each
15+Working with a type in Hoon normally requires the use of a `mold`.
16−type is defined by a mold. To define a custom type, you must create
16+Each type is defined by a mold. To define a custom type, you must
17−a custom mold.
17+create a custom mold.
@@ -24,40 +24,45 @@ function *f*, and *f* returns an object from the range. In Hoon we
24can think of a `gate` as a function, where the gate's `sample` is
24can think of a `gate` as a function, where the gate's `sample` is
25its argument.
25its argument.
27−A `mold` is an idempotent function (i.e., gate) that takes any noun
27+A `mold` is an idempotent function whose domain is the set of all
28−as its input (i.e., its domain is the set of all nouns). An
28+nouns. (That is, it's an idempotent gate that takes any noun for its
29−idempotent function *f* is one such that, if *f(x)* terminates,
29+sample.) An idempotent function *f* is one such that, if *f(x)*
30−*f(x) = f(f(x))*. The product range of a mold is the type defined
30+terminates, *f(x) = f(f(x))*. The product range of a mold is the
31−by that mold. That is, each mold's type is the set of possible
31+type defined by that mold. That is, each mold's type is the set of
32−outputs of that mold.
32+possible outputs of that mold.
34Essentially, molds are constructor functions. You can pass a mold
34Essentially, molds are constructor functions. You can pass a mold
35any data you like, and the product is guaranteed be of the type
35any data you like, and the product is guaranteed be of the type
36defined by that mold. Molds are the perfect tool for validating
36defined by that mold. Molds are the perfect tool for validating
37−untrusted foreign data: just call the relevant mold with that data.
37+untrusted foreign data. Just call the relevant mold with that data
38+and check that the input equals the output. This is one reason why
39+molds must be idempotent; if the untrusted data is of the correct
40+type, passing it to the mold shouldn't change it. But this use case
38−But this use case is unusual for beginners; otherwise you shouldn't
41+is unusual for beginners; otherwise you shouldn't call molds
39−call molds directly.
42+directly.
41More frequently, molds are used when we want to `cast`. We use a
44More frequently, molds are used when we want to `cast`. We use a
42cast when we want the Hoon compiler's type-checker to test whether
45cast when we want the Hoon compiler's type-checker to test whether
43a Hoon expression is guaranteed to evaluate to a product of the
46a Hoon expression is guaranteed to evaluate to a product of the
44desired type. If it isn't, then the compiler will halt with a
47desired type. If it isn't, then the compiler will halt with a
45−`nest-fail` crash. Proper Hoon code will include a cast for each
48+`nest-fail` crash. Proper Hoon code will include a cast for the
46−gate.
49+product type of each gate.
48The `^` family of runes is for casting. In particular, `^-` allows
51The `^` family of runes is for casting. In particular, `^-` allows
49us to cast with a mold. For example, we can cast for an `atom` using
52us to cast with a mold. For example, we can cast for an `atom` using
50the `@` mold as follows:
53the `@` mold as follows:
56Evaluating the above in `dojo` should return 17, because 17 is of
60Evaluating the above in `dojo` should return 17, because 17 is of
57the type `atom`. On the other hand,
61the type `atom`. On the other hand,
60−^-(@ [17 18])
65+[17 18]
63...this should result in a `nest-fail`, because `[17 18]` is a cell,
68...this should result in a `nest-fail`, because `[17 18]` is a cell,
@@ -69,11 +74,14 @@ building molds. (Also check out the irregular `,` operator.)
70## `type`: a set of types
75## `type`: a set of types
72−Below is the mold for `type`, written in Hoon. This mold's range is
77+Below is the mold for `type`, which effectively defines all the types
73−the set of all types. (Don't let yourself get too dizzy thinking
78+available in Hoon.
74−about it! Strictly speaking, the range is of trees of type-*labels*
79+
75−used by the compiler's type-checker. We don't mess around with
80+Strictly speaking, this mold defines the tree data structure the Hoon
76−set-theoretic paradoxes.)
81+compiler uses to represent type information. It has a label for each
82+of the base types, and it's recursive, so a complex type is
83+represented as a nested combination of base types and various other
78You haven't seen this syntax before, and we haven't explained it yet;
86You haven't seen this syntax before, and we haven't explained it yet;
79just treat it as pseudocode.
87just treat it as pseudocode.
@@ -96,10 +104,9 @@ section.
99−If a type is an atom, it's labelled with either the atomic string
107+If the `type`-tree is an atom, it's either a `%noun` or a `%void`; if
100−`%noun` or `%void`; if a cell, it's labelled with a tuple with one of
108+the `type`-tree is a cell, it's a tuple with one of the heads `%atom`,
101−the heads `%atom`, `%cell`, `%core`, etc. We'll go through each of
109+`%cell`, `%core`, etc. We'll go through each of these cases below.
104### `?($noun $void)`
111### `?($noun $void)`
@@ -123,6 +130,9 @@ A `%hold` type, with type `p` and hoon `q`, is a lazy reference
123to the type of `(mint p q)`. In English, it means: "the type of
130to the type of `(mint p q)`. In English, it means: "the type of
124the product when we compile `q` against subject `p`."
131the product when we compile `q` against subject `p`."
133+Note that this means we can have parsed Hoon AST data in the
126### `{$face p/term q/type}`
136### `{$face p/term q/type}`
128A `[%face p/term q/type]` wraps the label `p` around the type
138A `[%face p/term q/type]` wraps the label `p` around the type