git.iko.soy/urbit.org
on 08099c7 help sign in
urbit.org/hoon/reference/basic.md
177 lines 7.0 kB history raw
1+++
2title = "Basic Types"
3weight = 4
4template = "doc.html"
5aliases = ["docs/reference/hoon-expressions/basic/"]
6+++
7A type is usually understood to be a set of values. Hoon values are all nouns,
8so a Hoon type is a set of nouns.
10Hoon's type system conducts various type-checks at compile time in order to
11ensure type safety. For example, one's program might have an integer squaring
12function, such that given some atom `n` the return value is `n^2`. The output
13value should be an unsigned integer (i.e., an atom). Hoon uses type inference
14on the expression that defines the squaring function in to determine what
15possible values it could produce. If the inferred type 'nests' under the
16desired type then the program compiles; otherwise the compile fails with a
17`nest-fail` crash.
19(For an introduction on how to use Hoon's type system, see Chapter 2 of the Hoon
20tutorial.)
22In this document we discuss the recursive data structure Hoon uses for type
23inference. Because the Hoon compiler is written in Hoon this structure is
24likewise defined in Hoon.
26## `$type`
28Below is a simplified version the `+$ type` arm, which defines the data
29structure Hoon uses to keep track of types. But this data structure is used for
30more than simply type inference. It also handles the resolution of names,
31including both faces and arm names. (See Chapter 1 of the Hoon tutorial for an
32introduction to name resolution.)
34As noted, this is a simplified version of `type`. We undo and
35explain the simplifications in the [advanced types](@/docs/reference/hoon-expressions/advanced.md)
36section.
38```hoon
39+$ term @tas
40+$ type $~ %noun
41 $@ $? %noun
42 %void
43 ==
44 $% [%atom p=term q=(unit @)]
45 [%cell p=type q=type]
46 [%core p=type q=(map term hoon)]
47 [%face p=term q=type]
48 [%fork p=(set type)]
49 [%hold p=type q=hoon]
50 ==
51```
53Effectively this structure defines a set of nouns that Hoon uses to keep track
54track of (1) type information, and (2) name resolution information. This set of
55nouns is recursively defined.
57### `?(%noun %void)`
59`%noun` is the label for a noun about which nothing else is known. Every piece
60of Hoon data is a noun, so everything nests under `%noun`.
62`%void` is the label for the empty set.
64### `[%cell p=type q=type]`
66`[%cell p=type q=type]` is for cells. The `type` of the head is labelled `p`
67and the tail `type` is `q`.
69### `[%fork p=(set type)]`
71`[%fork p=(set type)]` is for the union of all types in the set `p`. That is,
72when the type of an expression is known to be a `%fork`, the expression must
73evaluate as one of the types in `p`.
75Hoon uses branching (usually with conditional runes of the `?` family) for type
76inference in order to rule out which of the types in `p` can apply.
78### `[%hold p=type q=hoon]`
80A `%hold` type, with type `p` and hoon `q`, is a lazy reference to the type of
81`(mint p q)`. In English, it means: "the type of the product when we compile
82Hoon expression `q` against a subject with type `p`."
84### `[%face p=term q=type]`
86A `[%face p=term q=type]` wraps the label `p` around the type `q`. `p` is a
87`term` or `@tas`, an atomic ASCII string which obeys symbol rules: lowercase and
88digit only, infix hyphen, first character must be a lowercase letter.
90### `[%atom p=term q=(unit atom))]`
92`%atom` is for an atom, with two twists. `q` is a `unit`, Hoon's
93equivalent of a nullable pointer or a Haskell `Maybe`. If `q`
94is `~`, null, the type is **warm**; any atom is in the type.
95If `q` is `[~ x]`, where `x` is any atom, the type is **cold**;
96its only legal value is the constant `x`.
98`p` in the atom is a terminal used as an **aura**, or soft atom
99type. Auras are a lightweight, advisory representation of the
100units, semantics, and/or syntax of an atom. An aura is an atomic
101string; two auras are compatible if one is a prefix of the other.
103For instance, `@t` means UTF-8 text (LSB low), `@ta` means ASCII
104text, and `@tas` means an ASCII symbol. `@u` means an unsigned
105integer, `@ud` an unsigned decimal, `@ux` an unsigned
106hexadecimal. You can use a `@ud` atom as a `@u` or vice versa,
107but not as a `@tas`.
109Auras can also end with an optional, capitalized suffix, which
110defines the atom's bitwidth as a log starting from `A`. For
111example, `@udD` is an unsigned decimal byte; `@uxG` is an
112unsigned 64-bit hexadecimal.
114You can make up your own auras and are encouraged to do so, but
115here are some conventions bound to constant syntax:
117```
118@c UTF-32 codepoint
119@d date
120 @da absolute date
121 @dr relative date (ie, timespan)
122@n nil
123@p phonemic base (plot)
124@r IEEE floating-point
125 @rd double precision (64 bits)
126 @rh half precision (16 bits)
127 @rq quad precision (128 bits)
128 @rs single precision (32 bits)
129@s signed integer, sign bit low
130 @sb signed binary
131 @sd signed decimal
132 @sv signed base32
133 @sw signed base64
134 @sx signed hexadecimal
135@t UTF-8 text (cord)
136 @ta ASCII text (knot)
137 @tas ASCII text symbol (term)
138@u unsigned integer
139 @ub unsigned binary
140 @ud unsigned decimal
141 @uv unsigned base32
142 @uw unsigned base64
143 @ux unsigned hexadecimal
144```
146Auras are truly soft; you can turn any aura into any other,
147statically, by casting through the empty aura `@`. Hoon is not
148dependently typed and can't statically enforce data constraints
149(for example, it can't enforce that a `@tas` is really a symbol).
151### `[%core p=type q=(map term hoon)]`
153`%core` is for a code-data cell. The data (or **payload**) is the
154tail; the code (or **battery**) is the head. `p`, a type, is the
155type of the payload. `q` is a mapping of arm names and Hoon expressions. It is the source code for the core battery.
157(For an introduction to cores and arms, see Chapter 1 of the Hoon tutorial.)
159Each expression in the battery source is compiled to a formula, with
160the core itself as the subject. The battery is a tree of these
161formulas, or **arms**. An arm is a computed attribute against its
162core.
164All code-data structures in normal languages (functions, objects,
165modules, etc) become cores in Hoon. A Hoon battery looks a bit
166like a method table, but not every arm is a "method" in the OO
167sense. An arm is a computed attribute. A method is an arm whose
168product is a Hoon function (or **gate**).
170A gate (function, lambda, etc) is a core with one arm, whose name
171is the empty symbol `$`, and a payload whose shape is `[sample
172context]`. The **context** is the subject in which the gate was
173defined; the **sample** is the argument.
175To call this function on an argument `x`, replace the sample (at
176tree address `6` in the core) with `x`, then compute the arm.
177(Of course, we don't mutate the noun, we make a mutant copy.)