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