@@ -7,85 +7,125 @@ title: Basic types
77
88# Basic types
99
10−A `span` is a set of nouns and an interpretation of these nouns.
11−Officially, we don't use the word "type" in Hoon. But if we had
12−to say "type," it would mean `span`.
10+A Hoon `type` is a set of nouns. There is no syntax for directly
11+defining the data type of a Hoon expression. Instead, the compiler
12+infers the type of a Hoon expression by calculating the range of
13+possible values of that expression.
14+
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.
18+
19+## Molds
20+
21+A mathematical function is a mapping from one set (the domain) to
22+another (the range). Pass an object from the domain to some
23+function *f*, and *f* returns an object from the range. In Hoon we
24+can think of a `gate` as a function, where the gate's `sample` is
25+its argument.
26+
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.
33+
34+Essentially, molds are constructor functions. You can pass a mold
35+any data you like, and the product is guaranteed be of the type
36+defined 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.
40+
41+More frequently, molds are used when we want to `cast`. We use a
42+cast when we want the Hoon compiler's type-checker to test whether
43+a Hoon expression is guaranteed to evaluate to a product of the
44+desired 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.
47+
48+The `^` family of runes is for casting. In particular, `^-` allows
49+us to cast with a mold. For example, we can cast for an `atom` using
50+the `@` mold as follows:
1351
14−## Type, span and mold
15−
16−There is no Hoon syntax for a span. The programmer never defines
17−a span explicitly. It is always produced as the inferred range
18−of an expression (`twig`).
52+```
53+^-(@ 17)
54+```
1955
20−But we still need simple, well-formed expressions that produce
21−regular and well-shaped ranges, for three reasons.
56+Evaluating the above in `dojo` should return 17, because 17 is of
57+the type `atom`. On the other hand,
2258
23−First: in most cases, this trivial generator should be much
24−simpler than the computation itself. Casting the actual result
25−to its ideal shape makes sure we know what we're building.
59+```
60+^-(@ [17 18])
61+```
2662
27−Second: we can define a standard form for such generators, and
28−the standard form is useful. The standard form is a constructor
29−function, or *mold*.
63+...this should result in a `nest-fail`, because `[17 18]` is a cell,
64+not an atom.
3065
31−A mold is an idempotent function (`gate`), accepting any noun.
32−(An idempotent function is one such that *f(f(x))* equals *f(x)*
33−if *f(x)* terminates.) The product range of the function is the
34−span, or *icon*, of the mold.
66+See the documentation on the `^` family of runes for more information
67+on casts. See the documentation on the `$` family of runes for
68+building molds. (Also check out the irregular `,` operator.)
3569
36−Usually we use molds purely in the first sense: as an abstract
37−definition of a noun. Don't actually call a mold unless you're
38−actually validating untrusted foreign data. As a beginner,
39−hopefully you aren't!
70+## `type`: a set of types
4071
41−## `span`: a set of nouns
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.)
4277
43−Below is the mold for `span`. You haven't seen this syntax before,
44−and we haven't explained it yet; just treat it as pseudocode.
78+You haven't seen this syntax before, and we haven't explained it yet;
79+just treat it as pseudocode.
4580
46−This is a slightly simplified version of `span`. We undo and explain the
47−simplifications in the [advanced types](../advanced) section.
81+This is a slightly simplified version of `type`. We undo and
82+explain the simplifications in the [advanced types](../advanced)
83+section.
4884
4985```
5086++ term @tas
51−++ span
87+++ type
5288 $@ $? $noun
5389 $void
5490 == $% {$atom p/term q/(unit atom)}
55− {$cell p/span q/span}
56− {$core p/span q/(map term twig)}
57− {$face p/term q/span}
58− {$fork p/(set span)}
59− {$hold p/span q/twig}
91+ {$cell p/type q/type}
92+ {$core p/type q/(map term hoon)}
93+ {$face p/term q/type}
94+ {$fork p/(set type)}
95+ {$hold p/type q/hoon}
6096 ==
6197```
6298
63−If a span is an atom, it's either the atomic string `noun` or
64−`void`; if a cell, it's a tuple with one of the heads `atom`,
65−`cell`, `core`, etc. We'll go through each of these cases below.
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.
66103
67104### `?($noun $void)`
68105
69−`$noun` is the set of all nouns. `$void` is the set of no nouns.
106+`%noun` is the label for the set of all nouns. `%void` is the label
107+for the empty set.
108+
109+(For now, don't worry too much about the switch from `$` to `%`.)
70110
71−### `{$cell p/span q/span}`
111+### `{$cell p/type q/type}`
72112
73−`{$cell p/span q/span}` is the set of all cells with head `p` and
113+`[%cell p/type q/type]` is for the set of all cells with head `p` and
74114tail `q`.
75115
76−### `{$fork p/(set span)}`
116+### `{$fork p/(set type)}`
77117
78−`{$fork p/(set span)}` is the union of all spans in the set `p`.
118+`[%fork p/(set type)]` is for the union of all types in the set `p`.
79119
80−### `{$hold p/span q/twig}`
120+### `{$hold p/type q/hoon}`
81121
82−A `$hold` span, with span `p` and twig `q`, is a lazy reference
83−to the span of `(mint p q)`. In English, it means: "the type of
122+A `%hold` type, with type `p` and hoon `q`, is a lazy reference
123+to the type of `(mint p q)`. In English, it means: "the type of
84124the product when we compile `q` against subject `p`."
85125
86−### `{$face p/term q/span}`
126+### `{$face p/term q/type}`
87127
88−A `{$face p/term q/span}` wraps the label `p` around the span
128+A `[%face p/term q/type]` wraps the label `p` around the type
89129`q`. `p` is a `term` or `@tas`, an atomic ASCII string which
90130obeys symbol rules: lowercase and digit only, infix hyphen,
91131first character must be lowercase.
@@ -95,10 +135,10 @@ nontrivial.
95135
96136### `{%atom p/term q/(unit atom))}`
97137
98−An `$atom` is an atom, with two twists. `q` is a `unit`, Hoon's
138+`%atom` is for an atom, with two twists. `q` is a `unit`, Hoon's
99139equivalent of a nullable pointer or a Haskell `Maybe`. If `q`
100−is `~`, null, the span is *warm*; any atom is in the span.
101−If `q` is `[~ x]`, where `x` is any atom, the span is *cold*;
140+is `~`, null, the type is *warm*; any atom is in the type.
141+If `q` is `[~ x]`, where `x` is any atom, the type is *cold*;
102142its only legal value is the constant `x`.
103143
104144`p` in the atom is a terminal used as an *aura*, or soft atom
@@ -125,7 +165,6 @@ here are some conventions bound to constant syntax:
125165@d date
126166 @da absolute date
127167 @dr relative date (ie, timespan)
128−@f yes or no (inverse boolean)
129168@n nil
130169@p phonemic base (plot)
131170@r IEEE floating-point
@@ -155,14 +194,14 @@ statically, by casting through the empty aura `@`. Hoon is not
155194dependently typed and can't statically enforce data constraints
156195(for example, it can't enforce that a `@tas` is really a symbol).
157196
158−### `{$core p/span q/(map term span)}`
197+### `{$core p/type q/(map term type)}`
159198
160−A `$core` is a code-data cell. The data (or *payload*) is the
161−tail; the code (or *battery*) is the head. `p`, a span, is the
162−span of the payload. `q`, a name-twig table, is the source code
199+`%core` is for a code-data cell. The data (or *payload*) is the
200+tail; the code (or *battery*) is the head. `p`, a type, is the
201+type of the payload. `q`, a name-hoon table, is the source code
163202for the battery.
164203
165−Each twig in the battery source is compiled to a formula, with
204+Each hoon in the battery source is compiled to a formula, with
166205the core itself as the subject. The battery is a tree of these
167206formulas, or *arms*. An arm is a computed attribute against its
168207core.