git.iko.soy/urbit.org
on b641674 help sign in
urbit.org/docs/hoon/basic.md
222 lines 7.9 kB history raw
1---
2navhome: /docs/
3sort: 15
4next: true
5title: Basic types
6---
8# Basic types
10A Hoon `type` is a set of nouns. There is no syntax for directly
11defining the data type of a Hoon expression. Instead, the compiler
12infers the type of a Hoon expression by calculating the range of
13possible values of that expression.
15Working with a type in Hoon requires the use of a `mold`. Each
16type is defined by a mold. To define a custom type, you must create
17a custom mold.
19## Molds
21A mathematical function is a mapping from one set (the domain) to
22another (the range). Pass an object from the domain to some
23function *f*, and *f* returns an object from the range. In Hoon we
24can think of a `gate` as a function, where the gate's `sample` is
25its argument.
27A `mold` is an idempotent function (i.e., gate) that takes any noun
28as its input (i.e., its domain is the set of all nouns). An
29idempotent 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
31by that mold. That is, each mold's type is the set of possible
32outputs of that mold.
34Essentially, molds are constructor functions. You can pass a mold
35any data you like, and the product is guaranteed be of the type
36defined by that mold. Molds are the perfect tool for validating
37untrusted foreign data: just call the relevant mold with that data.
38But this use case is unusual for beginners; otherwise you shouldn't
39call molds directly.
41More frequently, molds are used when we want to `cast`. We use a
42cast when we want the Hoon compiler's type-checker to test whether
43a Hoon expression is guaranteed to evaluate to a product of the
44desired 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
46gate.
48The `^` family of runes is for casting. In particular, `^-` allows
49us to cast with a mold. For example, we can cast for an `atom` using
50the `@` mold as follows:
52```
53^-(@ 17)
54```
56Evaluating the above in `dojo` should return 17, because 17 is of
57the type `atom`. On the other hand,
59```
60^-(@ [17 18])
61```
63...this should result in a `nest-fail`, because `[17 18]` is a cell,
64not an atom.
66See the documentation on the `^` family of runes for more information
67on casts. See the documentation on the `$` family of runes for
68building molds. (Also check out the irregular `,` operator.)
70## `type`: a set of types
72Below is the mold for `type`, written in Hoon. This mold's range is
73the set of all types. (Don't let yourself get too dizzy thinking
74about it! Strictly speaking, the range is of trees of type-*labels*
75used by the compiler's type-checker. We don't mess around with
76set-theoretic paradoxes.)
78You haven't seen this syntax before, and we haven't explained it yet;
79just treat it as pseudocode.
81This is a slightly simplified version of `type`. We undo and
82explain the simplifications in the [advanced types](../advanced)
83section.
85```
86++ term @tas
87++ type
88 $@ $? $noun
89 $void
90 == $% {$atom p/term q/(unit atom)}
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}
96 ==
97```
99If 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
101the heads `%atom`, `%cell`, `%core`, etc. We'll go through each of
102these cases below.
104### `?($noun $void)`
106`%noun` is the label for the set of all nouns. `%void` is the label
107for the empty set.
109(For now, don't worry too much about the switch from `$` to `%`.)
111### `{$cell p/type q/type}`
113`[%cell p/type q/type]` is for the set of all cells with head `p` and
114tail `q`.
116### `{$fork p/(set type)}`
118`[%fork p/(set type)]` is for the union of all types in the set `p`.
120### `{$hold p/type q/hoon}`
122A `%hold` type, with type `p` and hoon `q`, is a lazy reference
123to the type of `(mint p q)`. In English, it means: "the type of
124the product when we compile `q` against subject `p`."
126### `{$face p/term q/type}`
128A `[%face p/term q/type]` wraps the label `p` around the type
129`q`. `p` is a `term` or `@tas`, an atomic ASCII string which
130obeys symbol rules: lowercase and digit only, infix hyphen,
131first character must be lowercase.
133See [`:limb`](../twig/limb/limb) for how labels are resolved. It's
134nontrivial.
136### `{%atom p/term q/(unit atom))}`
138`%atom` is for an atom, with two twists. `q` is a `unit`, Hoon's
139equivalent of a nullable pointer or a Haskell `Maybe`. If `q`
140is `~`, null, the type is *warm*; any atom is in the type.
141If `q` is `[~ x]`, where `x` is any atom, the type is *cold*;
142its only legal value is the constant `x`.
144`p` in the atom is a terminal used as an *aura*, or soft atom
145type. Auras are a lightweight, advisory representation of the
146units, semantics, and/or syntax of an atom. An aura is an atomic
147string; two auras are compatible if one is a prefix of the other.
149For instance, `@t` means UTF-8 text (LSB low), `@ta` means ASCII
150text, and `@tas` means an ASCII symbol. `@u` means an unsigned
151integer, `@ud` an unsigned decimal, `@ux` an unsigned
152hexadecimal. You can use a `@ud` atom as a `@u` or vice versa,
153but not as a `@tas`.
155Auras can also end with an optional, capitalized suffix, which
156defines the atom's bitwidth as a log starting from `A`. For
157example, `@udD` is an unsigned decimal byte; `@uxG` is an
158unsigned 64-bit hexadecimal.
160You can make up your own auras and are encouraged to do so, but
161here are some conventions bound to constant syntax:
163```
164@c UTF-32 codepoint
165@d date
166 @da absolute date
167 @dr relative date (ie, timespan)
168@n nil
169@p phonemic base (plot)
170@r IEEE floating-point
171 @rd double precision (64 bits)
172 @rh half precision (16 bits)
173 @rq quad precision (128 bits)
174 @rs single precision (32 bits)
175@s signed integer, sign bit low
176 @sb signed binary
177 @sd signed decimal
178 @sv signed base32
179 @sw signed base64
180 @sx signed hexadecimal
181@t UTF-8 text (cord)
182 @ta ASCII text (span)
183 @tas ASCII symbol (term)
184@u unsigned integer
185 @ub unsigned binary
186 @ud unsigned decimal
187 @uv unsigned base32
188 @uw unsigned base64
189 @ux unsigned hexadecimal
190```
192Auras are truly soft; you can turn any aura into any other,
193statically, by casting through the empty aura `@`. Hoon is not
194dependently typed and can't statically enforce data constraints
195(for example, it can't enforce that a `@tas` is really a symbol).
197### `{$core p/type q/(map term type)}`
199`%core` is for a code-data cell. The data (or *payload*) is the
200tail; the code (or *battery*) is the head. `p`, a type, is the
201type of the payload. `q`, a name-hoon table, is the source code
202for the battery.
204Each hoon in the battery source is compiled to a formula, with
205the core itself as the subject. The battery is a tree of these
206formulas, or *arms*. An arm is a computed attribute against its
207core.
209All code-data structures in normal languages (functions, objects,
210modules, etc) become cores in Hoon. A Hoon battery looks a bit
211like a method table, but not every arm is a "method" in the OO
212sense. An arm is a computed attribute. A method is an arm whose
213product is a Hoon function (or *gate*).
215A gate (function, lambda, etc) is a core with one arm, whose name
216is the empty symbol `$`, and a payload whose shape is `{sample
217context}`. The *context* is the subject in which the gate was
218defined; the *sample* is the argument.
220To call this function on an argument `x`, replace the sample (at
221tree address `6` in the core) with `x`, then compute the arm.
222(Of course, we don't mutate the noun, we make a mutant copy.)