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