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