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