@@ -0,0 +1,157 @@
1+---
2+sort: 7
3+---
4+
5+# Type: `span`
6+
7+A `span` is a set of nouns and an interpretation of these nouns.
8+
9+## Span, mold, type: what's in a type system?
10+
11+There is no Hoon syntax for a span. The programmer never defines
12+a span explicitly. It is always produced as the inferred range
13+of an expression (twig).
14+
15+But we still need simple, well-formed expressions that produce
16+regular and well-shaped ranges, for three reasons.
17+
18+First: in most cases, this trivial generator should be much
19+simpler than the computation itself. Casting the actual result
20+to its ideal shape makes sure we know what we're building.
21+
22+Second: we can define a standard form for such generators, and
23+the standard form is useful. The standard form is a constructor
24+function, or *mold*.
25+
26+A mold is an idempotent function (`gate`), accepting any noun.
27+(An idempotent function is one such that f(f(x)) equals f(x) if
28+f(x) does not crash.) The product range of the function is the
29+span, or *icon*, of the mold.
30+
31+Usually we use molds purely in the first sense: as an abstract
32+definition of a noun. Don't actually call a mold unless you're
33+actually validating untrusted foreign data. As a beginner,
34+hopefully you aren't!
35+
36+(It's also important to remember that any twig can be a mold.
37+Some stems are macros designed for making molds, but a mold is
38+defined by how it's used, not what it's made of. The Hoon type
39+system cannot even check the mold definition, since Hoon lacks
40+dependent type and therefore can't verify idempotence.)
41+
42+To summarize: a Hoon "type declaration" is the definition of a
43+function, the mold. A mold and a span are different things. A
44+mold is a constructor. A span defines a set of nouns, possibly
45+infinite, and annotates them with semantics.
46+
47+Either mold or span could be called a "type," but not both. We
48+often say "type" in Hoon. But we always mean it informally.
49+Ideally, the meaning is obvious from context. ("Type" can also
50+mean a `mark`, Urbit's equivalent of a MIME type.)
51+
52+## The `span` mold
53+
54+Usually in Hoon we define the semantics of a primitive by the
55+state the span of all nouns that implement that primitive. We
56+state this span as the icon of a mold. That mold is produced by
57+a kernel arm `span`:
58+
59+```
60+++ term @tas
61+++ span
62+ $@ $? $noun
63+ $void
64+ == $% {$atom p/term q/(unit atom)}
65+ {$cell p/span q/span}
66+ {$core p/span q/(map term span)}
67+ {$face p/term q/span}
68+ {$fork p/(set span)}
69+ {$hold p/span q/twig}
70+ ==
71+```
72+
73+This is a syntactically correct Hoon twig, but treat it as
74+pseudocode. If a span is an atom, it's either the atomic string
75+`noun` or `void`; if a cell, it's a tuple with one of the heads
76+`atom`, `cell`, `core`, etc. We'll go through each of these
77+cases below.
78+
79+## `$noun` and `$void`
80+
81+`$noun` is the set of all nouns. `$void` is the set of no nouns.
82+
83+## `{$cell p/span q/span}`
84+
85+`{$cell p/span q/span}` is the set of all cells with head `p` and
86+tail `q`.
87+
88+## `{$fork p/(set span)}
89+
90+`{$fork p/(set span)}` is the union of all spans in the set `p`.
91+
92+## `{$hold p/span q/twig}`
93+
94+A `$hold` span, with span `p` and twig `q`, is a lazy reference
95+to the span of `(mint p q)`. In English it means: "the type of
96+the product when we compile `q` against subject `p`.
97+
98+## `{$face p/term q/span}
99+
100+A `{$face p/term q/span}` wraps the label `p` around the span
101+`q`. `p` is a `term` or `@tas`, an atomic ASCII string which
102+obeys symbol rules: lowercase and digit only, infix hyphen,
103+first character must be lowercase.
104+
105+See the [twig chapter](twig) for how labels are resolved. It's
106+nontrivial.
107+
108+## `{%atom p/term q/(unit atom))}
109+
110+An `$atom` is an atom, with two twists. `q` is a `unit`, Hoon's
111+equivalent of a nullable pointer or a Haskell `Maybe`. If `q`
112+is `~`, null, the span is *warm*; any atom is in the span.
113+If `q` is `[~ x]`, where `x` is any atom, the span is *cold*;
114+its only legal value is the constant `x`.
115+
116+`p` in the atom is a terminal used as an *aura*, or soft atom
117+type. Auras are a lightweight, advisory representation of the
118+units, semantics, and/or syntax of an atom. An aura is an atomic
119+string; Two auras are compatible if one is a prefix of the other.
120+
121+For instance, `@t` means UTF-8 text (LSB low), `@ta` means ASCII
122+text, and `@tas` means an ASCII symbol. `@u` means an unsigned
123+integer, `@ud` an unsigned decimal, `@ux` an unsigned
124+hexadecimal. You can use a `@ud` atom as a `@u` or vice versa,
125+but not as a `@tas`.
126+
127+Auras are truly soft; you can turn any aura into any other,
128+statically, by casting through the empty aura `@`. Hoon is not
129+dependently typed and can't statically enforce data constraints
130+(for example, it can't enforce that a `@tas` is really a symbol).
131+
132+## `{$core p/span q/(map term span)}
133+
134+A `$core` is a code-data cell. The data (or *payload*) is the
135+tail; the code (or *battery*) is the head. `p`, a span, is the
136+span of the payload. `q`, a name-twig table, is the source code
137+for the battery.
138+
139+Each twig in the battery source is compiled to a formula, with
140+the core itself as the subject. The battery is a tree of these
141+formulas, or *arms*. An arm is a computed attribute against its
142+core.
143+
144+All code-data structures in normal languages (functions, objects,
145+modules, etc) become cores in Hoon. A Hoon battery looks a bit
146+like a method table, but not every arm is a "method" in the OO
147+sense. An arm is a computed attribute. A method is an arm whose
148+product is a Hoon function (or *gate*).
149+
150+A gate is a core with one arm, whose name is the empty symbol
151+`$`, and a payload whose shape is `{sample context}`. The
152+*context* is the subject in which the gate was defined; the
153+*sample* is the argument.
154+
155+To call this function on an argument `x`, replace the sample (at
156+tree address `6` in the core) with `x`, then compute the arm.
157+(Of course, we don't mutate the noun, we make a mutant copy.)