2title = "Advanced Types"
5aliases = ["docs/reference/hoon-expressions/advanced/"]
7The definition of `type` in the 'Basic Types' section is only a simplified version. The Hoon type system is simple, but not **that** simple.
9The good news is that you can **skip this section**, at least when
10you're first learning Hoon. Polymorphism and aliasing are mainly
11for advanced programmers writing complex infrastructure and/or
12large functions. Don't worry about them for a little while.
14## The Full Version of `$type`
21 $% [%atom p=term q=(unit @)]
24 [%face p=$@(term tune) q=type]
26 [%hint p=(pair type note) q=type]
30+$ coil $: p=garb :: name, wet=dry, vary
32 r=(pair seminoun (map term tome)) :: chapters
35+$ garb (trel (unit term) poly vair) :: core
37+$ vair ?(%gold %iron %lead %zinc)
38+$ tome (pair what (map term hoon))
41 $: p=(map term (unit hoon)) :: aliases
42 q=(list hoon) :: bridges
46If you compare this to the basic `type`, you'll see that we've
47changed two parts: `%core` and `%face`. We added polymorphism to
48`%core`, and aliases and bridges to `%face`.
50(We also added `%hint` for hint expressions.)
52## `%core`: advanced polymorphism
54If cores never changed, we wouldn't need polymorphism. Of
55course, nouns are immutable and never change, but we use them as
56templates to construct new nouns around.
58Suppose we take a core, a cell `[battery payload]`, and replace
59the payload with a different noun. Then, we invoke an arm from
62Is this legal? Does it make sense? Every function call in Hoon
63does this, so we'd better make it work well.
65The full core stores both payload types. The type that describes
66the payload currently in the core is `p`. The type that describes
67the payload the core was compiled with is `q.q`.
69In the Bertrand Meyer tradition of type theory, there are two
70forms of polymorphism: variance and genericity. In Hoon this
71choice is per core, hence the `poly` label in `p.q`: it can be either `%wet`
72or `%dry`. Dry polymorphism relies on variance; wet polymorphism relies on
77For a dry arm, we apply the Liskov substitution principle: we
78ask, "can we use any `p` as if it was a `q.q`?" This is the same
79test as in `^-` ("kethep") or any type comparison (`nest`). Intuitively,
80we ask: "is the new payload compatible with the old payload?"
82For a core `a`, if `p.a` fits in `q.q.a`, we can use arms on the
83core. The product of a dry arm whose expression is `b` is always
84defined as `[%hold a(p q.q.a, r.p.q %gold) b]`.
86In other words, the subject of the arm computation is the
87original core type. The type of the modified payload, `p`, is
88thrown away. This is of course the normal behavior of a function
89call in most languages.
91### Dry polymorphism and core nesting rules
93Dry polymorphism works by substituting cores. Typically, the
94the programmer uses one core as an interface definition, then
95replaces it with another core which does something useful.
97For core `b` to nest within core `a`, the batteries of `a` and
98`b` must have the same tree shape, and the product of each `b`
99arm must nest within the product of the `a` arm. Wet arms (see
100below) are not compatible unless the hoon is exactly the same.
102But we also apply a payload test that depends on the rules of
103variance. Again, this is traditional Meyer type theory; don't
104worry if you don't know it. These rules should make sense if you
105just think about them intuitively.
107Each core has a "metal" `r.p.q` which defines its variance model.
108A core can be **invariant** (`%gold`), **bivariant** (`%lead`),
109**covariant** (`%zinc`), or **contravariant** (`%iron`). The default
110is gold; a gold core can be cast or converted to any metal, and
111any metal can be cast or converted to lead.
113A gold core `a` has a read-write payload; another core `b` that
114nests within it (i.e., can be substituted for it) must be a gold
115core whose payload is mutually compatible (`+3.a` nests in `+3.b`,
116`+3.b` nests in `+3.a`). Hence, **invariant**.
118A lead core `a` has an opaque payload. There is no constraint on
119the payload of a core `b` which nests within it. Hence,
122(_Opaque_ here means that the faces and arms are not exported into
123the namespace, and that the values of faces and arms can't be written to.
124The object in question can be replaced by something else without breaking type
127An iron core `a` has a write-only sample (payload head, `+6.a`)
128and an opaque context (payload tail, `+7.a`). A core `b` which
129nests within it must be a gold or iron core, such that `+6.a`
130nests within `+6.b`. Hence, **contravariant**.
132A zinc core `a` has a read-only sample (payload head, `+6.a`)
133and an opaque context (payload tail, `+7.a`). A core `b` which
134nests within it must be a gold or zinc core, such that `+6.b`
135nests within `+6.a`. Hence, **covariant**.
139For a wet arm, we ask: "suppose this core was actually compiled
140using `p` instead of `q.q`?" Would the Nock formula we generated
141for `q.q` actually work for a `p` payload?
143A wet arm with hoon `b` in core `a` produces the type `[%hold a
144b]`. Assuming `a` has a modified payload, this will (lazily)
145analyze the arm with the caller's modified payload, `p`.
147But of course, we don't actually recompile the arm at runtime.
148We actually run the formula generated for the original payload,
151When we call a wet arm, we're essentially using the hoon as a
152macro. We are not generating new code for every call site; we
153are creating a new type analysis path, which works as if we
154expanded the callee with the caller's context.
156Consider a function like `turn` (Haskell `map`) which transforms
157each element of a list. To use `turn`, we install a list and a
158transformation function in a generic core. The type of the list
159we produce depends on the type of the list and the type of the
160transformation function. But the Nock formulas for transforming
161each element of the list will work on any function and any list,
162so long as the function's argument is the list item.
164Again, will this work? A simple (and not quite right) way to ask
165this question is to compile all the hoons in the battery for both
166a payload of `p` and a payload of `q.q`, and see if they generate
167exactly the same Nock. The actual algorithm is a little more
168interesting, but not much.
170A Haskeller might say that in a sense, `q.q` and `q.r.q` (the
171original payload and the battery) define a sort of implicit
172typeclass. And indeed, Hoon uses wet arms for the same kinds of
173problems as Haskell typeclasses.
175Like typeclasses, wet arms / gates are a powerful tool. Don't
176use them unless you know what you're doing.
180There's only one field of the `coil` we haven't explained yet:
181`p.r.q`. This is simply the compiled battery, if available. (Of
182course, we compile the hoons in a core against the core itself,
183and the formulas can't be available while we're compiling them.)
184External users of the core want this battery constant, though: it
185lets us fold constants by executing arms at compile time.
187## `%face`: aliases and bridges
189In the advanced `tune` form, the `%face` type also has a couple
190of secret superpowers for hacking the namespace. Remember that
191Hoon doesn't have anything like a symbol table; to resolve a
192limb, we just search the type depth-first.
194If a name is in the `p.p` `map`, it's an alias. (An alias is defined using the
195`=*` rune.) The map contains a `(unit hoon)`; if the unit is full, the name
196resolves to that hoon (compiled against the `q` type). If the unit is empty,
197the name is blocked / skipped (see [limb](/docs/hoon/reference/limbs/limb) for what
200If a name is the `q.p` `term`, it's a bridge. (A bridge is defined using the
201`=,` rune.) When we search for a name, we also compile the bridge, and check
202if the name resolves against the bridge product. If so, we use it.
204These hacks let us deal with interesting large-scale problems,
205like complex library dependencies. You definitely don't need to
206understand them to just write simple Hoon programs.
keysesc to close
- j k
- move down, up
- enter
- open
- esc
- back, or up a level
- 1 2 3 4
- readme, files, commits, refs
- /
- filter
- y
- copy the clone command
- c
- compare the chosen commit with another (or shift-click both)
- ?
- show or hide this list