@@ -0,0 +1,674 @@
1+:- :~ navhome/'/docs/'
2+ navuptwo/'true'
3+ sort/'38'
4+ title/'3.1 Type Polymorphism'
5+ ==
6+;>
7+
8+# Polymorphism
9+
10+There are many cases in which one may want to write a function that accepts as input various different types of data. Such a function is said to be [polymorphic](https://en.wikipedia.org/wiki/Polymorphism_(computer_science%29). ("Polymorphism" = "many forms"; so polymorphic functions accept many forms of data as input.)
11+
12+One relatively trivial form of polymorphism involves sub-typing. A gate whose sample is a raw `noun` can accept any Hoon data structure as input -- it's just that the sample will only be treated as a noun. For example, consider the `copy` gate below:
13+
14+```
15+> =copy |=(a=* [a a])
16+
17+> (copy 15)
18+[15 15]
19+
20+> (copy [15 16])
21+[[15 16] [15 16]]
22+
23+> (copy "Hello!")
24+[[72 101 108 108 111 33 0] [72 101 108 108 111 33 0]]
25+```
26+
27+`copy` takes the input, `a`, and returns a cell of `[a a]`. Because every piece of Hoon data is a noun, anything can be taken as input. Every other type in Hoon is a sub-type of `noun`. But the output of `copy` is always going to be just a cell of nouns; the type information of the original input value is not preserved by the gate. Consider the `tape` in the last example -- `"Hello!"` was pretty-printed in the dojo as a raw noun, not as a string. So `copy` is a relatively uninteresting polymorphic function.
28+
29+In this lesson we'll go over Hoon's support for more interesting polymorphic functions.
30+
31+## Polymorphic Properties of Cores
32+
33+Hoon supports type polymorphism at the core level. That is, each core has certain polymorphic properties that are tracked and maintained as metadata by Hoon's type system. (See `+$ type` of `hoon.hoon`.) These properties determine the extent to which a core can be used as an interface for values of various types.
34+
35+This is rather vaguely put so far. We can clarify by talking more specifically about the different kinds of polymorphism supported in Hoon. There are two kinds of type polymorphism for cores: [genericity](https://en.wikipedia.org/wiki/Generic_programming), to include certain kinds of of [parametric polymorphism](https://en.wikipedia.org/wiki/Parametric_polymorphism); and [variance polymorphism](https://en.wikipedia.org/wiki/Covariance_and_contravariance_(computer_science%29), which involves making use of special sub-typing rules for cores.
36+
37+If you don't understand these very well, that's okay. We'll explain them. Let's begin with the former.
38+
39+## Dry vs. Wet Cores
40+
41+To review briefly, a *core* is a pair of `[battery payload]`. The *battery* contains the various arms of the core (code), and the *payload* contains all the data needed to evaluate those arms correctly (data). Every arm is evaluated with its parent core as the subject. A *gate* (i.e., a Hoon function) is a core with exactly one arm named `$` and with a payload of the form: `[sample context]`. The *sample* is reserved for the function's argument value, and the *context* is any other data needed to evaluate `$` correctly.
42+
43+There are two kinds of cores: *dry* and *wet*. Dry cores, which are more typical, _don't_ make use of *genericity*. Wet cores do. In order to understand generic functions in Hoon, you first have to understand the difference between dry and wet cores.
44+
45+The cores produced with the `|=`, `|-`, `|%`, and `|_` runes, among others, are all dry. (Dry is more typical.) The cores produced with the `|*` and `|@` runes are wet. (`|*` and `|@` are the wet versions of `|=` and `|%`, respectively.)
46+
47+Briefly, the difference between dry and wet cores has to do with how they're treated at compile time, for type inference and type checking. During the type check, the product type of each arm is inferred. For computing a dry arm type, it's assumed that the arm's subject type is of the original parent core. For computing a wet arm type, the parent core type is used, except that the payload value may vary from the original type.
48+
49+Because of this difference, wet cores can be used to make functions that take different input types at different call sites. We'll go over the dry/wet distinction in more detail below and explain why it matters.
50+
51+### Dry Cores
52+
53+A core's payload can change its values swapped out for other values. How can we ensure that its arms are still able to run correctly?
54+
55+There is a type check for each arm of a dry core, intended to verify that the arm's parent core has a payload of the appropriate type. In this section we'll describe that type check.
56+
57+When an arm of a dry core is evaluated it takes its parent core as the subject, often with a modified sample _value_. But any change in sample _type_ should be conservative; the modified sample value must be of the same type as the default sample value (or possibly a subtype). When the `$` arm is evaluated it should have a subject of a type it knows how to use.
58+
59+For example, consider the gate created by `add`, a function in the Hoon standard library. The structure of the `add` gate is as follows:
60+
61+```
62+ add
63+ / \
64+ $ .
65+ / \
66+ sample context
67+```
68+
69+The `add` code depends on the fact that there are two atoms in the sample: the numbers to be added together. Hence, it is appropriate that only a cell of atoms is permitted for the sample. We can look at the default sample of `add` at address `+6`:
70+
71+```
72+> +6:add
73+[a=0 b=0]
74+```
75+
76+If we call `add` with no arguments, we get the sum of these two values:
77+
78+```
79+> (add)
80+0
81+```
82+
83+Any other type of value in the sample results in a `nest-fail` crash:
84+
85+```
86+> (add 12 "hello")
87+nest-fail
88+```
89+
90+This function call attempts to create a modified copy of the `add` gate, replacing the original sample `[0 0]` with `[12 "hello"]`, then evaluate the `$` arm of this modified core. (We ignore the `a` and `b` faces for now.) But this piece of code failed to compile; the type system knew to reject it.
91+
92+How does it know? The type system keeps track of two payload types for each core:
93+
94++ The original payload type, i.e., the type of the payload when the core was first created. In the case of `add`, the original sample type is a cell of atoms, `[@ @]`. This original type information is always preserved, regardless of what value type is used for calling `add`.
95++ The current payload type, i.e., the type of the payload after any substitutions or other changes have been made. In the last `add` call, `(add 12 "hello")`, this would have been a cell whose head is an `@ud`, and whose tail is a `tape`.
96+
97+The type check at compile time compares these two types, and if the current payload type doesn't nest under the original payload, the compile fails with a `nest-fail` crash. (E.g., a cell of type `[@ud tape]` doesn't nest under `[@ @]`!) Otherwise, the original payload _type_ is used for evaluation, even though the original sample _value_ has been replaced. So the arm of a dry core is guaranteed to run with exactly the same subject type each time it is evaluated.
98+
99+The type check for each arm in a dry core can be understood as implementing a version of the ["Liskov substitution principle"](https://en.wikipedia.org/wiki/Liskov_substitution_principle). The arm works for some (originally defined) payload type `P`. Payload type `Q` nests under `P`. Therefore the arm works for `Q` as well, though for type inference purposes the payload is treated as a `P`. The inferred type of the arm is based on the assumption that it's evaluated with a subject type exactly like that of its original parent core -- i.e., whose payload is of type `P`.
100+
101+### Wet Cores (Genericity)
102+
103+The type checking and inference rules for arms are a bit different for wet cores. Whereas the dry arm is understood as having _exactly_ its parent core type for its subject, wet arms can be evaluated with payloads of various types.
104+
105+When a function call occurs on a wet arm, the [call site](https://en.wikipedia.org/wiki/Call_site) argument value type is used as the sample type -- not the original parent core sample type. Correspondingly, the inferred type of a wet arm depends, among other things, on the type of the argument value -- i.e., the modified sample value type of the core, not the original. Thus, the inferred product type typically varies from one call site to another.
106+
107+The arms of wet cores must be able to handle subjects of various types -- they are interestingly polymorphic in a way that dry cores cannot be. The Hoon code that defines each wet arm must be [generic](https://en.wikipedia.org/wiki/Generic_programming) with respect to the sample type.
108+
109+An example will clarify how wet gates work. Recall the `copy` gate from earlier in the lesson:
110+
111+```
112+> =copy |=(a=* [a a])
113+
114+> (copy 15)
115+[15 15]
116+
117+> (copy [15 16])
118+[[15 16] [15 16]]
119+
120+> (copy "Hello!")
121+[[72 101 108 108 111 33 0] [72 101 108 108 111 33 0]]
122+```
123+
124+This gate is dry (as are all cores produced with `|=`), and so the inferred type of the product is determined based on the original core sample type. In this case, that's a raw noun, `*`. The dojo pretty-printer therefore has no way of knowing that the product of the last `copy` call should be printed as a pair of `tape`s -- it just sees a pair of nouns. If we want the original type information preserved, we must use a wet gate, which can be produced with `|*`:
125+
126+```
127+> =wet-copy |*(a=* [a a])
128+
129+> (wet-copy 15)
130+[15 15]
131+
132+> (wet-copy [15 16])
133+[[15 16] 15 16]
134+
135+> (wet-copy "Hello!")
136+["Hello!" "Hello!"]
137+```
138+
139+We see that the type information about the `tape` literal `"Hello!"` is preserved in the last function call, as desired. The original sample value of `wet-copy` is replaced with `"Hello!"`, and the original sample type is ignored in favor of the new sample type, `tape`. So the inferred arm type is a cell of `tape`s, which the dojo pretty-printer handles appropriately.
140+
141+In fact, `wet-copy` can take a Hoon value of any type you like!
142+
143+For another example, consider the following gate that switches the order of the head and tail of a cell:
144+
145+```
146+> =switch |*([a=* b=*] [b a])
147+
148+> (switch 2 3)
149+[3 2]
150+
151+> (switch "Hello" [11 22 33])
152+[[11 22 33] "Hello"]
153+
154+> (switch 0xbeef 0b1101)
155+[0b1101 0xbeef]
156+```
157+
158+Not only does `switch` reverse the order of the values, it also reverses their respective types, as desired. The dry version of switch is not as useful:
159+
160+```
161+> =dry-switch |=([a=* b=*] [b a])
162+
163+> (dry-switch "Hello" [11 22 33])
164+[[11 22 33] [72 101 108 108 111 0]]
165+
166+> (dry-switch 0xbeef 0b1101)
167+[13 48.879]
168+```
169+
170+Even though both `switch` and `dry-switch` are polymorphic in the sense that each can operate on any pair of nouns, the former does so in a way that makes use of the argument value types.
171+
172+But `switch` can't take just any input:
173+
174+```
175+> (switch 11)
176+-find.b
177+```
178+
179+It must take a cell, not an atom. So it's certainly possible to write a wet gate that doesn't take all possible input types.
180+
181+It is good practice to include a cast with all gates, even wet gates. But in many cases the desired output type depends on the input type. How can we cast appropriately? Often we can cast by example, using the input values themselves. For example, we can rewrite `switch` as:
182+
183+```
184+> =switch |*([a=* b=*] ^+([b a] [b a]))
185+
186+> (switch "Hello" 0xbeef)
187+[0xbeef "Hello"]
188+```
189+
190+As is the case with dry arms, there is a type-check associated with each wet arm. Or, rather, there are potentially many checks for each wet arm, one for each wing in the code that resolves to a wet arm. The product type of that arm is inferred at each call site, using the argument value type given at that site. If the type inference doesn't go through -- e.g., if there is a cast that doesn't succeed relative to the call site argument value -- then the compile will crash with a `nest-fail`. Otherwise the type check goes through with the inferred type of the wet arm at that call site. So the product type of a wet gate can differ from one call site to another, as we saw with `switch` above.
191+
192+### Parametric Polymorphism and `+*` Arms
193+
194+In Chapter 2 we saw how to use the `+*` rune to define an arm that produced a more complex type from one or more simpler types. This rune provides a way of making use of *parametric polymorphism* in Hoon.
195+
196+For example, we have `list`s, `tree`s, and `set`s in Hoon, which are each defined in `hoon.hoon` with `+*` arms. (Take a moment to see for yourself!) Each `+*` arm is followed by an argument definition, surrounded in square brackets `[ ]`. After that subexpression comes another that defines a type, relative to the input value. For example, here is the definition of `list` from `hoon.hoon`:
197+
198+```
199++* list [item]
200+ :: null-terminated list
201+ ::
202+ :: mold generator: produces a mold of a null-terminated list of the
203+ :: homogeneous type {a}.
204+ ::
205+ $@(~ [i=item t=(list item)])
206+```
207+
208+The `+*` rune is especially useful for defining [containers](https://en.wikipedia.org/wiki/Container_(abstract_data_type%29) of various kinds. A container is a kind of data structure for a collection of values of one or more given types. Indeed, `list`s, `tree`s, and `set`s are all examples of containers. You can have a `(list @)`, a `(list ^)`, a `(list *)`, and so on. Or a `(tree @)`, a `(tree ^)`, a `(tree *)`, etc. And the same for `set`.
209+
210+One nice thing about containers defined by `+*` is that they nest in the expected way. Intuitively a `(list @)` should nest under `(list *)`, because `@` nests under `*`. And so it does:
211+
212+```
213+> =a `(list @)`~[11 22 33]
214+
215+> ^-((list *) a)
216+~[11 22 33]
217+```
218+
219+Conversely, a `(list *)` should not nest under `(list @)`, because `*` does not nest under `@`:
220+
221+```
222+> =b `(list *)`~[11 22 33]
223+
224+> ^-((list @) b)
225+nest-fail
226+```
227+
228+Let's clear the dojo subject by unbinding the faces we've used up to now in the lesson:
229+
230+```
231+=a
232+
233+=b
234+
235+=copy
236+
237+=wet-copy
238+
239+=switch
240+
241+=dry-switch
242+```
243+
244+## Core Variance
245+
246+Let's say you want to write a function that takes a gate as one (or more) of its arguments. It's not hard to imagine useful cases of this. Consider `turn` from the Hoon standard library, which applies an arbitrary function to each item in a list and returns a modified list:
247+
248+```
249+> =b `(list @)`~[2 3 4 5]
250+
251+> (turn b |=(a=@ +(a)))
252+~[3 4 5 6]
253+
254+> (turn b |=(a=@ (mul 2 a)))
255+~[4 6 8 10]
256+
257+=b
258+```
259+
260+It's quite useful to be able to pass cores as arguments. But let's think about how to write a function that accepts a core as input. How do we define a sample so that it accepts a core?
261+
262+We _could_ define the sample by example -- i.e., with `$_`, or `_` for short -- using a core. Consider the following:
263+
264+```
265+> =mycore =>([12 13] |=(a=@ +(a)))
266+
267+> =apply |=([a=@ b=_mycore] (b a))
268+
269+> (apply 15 mycore)
270+16
271+
272+> (apply 15 =>([12 13] |=(a=@ +(+(a)))))
273+17
274+
275+> (apply 15 =>([12 13] |=(a=@ 123)))
276+123
277+```
278+
279+This works, but in fact `apply` is a very brittle function. It can only take as input a core whose payload is exactly like, or a subtype of, the payload of `mycore`:
280+
281+```
282+> (apply 15 |=(a=@ (mul 2 a)))
283+nest-fail
284+```
285+
286+A core created in one place of your code isn't likely to have the same payload as a core produced elsewhere, unless you intentionally define it so that it does. This often isn't practical, so we need another way to indicate that we want a core as input.
287+
288+Why did the last example crash? To understand this, you need to understand the the different variance properties a core can have. These properties determine the nesting and type inference rules associated with that core.
289+
290+The basic question to be answered is: when does one core type nest under another?
291+
292+The battery nesting rules for dry cores are relatively straightforward, and they're the same for all cores, regardless of variance properties. Let `A` and `B` be two cores. The type of `B` nests under the type of `A` only if two conditions are met: (i) the batteries of `A` and `B` have exactly the same tree shape, and (ii) the product type of each `B` arm nests under the product type of the corresponding `A` arm.
293+
294+The payload types of `A` and `B` must also be checked. Certain payload nesting rules apply to all cores, if `B` is to nest under `A`: (i) if `A` is dry (wet) then `B` must also be dry (wet); (ii) the original payload type of `A` must mutually nest with the current payload type of `A` (i.e., these types nest under each other); and (iii) the current payload type of `B` must nest under the original payload type of `B`.
295+
296+### The Four Kinds of Cores: Gold, Iron, Zinc, and Lead
297+
298+But there are different sets of nesting rules for finishing the payload type check, depending on the variance properties of the core.
299+
300+There are four kinds of core variance properties: *gold* (invariant sample), *iron* (contravariant sample), *zinc* (covariant sample), and *lead* (bivariant sample). These properties are tracked by the Hoon type system.
301+
302+In brief:
303+
304++ If `A` is a gold core, then core `B` nests under it only if `B` is gold and the sample of `B` doesn't vary in type from the sample of `A`. The sample `B` is *invariant* (i.e., neither co- nor contravariant) relative to the sample of an `A` it nests under. Gold cores have a read-write payload.
305++ If `A` is an iron core, then core `B` nests under it only if `B` is gold or iron and the sample of `A` nests under the sample of `B`. Notice that the nesting direction of the samples is the opposite of the nesting direction of the cores. I.e., the sample types *contravary* with respect to the iron core types. Iron cores have a write-only sample and an opaque context (neither read nor write).
306++ If `A` is a zinc core, then core `B` nests under it only if `B` is gold or zinc and the sample of `B` nests under the sample of `A`. Notice that the nesting direction of the samples is the same as the nesting direction of the cores. I.e., the sample types *co-vary* with respect to the zinc core types. Zinc cores have a read-only sample and an opaque context.
307++ If `A` is a lead core, then core `B` nests under it without any additional payload check beyond those described in the previous section. It trivially follows that the payload type both co- and contravaries with respect to the lead core types (hence lead cores are *bivariant*). Lead cores have an opaque payload.
308+
309+Let's go through each kind more carefully.
310+
311+#### Gold Cores (Invariant)
312+
313+By default, most cores are gold. This includes the cores produced with the `|%`, `|=`, `|_`, and `|-` runes, among others.
314+
315+Assume that `A` is a gold core and that `B` is some other core. The type of `B` nests under the type of `A` only if the original payload types of each mutually nest -- i.e., the original payload type of `A` nests under the original payload type of `B`, and _vice versa_. Furthermore, only gold cores nest under other gold cores; so `B` must be gold to nest under `A`.
316+
317+These payload nesting rules are the strictest ones for cores. The payload type is neither covariant nor contravariant; when type-checking against a gold core, the target payload cannot vary at all in type. Consequently, it is type-safe to modify every part of the payload: gold cores have a read-write payload.
318+
319+Usually it makes sense to cast for a gold core type when you're treating a core as a state machine. The check ensures that the payload, which includes the relevant state, doesn't vary in type. To see state machines that involve casts for gold cores, see Chapter 2 of the Hoon tutorial.
320+
321+Let's look at simpler examples here, using the `^+` rune:
322+
323+```
324+> ^+(|=(^ 15) |=(^ 16))
325+< 1.xqz
326+ { {* *}
327+ {our/@p now/@da eny/@uvJ}
328+ <19.rga 23.byz 5.rja 36.apb 119.ikf 238.utu 51.mcd 93.glm 74.dbd 1.qct $141>
329+ }
330+>
331+
332+> ^+(|=(^ 15) |=([@ @] 16))
333+nest-fail
334+
335+> ^+(|=(^ 15) |=(* 16))
336+nest-fail
337+```
338+
339+The first cast goes through because the right-hand gold core has the same sample type as the left-hand gold core. The sample types mutually nest. The second cast fails because the right-hand sample type is more specific than the left-hand sample type. (Not all cells, `^`, are pairs of atoms, `[@ @]`.) And the third cast fails because the right-hand sample type is broader than the left-hand sample type. (Not all nouns, `*`, are cells, `^`.)
340+
341+Two more examples:
342+
343+```
344+> ^+(=>([1 2] |=(@ 15)) =>([123 456] |=(@ 16)))
345+<1.xqz {@ @ud @ud}>
346+
347+> ^+(=>([1 2] |=(@ 15)) =>([123 456 789] |=(@ 16)))
348+nest-fail
349+```
350+
351+In these examples, the `=>` rune is used to give each core a simple context. The context of the left-hand core in each case is a pair of atoms, `[@ @]`. The first cast goes through because the right-hand core also has a pair of atoms as its context. The second cast fails because the right-hand core has the wrong type of context -- three atoms, `[@ @ @]`.
352+
353+#### Iron Cores (Contravariant)
354+
355+Assume that `A` is an iron core and `B` is some other core. The type of `B` nests under the type of `A` only if the original sample type of `A` nests under the original sample type of `B`. That is, `B`'s sample type must be equivalent or more general than the sample type of `A`. Furthermore, `B` must be either iron or gold to nest under `A`.
356+
357+The context type of `B` isn't checked at all; and because of the nesting rules it isn't type-safe to do type-inference on the sample of an iron gate. Thus, there are certain restrictions on iron cores that preserve type safety: (i) the context of an iron core is opaque, meaning that it cannot be written-to or read-from; and (ii) the iron core payload is write-only.
358+
359+Iron gates are particularly useful when you want to pass gates (having various payload types) to other gates. We can illustrate this use with a very simple example. Save the following as `gatepass.hoon` in the `gen` directory of your urbit's pier:
360+
361+```
362+|= a=_^|(|=(@ 15))
363+^- @
364+=/ b=@ (a 10)
365+(add b 20)
366+```
367+
368+This generator is mostly very simple. Everything about it should be clear except possibly the first line.
369+
370+The first line defines the gate sample as an iron gate and gives it the face `a`. So the function as a whole is for taking some gate, calling it by passing it the value `10`, adding `20` to it, and returning the result. Let's try it out in the dojo:
371+
372+```
373+> +gatepass |=(a=@ +(a))
374+31
375+
376+> +gatepass |=(a=@ (add 3 a))
377+33
378+
379+> +gatepass |=(a=@ (mul 3 a))
380+50
381+```
382+
383+But we still haven't fully explained the first line of the code. In particular, what does `_^|(|=(@ 15))` mean? The inside portion is clear enough -- `|=(@ 15)` produces a normal (i.e., gold) gate that takes an atom and returns `15`. The `^|` rune is used to turn gold gates to iron. (Reverse alchemy!) And the `_` character turns that iron gate value into a structure, i.e. a type. So the whole subexpression means, roughly: "the same type as an iron gate whose sample is an atom, `@`, and whose product is another atom, `@`". The context isn't checked at all. This is good, because that allows us to accept gates defined in drastically different environments. Let's try passing a gate with a different context:
384+
385+```
386+> +gatepass =>([22 33] |=(a=@ +(a)))
387+31
388+```
389+
390+Yup, it still works. You can't do that with a gold core sample!
391+
392+There's a simpler way to define an iron sample. Revise the first line of `gatepass.hoon` to the following:
393+
394+```
395+|= a=$-(@ @)
396+^- @
397+=/ b=@ (a 10)
398+(add b 20)
399+```
400+
401+If you test it you'll find that the generator behaves the same as it did before the edits. The `$-` rune is used to create an iron gate structure, i.e., an iron gate type. The first expression defines the sample type of the iron gate, and the second subexpression defines the gate output type.
402+
403+The sample type of an iron gate is contravariant. This means that, when doing a cast with some iron gate, the desired gate must have either the same sample type or a superset.
404+
405+Why is this a useful nesting rule for passing gates?
406+
407+Let's say you're writing a function `F` that takes as input some gate `G`. Let's also say you want `G` to be able to take as input any *mammal*. That's because the code of `F` is going to pass arbitrary *mammals* to `G`, so that `G` needs to know how to handle all *mammals* correctly. You can't pass `F` a gate that only takes *dogs* as input, because `F` might call it with a *cat*. But `F` can accept a gate that takes all *animals* as input, because a gate that can handle any *animal* can handle *any mammal*.
408+
409+Iron cores are designed precisely with this purpose in mind. The reason that the sample is write-only is that we want to be able to assume, within function `F`, that the sample of `G` is a *mammal*. But that might not be true when `G` is first passed into `F` -- the default value of `G` could be another *animal*, say, a *lizard*. So we restrict looking into the sample of `G` by making the sample write-only. The illusion is maintained and type safety secured.
410+
411+Let's illustrate iron core nesting properties:
412+
413+```
414+> ^+(^|(|=(^ 15)) |=(^ 16))
415+< 1|xqz
416+ { {* *}
417+ {our/@p now/@da eny/@uvJ}
418+ <19.rga 23.byz 5.rja 36.apb 119.ikf 238.utu 51.mcd 93.glm 74.dbd 1.qct $141>
419+ }
420+>
421+
422+> ^+(^|(|=(^ 15)) |=([@ @] 16))
423+nest-fail
424+
425+ ^+(^|(|=(^ 15)) |=(* 16))
426+< 1|xqz
427+ { {* *}
428+ {our/@p now/@da eny/@uvJ}
429+ <19.rga 23.byz 5.rja 36.apb 119.ikf 238.utu 51.mcd 93.glm 74.dbd 1.qct $141>
430+ }
431+>
432+```
433+
434+(As before, we use the `^|` rune to turn gold gates iron.)
435+
436+The first cast goes through because the two gates have the same sample type. The second cast fails because the right-hand gate has a more specific sample type than the left-hand gate does. If you're casting for a gate that accepts any cell, `^`, it's because we want to be able to pass any cell to it. A gate that is only designed for pairs of atoms, `[@ @]`, can't handle all such cases, naturally. The third cast goes through because the right-hand gate sample type is broader than the left-hand gate sample type. A gate that can take any noun as its sample, `*`, works just fine if we choose only to pass it cells, `^`.
437+
438+We mentioned previously that an iron core has a write-only sample and an opaque core. Let's prove it.
439+
440+Let's define a trivial gate with a context of `[g=22 h=44 .]`, convert it to iron with `^|`, and bind it to `iron-gate` in the dojo:
441+
442+```
443+> =iron-gate ^| =>([g=22 h=44 .] |=(a=@ (add a g)))
444+
445+> (iron-gate 10)
446+32
447+
448+> (iron-gate 11)
449+33
450+```
451+
452+Not a complicated function, but it serves our purposes. Normally (i.e., with gold cores) we can look at a context value `p` of some gate `q` with a wing expression: `p.q`. Not so with the iron gate:
453+
454+```
455+> g.iron-gate
456+-find.g.iron-gate
457+```
458+
459+And usually we can look at the sample value using the face given in the gate definition. Not in this case:
460+
461+```
462+> a.iron-gate
463+-find.a.iron-gate
464+```
465+
466+If you really want to look at the sample you can check `+6` of `iron-gate`:
467+
468+```
469+> +6.iron-gate
470+0
471+```
472+
473+...and if you really want to look at the head of the context (i.e., where `g` is located, `+14`) you can:
474+
475+```
476+> +14.iron-gate
477+22
478+```
479+
480+...but in both cases all the relevant type information has been thrown away:
481+
482+```
483+> -:!>(+6.iron-gate)
484+#t/*
485+
486+> -:!>(+14.iron-gate)
487+#t/*
488+```
489+
490+Let's clear up the dojo subject by unbinding `iron-gate`:
491+
492+```
493+=iron-gate
494+```
495+
496+#### Zinc Cores (Covariant)
497+
498+Zinc cores are like 'inverted' versions of iron cores.
499+
500+Assume that `A` is a zinc core and `B` is some other core. The type of `B` nests under the type of `A` only if the original sample type of `B` nests under the original sample type of `A`. That is, the target core sample type must be equivalent or a subset of the cast core sample type. Furthermore, `B` must be either zinc or gold to nest under `A`.
501+
502+As with iron cores, the context of zinc cores is opaque -- they cannot be written-to or read-from. The sample of a zinc core is read-only. That means, among other things, that zinc cores cannot be used for function calls. Function calls in Hoon involve a change to the sample (the sample is replaced with the argument value), which is disallowed as type-unsafe for zinc cores. (Note: due to a bug this isn't yet enforced properly.)
503+
504+We can illustrate the casting properties of zinc cores with a few examples. The `^&` rune is used to convert gold cores to zinc:
505+
506+```
507+> ^+(^&(|=(^ 15)) |=(^ 16))
508+< 1&xqz
509+ { {* *}
510+ {our/@p now/@da eny/@uvJ}
511+ <19.rga 23.byz 5.rja 36.apb 119.ikf 238.utu 51.mcd 93.glm 74.dbd 1.qct $141>
512+ }
513+>
514+
515+> ^+(^&(|=(^ 15)) |=([@ @] 16))
516+< 1&xqz
517+ { {* *}
518+ {our/@p now/@da eny/@uvJ}
519+ <19.rga 23.byz 5.rja 36.apb 119.ikf 238.utu 51.mcd 93.glm 74.dbd 1.qct $141>
520+ }
521+>
522+
523+> ^+(^&(|=(^ 15)) |=(* 16))
524+nest-fail
525+```
526+
527+The first two casts succeed because the right-hand core sample type is either the same or more specific than the laft-hand core sample type. The last one fails because the right-hand sample type is a superset.
528+
529+The arms of a zinc core can be computed, and the sample can be read. Let's test this with a zinc gate of our own:
530+
531+```
532+> =zinc-gate ^& |=(a=_22 (add 10 a))
533+
534+> a.zinc-gate
535+22
536+
537+> $.zinc-gate
538+32
539+```
540+
541+Zinc cores are not as widely used as gold or even iron cores. But they do have one plausible use. Imagine a core that serves effectively as an object, roughly in the object-oriented sense. The arms are methods and 'attributes' are kept as state, somewhere in the sample. We might imagine there being a class of such objects, defined as a type of core with an appropriate identifier in the sample somewhere. It may be that one class of objects is to be understood as a subclass of another. We can enforce this relationship with the nesting rules of zinc cores.
542+
543+An example will clarify. Let's define `animal` and `mammal` as types.
544+
545+```
546+> =mammal ?(%cow %dog %cat)
547+
548+> =animal ?(mammal %lizard %chicken)
549+```
550+
551+These aren't quite comprehensive, but are enough to illustrate cores as objects with classes. Let's test them with casts, to make sure they nest in the expected way:
552+
553+```
554+> `animal`%cow
555+%cow
556+
557+> `mammal`%cow
558+%cow
559+
560+> `animal`%lizard
561+%lizard
562+
563+> `mammal`%lizard
564+nest-fail
565+```
566+
567+Good. Now let's define a `%cow` named `bess` as a zinc core. We'll write `bess` so that she can gain weight by eating food:
568+
569+```
570+> =bess ^& |_ [species=%cow weight=_100]
571+ ++ this .
572+ ++ eat |=(food=@ this(weight (add food weight)))
573+ --
574+
575+> species.bess
576+%cow
577+
578+> weight.bess
579+100
580+
581+> =bess (eat.bess 20)
582+
583+> weight.bess
584+120
585+```
586+
587+Note that zinc cores can 'modify' themselves! (I.e., make a modified version of themselves, strictly speaking.) Nothing keeps you from treating a zinc core as a state machine. Only arms inside the zinc core can make modifications, however.
588+
589+Let's now define a `%lizard` named `leo` with the same eating function:
590+
591+```
592+> =leo ^& |_ [species=%lizard weight=_20]
593+ ++ this .
594+ ++ eat |=(food=@ this(weight (add food weight)))
595+ --
596+
597+> species.leo
598+%lizard
599+
600+> weight.leo
601+20
602+
603+> =leo (eat.leo 7)
604+
605+> weight.leo
606+27
607+```
608+
609+Good. Now let's write a function that only accepts *mammals* as input, and then which gives what the new *mammal* `weight` would be if fed `15`. First we define an 'object class' by example, i.e. a zinc core named `mammal-core` that can serve as a prototype *mammal*:
610+
611+```
612+> =mammal-core ^& |_ [species=mammal weight=@]
613+ ++ this .
614+ ++ eat |=(food=@ this(weight (add food weight)))
615+ --
616+
617+> =mammal-feed |=(a=_mammal-core (add 15 weight.a))
618+
619+> (mammal-feed bess)
620+135
621+
622+> (mammal-feed leo)
623+nest-fail
624+```
625+
626+(Note: the last example won't actually `nest-fail` in your dojo. This is a bug, however, and it will be corrected soon.)
627+
628+So you see that zinc cores can be used as prototypes of core classes, analogous to object classes in object-oriented languages.
629+
630+Let's clear up the dojo subject again:
631+
632+```
633+> =zinc-gate
634+
635+> =mammal-feed
636+
637+> =mammal-core
638+
639+> =leo
640+
641+> =bess
642+
643+> =mammal
644+
645+> =animal
646+```
647+
648+#### Lead Cores (Bivariant)
649+
650+Lead cores have more permissive nesting rules than either iron or zinc cores. There is no restriction on which payload types nest. That means, among other things, that the payload type of a lead core is both covariant and contravariant ('bivariant').
651+
652+In order to preserve type safety when working with lead cores, a severe restriction is needed. The whole payload of a lead core is opaque -- the payload can neither be written-to or read-from. For this reason, as was the case with zinc cores, lead cores cannot be called as functions. (Note: because of a type system bug, this is a lie. You can do function calls on lead gates right now. But it's bad for your soul and you shouldn't do it. I'll get that bug soon!)
653+
654+The arms of a lead core can still be evaluated, however. We can use the `^?` rune to convert a gold, iron, or zinc core to lead:
655+
656+```
657+> =lead-gate ^? |=(a=_22 (add 10 a))
658+
659+> $.lead-gate
660+32
661+```
662+
663+But don't try to read the sample:
664+
665+```
666+> a.lead-gate
667+-find.a.lead-gate
668+```
669+
670+Once more let's clear up the dojo subject:
671+
672+```
673+=lead-gate
674+```