@@ -7,85 +7,125 @@ title: Basic types
8# Basic types
8# Basic types
10−A `span` is a set of nouns and an interpretation of these nouns.
10+A Hoon `type` is a set of nouns. There is no syntax for directly
11−Officially, we don't use the word "type" in Hoon. But if we had
11+defining the data type of a Hoon expression. Instead, the compiler
12−to say "type," it would mean `span`.
12+infers the type of a Hoon expression by calculating the range of
13+possible values of that expression.
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
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
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
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
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
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:
14−## Type, span and mold
52+```
16−There is no Hoon syntax for a span. The programmer never defines
54+```
17−a span explicitly. It is always produced as the inferred range
18−of an expression (`twig`).
20−But we still need simple, well-formed expressions that produce
56+Evaluating the above in `dojo` should return 17, because 17 is of
21−regular and well-shaped ranges, for three reasons.
57+the type `atom`. On the other hand,
23−First: in most cases, this trivial generator should be much
59+```
24−simpler than the computation itself. Casting the actual result
60+^-(@ [17 18])
25−to its ideal shape makes sure we know what we're building.
61+```
27−Second: we can define a standard form for such generators, and
63+...this should result in a `nest-fail`, because `[17 18]` is a cell,
28−the standard form is useful. The standard form is a constructor
64+not an atom.
31−A mold is an idempotent function (`gate`), accepting any noun.
66+See the documentation on the `^` family of runes for more information
32−(An idempotent function is one such that *f(f(x))* equals *f(x)*
67+on casts. See the documentation on the `$` family of runes for
33−if *f(x)* terminates.) The product range of the function is the
68+building molds. (Also check out the irregular `,` operator.)
34−span, or *icon*, of the mold.
36−Usually we use molds purely in the first sense: as an abstract
70+## `type`: a set of types
37−definition of a noun. Don't actually call a mold unless you're
38−actually validating untrusted foreign data. As a beginner,
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.)
43−Below is the mold for `span`. You haven't seen this syntax before,
78+You haven't seen this syntax before, and we haven't explained it yet;
44−and we haven't explained it yet; just treat it as pseudocode.
79+just treat it as pseudocode.
46−This is a slightly simplified version of `span`. We undo and explain the
81+This is a slightly simplified version of `type`. We undo and
47−simplifications in the [advanced types](../advanced) section.
82+explain the simplifications in the [advanced types](../advanced)
50++ term @tas
86++ term @tas
52 $@ $? $noun
88 $@ $? $noun
54 == $% {$atom p/term q/(unit atom)}
90 == $% {$atom p/term q/(unit atom)}
55− {$cell p/span q/span}
91+ {$cell p/type q/type}
56− {$core p/span q/(map term twig)}
92+ {$core p/type q/(map term hoon)}
57− {$face p/term q/span}
93+ {$face p/term q/type}
58− {$fork p/(set span)}
94+ {$fork p/(set type)}
59− {$hold p/span q/twig}
95+ {$hold p/type q/hoon}
63−If a span is an atom, it's either the atomic string `noun` or
99+If a type is an atom, it's labelled with either the atomic string
64−`void`; if a cell, it's a tuple with one of the heads `atom`,
100+`%noun` or `%void`; if a cell, it's labelled with a tuple with one of
65−`cell`, `core`, etc. We'll go through each of these cases below.
101+the heads `%atom`, `%cell`, `%core`, etc. We'll go through each of
67### `?($noun $void)`
104### `?($noun $void)`
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
109+(For now, don't worry too much about the switch from `$` to `%`.)
71−### `{$cell p/span q/span}`
111+### `{$cell p/type q/type}`
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
76−### `{$fork p/(set span)}`
116+### `{$fork p/(set type)}`
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`.
80−### `{$hold p/span q/twig}`
120+### `{$hold p/type q/hoon}`
82−A `$hold` span, with span `p` and twig `q`, is a lazy reference
122+A `%hold` type, with type `p` and hoon `q`, is a lazy reference
83−to the span of `(mint p q)`. In English, it means: "the type of
123+to the type of `(mint p q)`. In English, it means: "the type of
84the product when we compile `q` against subject `p`."
124the product when we compile `q` against subject `p`."
86−### `{$face p/term q/span}`
126+### `{$face p/term q/type}`
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
89`q`. `p` is a `term` or `@tas`, an atomic ASCII string which
129`q`. `p` is a `term` or `@tas`, an atomic ASCII string which
90obeys symbol rules: lowercase and digit only, infix hyphen,
130obeys symbol rules: lowercase and digit only, infix hyphen,
91first character must be lowercase.
131first character must be lowercase.
@@ -95,10 +135,10 @@ nontrivial.
96### `{%atom p/term q/(unit atom))}`
136### `{%atom p/term q/(unit atom))}`
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
99equivalent of a nullable pointer or a Haskell `Maybe`. If `q`
139equivalent of a nullable pointer or a Haskell `Maybe`. If `q`
100−is `~`, null, the span is *warm*; any atom is in the span.
140+is `~`, null, the type is *warm*; any atom is in the type.
101−If `q` is `[~ x]`, where `x` is any atom, the span is *cold*;
141+If `q` is `[~ x]`, where `x` is any atom, the type is *cold*;
102its only legal value is the constant `x`.
142its only legal value is the constant `x`.
104`p` in the atom is a terminal used as an *aura*, or soft atom
144`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:
126 @da absolute date
166 @da absolute date
127 @dr relative date (ie, timespan)
167 @dr relative date (ie, timespan)
128−@f yes or no (inverse boolean)
130@p phonemic base (plot)
169@p phonemic base (plot)
131@r IEEE floating-point
170@r IEEE floating-point
@@ -155,14 +194,14 @@ statically, by casting through the empty aura `@`. Hoon is not
155dependently typed and can't statically enforce data constraints
194dependently typed and can't statically enforce data constraints
156(for example, it can't enforce that a `@tas` is really a symbol).
195(for example, it can't enforce that a `@tas` is really a symbol).
158−### `{$core p/span q/(map term span)}`
197+### `{$core p/type q/(map term type)}`
160−A `$core` is a code-data cell. The data (or *payload*) is the
199+`%core` is for a code-data cell. The data (or *payload*) is the
161−tail; the code (or *battery*) is the head. `p`, a span, is the
200+tail; the code (or *battery*) is the head. `p`, a type, is the
162−span of the payload. `q`, a name-twig table, is the source code
201+type of the payload. `q`, a name-hoon table, is the source code
163for the battery.
202for the battery.
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
166the core itself as the subject. The battery is a tree of these
205the core itself as the subject. The battery is a tree of these
167formulas, or *arms*. An arm is a computed attribute against its
206formulas, or *arms*. An arm is a computed attribute against its