on master help sign in
More revisions to the Basic Type doc

No set theory jokes this time.

commit6dba9ba75759945db72c8c19e80684486a569d3a authorJoshua Reagan <joshuareagan@users.noreply.github.com> dateTue 12 Dec 2017, 08:57 (9 years ago) parentaa85158
1 file changed+35−25
docs/hoon/basic.md+35−25
docs/hoon/basic.md+35−25
@@ -12,9 +12,9 @@ defining the data type of a Hoon expression. Instead, the compiler
1212infers the type of a Hoon expression by calculating the range of
1313possible values of that expression.
1414
15−Working with a type in Hoon requires the use of a `mold`. Each
16−type is defined by a mold. To define a custom type, you must create
17−a custom mold.
15+Working with a type in Hoon normally requires the use of a `mold`.
16+Each type is defined by a mold. To define a custom type, you must
17+create a custom mold.
1818
1919## Molds
2020
@@ -24,40 +24,45 @@ function *f*, and *f* returns an object from the range. In Hoon we
2424can think of a `gate` as a function, where the gate's `sample` is
2525its argument.
2626
27−A `mold` is an idempotent function (i.e., gate) that takes any noun
28−as its input (i.e., its domain is the set of all nouns). An
29−idempotent function *f* is one such that, if *f(x)* terminates,
30−*f(x) = f(f(x))*. The product range of a mold is the type defined
31−by that mold. That is, each mold's type is the set of possible
32−outputs of that mold.
27+A `mold` is an idempotent function whose domain is the set of all
28+nouns. (That is, it's an idempotent gate that takes any noun for its
29+sample.) An idempotent function *f* is one such that, if *f(x)*
30+terminates, *f(x) = f(f(x))*. The product range of a mold is the
31+type defined by that mold. That is, each mold's type is the set of
32+possible outputs of that mold.
3333
3434Essentially, molds are constructor functions. You can pass a mold
3535any data you like, and the product is guaranteed be of the type
3636defined by that mold. Molds are the perfect tool for validating
37−untrusted foreign data: just call the relevant mold with that data.
38−But this use case is unusual for beginners; otherwise you shouldn't
39−call molds directly.
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
41+is unusual for beginners; otherwise you shouldn't call molds
42+directly.
4043
4144More frequently, molds are used when we want to `cast`. We use a
4245cast when we want the Hoon compiler's type-checker to test whether
4346a Hoon expression is guaranteed to evaluate to a product of the
4447desired 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
46−gate.
48+`nest-fail` crash. Proper Hoon code will include a cast for the
49+product type of each gate.
4750
4851The `^` family of runes is for casting. In particular, `^-` allows
4952us to cast with a mold. For example, we can cast for an `atom` using
5053the `@` mold as follows:
5154
5255```
53−^-(@ 17)
56+^- @
57+17
5458```
5559
5660Evaluating the above in `dojo` should return 17, because 17 is of
5761the type `atom`. On the other hand,
5862
5963```
60−^-(@ [17 18])
64+^- @
65+[17 18]
6166```
6267
6368...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.)
6974
7075## `type`: a set of types
7176
72−Below is the mold for `type`, written in Hoon. This mold's range is
73−the set of all types. (Don't let yourself get too dizzy thinking
74−about it! Strictly speaking, the range is of trees of type-*labels*
75−used by the compiler's type-checker. We don't mess around with
76−set-theoretic paradoxes.)
77+Below is the mold for `type`, which effectively defines all the types
78+available in Hoon.
79+
80+Strictly speaking, this mold defines the tree data structure the Hoon
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
84+odds and ends.
7785
7886You haven't seen this syntax before, and we haven't explained it yet;
7987just treat it as pseudocode.
@@ -96,10 +104,9 @@ section.
96104 ==
97105```
98106
99−If a type is an atom, it's labelled with either the atomic string
100−`%noun` or `%void`; if a cell, it's labelled with a tuple with one of
101−the heads `%atom`, `%cell`, `%core`, etc. We'll go through each of
102−these cases below.
107+If the `type`-tree is an atom, it's either a `%noun` or a `%void`; if
108+the `type`-tree is a cell, it's a tuple with one of the heads `%atom`,
109+`%cell`, `%core`, etc. We'll go through each of these cases below.
103110
104111### `?($noun $void)`
105112
@@ -123,6 +130,9 @@ A `%hold` type, with type `p` and hoon `q`, is a lazy reference
123130to the type of `(mint p q)`. In English, it means: "the type of
124131the product when we compile `q` against subject `p`."
125132
133+Note that this means we can have parsed Hoon AST data in the
134+`type`-tree.
135+
126136### `{$face p/term q/type}`
127137
128138A `[%face p/term q/type]` wraps the label `p` around the type