@@ -5,9 +5,9 @@ template = "doc.html"
5aliases = ["/docs/learn/hoon/hoon-tutorial/type-polymorphism/"]
5aliases = ["/docs/learn/hoon/hoon-tutorial/type-polymorphism/"]
8−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_%28computer_science%29). ("Polymorphism" = "many forms"; so polymorphic functions accept many forms of data as input.)
8+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_%28computer_science%29). ("Polymorphism" = "many forms"; so polymorphic functions accept many forms of data as input.)
10−One relatively trivial form of polymorphism involves sub-typing. A [gate](/docs/glossary/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 raw [noun](/docs/glossary/noun/). For example, consider the `copy` gate below:
10+One relatively trivial form of polymorphism involves sub-typing. A [gate](/docs/glossary/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 raw [noun](/docs/glossary/noun/). For example, consider the `copy` gate below:
13> =copy |=(a=* [a a])
13> =copy |=(a=* [a a])
@@ -22,39 +22,39 @@ One relatively trivial form of polymorphism involves sub-typing. A [gate](/docs
22[[72 101 108 108 111 33 0] [72 101 108 108 111 33 0]]
22[[72 101 108 108 111 33 0] [72 101 108 108 111 33 0]]
25−`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.
25+`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.
27In this lesson we'll go over Hoon's support for more interesting polymorphic functions.
27In this lesson we'll go over Hoon's support for more interesting polymorphic functions.
29## Polymorphic Properties of Cores
29## Polymorphic Properties of Cores
31−Hoon supports type polymorphism at the [core](/docs/glossary/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.
31+Hoon supports type polymorphism at the [core](/docs/glossary/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.
33−This is rather vaguely put so far. We can clarify by talking more specifically about the 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 [parametric polymorphism](https://en.wikipedia.org/wiki/Parametric_polymorphism); and [variance polymorphism](https://en.wikipedia.org/wiki/Covariance_and_contravariance_%28computer_science%29), which involves making use of special sub-typing rules for cores.
33+This is rather vaguely put so far. We can clarify by talking more specifically about the 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 [parametric polymorphism](https://en.wikipedia.org/wiki/Parametric_polymorphism); and [variance polymorphism](https://en.wikipedia.org/wiki/Covariance_and_contravariance_%28computer_science%29), which involves making use of special sub-typing rules for cores.
35−If you don't understand these very well, that's okay. We'll explain them. Let's begin with the former.
35+If you don't understand these very well, that's okay. We'll explain them. Let's begin with the former.
37## Dry vs. Wet Cores
37## Dry vs. Wet Cores
39−To review briefly, a **core** is a pair of `[battery payload]`. The **battery** contains the various [arms](/docs/glossary/arm/) 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](/docs/glossary/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.
39+To review briefly, a **core** is a pair of `[battery payload]`. The **battery** contains the various [arms](/docs/glossary/arm/) 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](/docs/glossary/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.
41−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 have to understand the difference between dry and wet cores.
41+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 have to understand the difference between dry and wet cores.
43−The cores produced with the `|=`, `|-`, `|%`, and `|_` runes, among others, are all dry. The cores produced with the `|*` and `|@` runes are wet. (`|*` and `|@` are the wet versions of `|=` and `|%`, respectively.)
43+The cores produced with the `|=`, `|-`, `|%`, and `|_` runes, among others, are all dry. The cores produced with the `|*` and `|@` runes are wet. (`|*` and `|@` are the wet versions of `|=` and `|%`, respectively.)
45−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.
45+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.
47−Because of this, wet gates can be used as 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.
47+Because of this, wet gates can be used as 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.
49### Dry Cores
49### Dry Cores
51−A core's payload can change from its original value. In fact, this happens in the typical function call -- the default sample is replaced with an input value. How can we ensure that the core's arms are able to run correctly, that the payload type is still appropriate despite whatever changes it has undergone?
51+A core's payload can change from its original value. In fact, this happens in the typical function call -- the default sample is replaced with an input value. How can we ensure that the core's arms are able to run correctly, that the payload type is still appropriate despite whatever changes it has undergone?
53−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 correct type. In this section we'll describe that type check, starting with typical gate usage.
53+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 correct type. In this section we'll describe that type check, starting with typical gate usage.
55−When the `$` arm of a dry gate is evaluated it takes its parent core -- the dry gate itself -- 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.
55+When the `$` arm of a dry gate is evaluated it takes its parent core -- the dry gate itself -- 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.
57−For illustration, consider the gate created by `add`, a function in the Hoon standard library. The structure of the `add` gate is as follows:
57+For illustration, consider the gate created by `add`, a function in the Hoon standard library. The structure of the `add` gate is as follows:
@@ -64,7 +64,7 @@ For illustration, consider the gate created by `add`, a function in the Hoon sta
64 sample context
64 sample context
67−The `add` code depends on the fact that there are two [atoms](/docs/glossary/atom/) 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`:
67+The `add` code depends on the fact that there are two [atoms](/docs/glossary/atom/) 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`:
@@ -85,28 +85,28 @@ Any other type of value in the sample results in a `nest-fail` crash:
88−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.
88+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.
90−How does it know? The type system keeps track of two copies of the payload type for each core:
90+How does it know? The type system keeps track of two copies of the payload type for each core:
92−+ 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 the argument values used to call `add`.
92+- 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 the argument values used to call `add`.
93−+ 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")`, the sample would be a cell whose head is an `@ud`, and whose tail is a `tape`.
93+- 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")`, the sample would be a cell whose head is an `@ud`, and whose tail is a `tape`.
95−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.
95+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.
97−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`.
97+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`.
99### Wet Cores (Genericity)
99### Wet Cores (Genericity)
101−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.
101+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.
103Let's start again with a typical function call.
103Let's start again with a typical function call.
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 sample. Thus, the inferred product type typically varies from one call site to another.
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 sample. Thus, the inferred product type typically varies from one call site to another.
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.
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.
109−An example will clarify how wet gates work. Recall the `copy` gate from earlier in the lesson:
109+An example will clarify how wet gates work. Recall the `copy` gate from earlier in the lesson:
112> =copy |=(a=* [a a])
112> =copy |=(a=* [a a])
@@ -121,7 +121,7 @@ An example will clarify how wet gates work. Recall the `copy` gate from earlier
121[[72 101 108 108 111 33 0] [72 101 108 108 111 33 0]]
121[[72 101 108 108 111 33 0] [72 101 108 108 111 33 0]]
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 `|*`:
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 `|*`:
127> =wet-copy |*(a=* [a a])
127> =wet-copy |*(a=* [a a])
@@ -136,7 +136,7 @@ This gate is dry (as are all cores produced with `|=`), and so the inferred type
136["Hello!" "Hello!"]
136["Hello!" "Hello!"]
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.
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.
141In fact, `wet-copy` can take a Hoon value of any type you like.
141In fact, `wet-copy` can take a Hoon value of any type you like.
@@ -155,7 +155,7 @@ For another example, consider the following gate that switches the order of the
155[0b1101 0xbeef]
155[0b1101 0xbeef]
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:
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:
161> =dry-switch |=([a=* b=*] [b a])
161> =dry-switch |=([a=* b=*] [b a])
@@ -176,9 +176,9 @@ But `switch` can't take just any input:
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.
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.
181−It is good practice to include a cast in 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:
181+It is good practice to include a cast in 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:
184> =switch |*([a=* b=*] ^+([b a] [b a]))
184> =switch |*([a=* b=*] ^+([b a] [b a]))
@@ -187,7 +187,7 @@ It is good practice to include a cast in all gates, even wet gates. But in many
187[0xbeef "Hello"]
187[0xbeef "Hello"]
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.
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.
192### Parametric Polymorphism and `|$`
192### Parametric Polymorphism and `|$`
@@ -197,10 +197,10 @@ list of molds and produces a new mold. Here we take another look at this rune as
197an implementation of **parametric polymorphism** in Hoon.
197an implementation of **parametric polymorphism** in Hoon.
199For example, we have `list`s, `tree`s, and `set`s in Hoon, which are each
199For example, we have `list`s, `tree`s, and `set`s in Hoon, which are each
200−defined in `hoon.hoon` as wet gate mold builders. Take a moment to see for
200+defined in `hoon.hoon` as wet gate mold builders. Take a moment to see for
201−yourself. Each `++` arm is followed by `|$` and a list of labels for input
201+yourself. Each `++` arm is followed by `|$` and a list of labels for input
202−types inside brackets `[ ]`. After that subexpression comes another that
202+types inside brackets `[ ]`. After that subexpression comes another that
203−defines a type that is parametrically polymorphic with respect to the input values. For example, here is the definition of `list` from `hoon.hoon`:
203+defines a type that is parametrically polymorphic with respect to the input values. For example, here is the definition of `list` from `hoon.hoon`:
@@ -213,9 +213,9 @@ defines a type that is parametrically polymorphic with respect to the input valu
213 $@(~ [i=item t=(list item)])
213 $@(~ [i=item t=(list item)])
216−The `|$` rune is especially useful for defining [containers](https://en.wikipedia.org/wiki/Container_%28abstract_data_type%29) of various kinds. 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`.
216+The `|$` rune is especially useful for defining [containers](https://en.wikipedia.org/wiki/Container_%28abstract_data_type%29) of various kinds. 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`.
218−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:
218+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:
221> =a `(list @)`~[11 22 33]
221> =a `(list @)`~[11 22 33]
@@ -251,7 +251,7 @@ Let's clear the dojo subject by unbinding the faces we've used up to now in the
252## Core Variance
252## Core Variance
254−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:
254+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:
257> =b `(list @)`~[2 3 4 5]
257> =b `(list @)`~[2 3 4 5]
@@ -265,9 +265,9 @@ Let's say you want to write a function that takes a gate as one (or more) of its
268−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?
268+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?
270−We _could_ define the sample by example -- i.e., with `$_`, or `_` for short -- using a core. Consider the following, in which `mycore` is the example core and `apply` is function that accepts gates:
270+We _could_ define the sample by example -- i.e., with `$_`, or `_` for short -- using a core. Consider the following, in which `mycore` is the example core and `apply` is function that accepts gates:
273> =mycore =>([12 13] |=(a=@ +(a)))
273> =mycore =>([12 13] |=(a=@ +(a)))
@@ -284,47 +284,47 @@ We _could_ define the sample by example -- i.e., with `$_`, or `_` for short --
287−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`:
287+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`:
290> (apply 15 |=(a=@ (mul 2 a)))
290> (apply 15 |=(a=@ (mul 2 a)))
294−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 generally isn't practical, so we need another way to indicate that we want a core as input.
294+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 generally isn't practical, so we need another way to indicate that we want a core as input.
296−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 each core.
296+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 each core.
298The basic question to be answered is: when does one core type nest under another?
298The basic question to be answered is: when does one core type nest under another?
300−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.
300+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.
302−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 wet then `B` must also be 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`.
302+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 wet then `B` must also be 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`.
304### The Four Kinds of Cores: Gold, Iron, Zinc, and Lead
304### The Four Kinds of Cores: Gold, Iron, Zinc, and Lead
306But there are different sets of nesting rules for finishing the payload type check, depending on the variance properties of the core.
306But there are different sets of nesting rules for finishing the payload type check, depending on the variance properties of the core.
308−There are four kinds of cores: **gold** (invariant payload), **iron** (contravariant sample), **zinc** (covariant sample), and **lead** (bivariant sample). Information about the kind of core is tracked by the Hoon type system.
308+There are four kinds of cores: **gold** (invariant payload), **iron** (contravariant sample), **zinc** (covariant sample), and **lead** (bivariant sample). Information about the kind of core is tracked by the Hoon type system.
310Their nesting rules in brief:
310Their nesting rules in brief:
312−+ If `A` is a gold core, then core `B` nests under it only if `B` is gold and the payload of `B` doesn't vary in type from the payload of `A`. The payload `B` is **invariant** (i.e., neither co- nor contravariant) relative to the payload of an `A` it nests under. Gold cores have a read-write payload.
312+- If `A` is a gold core, then core `B` nests under it only if `B` is gold and the payload of `B` doesn't vary in type from the payload of `A`. The payload `B` is **invariant** (i.e., neither co- nor contravariant) relative to the payload of an `A` it nests under. Gold cores have a read-write payload.
313−+ 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 are **contravariant** with respect to the iron core types. Iron cores have a write-only sample and an opaque context. ("Opaque" means neither read nor write.)
313+- 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 are **contravariant** with respect to the iron core types. Iron cores have a write-only sample and an opaque context. ("Opaque" means neither read nor write.)
314−+ 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 are **covariant** with respect to the zinc core types. Zinc cores have a read-only sample and an opaque context.
314+- 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 are **covariant** with respect to the zinc core types. Zinc cores have a read-only sample and an opaque context.
315−+ 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.
315+- 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.
317Let's go through each kind more carefully.
317Let's go through each kind more carefully.
319#### Gold Cores (Invariant)
319#### Gold Cores (Invariant)
321−By default, most cores are gold. This includes the cores produced with the `|%`, `|=`, `|_`, and `|-` runes, among others.
321+By default, most cores are gold. This includes the cores produced with the `|%`, `|=`, `|_`, and `|-` runes, among others.
323−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`.
323+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`.
325−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.
325+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.
327−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.
327+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.
329Let's look at simpler examples here, using the `^+` rune:
329Let's look at simpler examples here, using the `^+` rune:
@@ -344,7 +344,7 @@ nest-fail
347−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, `^`.)
347+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, `^`.)
349Two more examples:
349Two more examples:
@@ -356,15 +356,15 @@ Two more examples:
359−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, `[@ @ @]`.
359+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, `[@ @ @]`.
361#### Iron Cores (Contravariant)
361#### Iron Cores (Contravariant)
363−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`.
363+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`.
365−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.
365+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.
367−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:
367+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 `%base` desk:
370|= a=_^|(|=(@ 15))
370|= a=_^|(|=(@ 15))
@@ -373,9 +373,9 @@ Iron gates are particularly useful when you want to pass gates (having various p
373(add b 20)
373(add b 20)
376−This generator is mostly very simple. Everything about it should be clear except possibly the first line.
376+This generator is mostly very simple. Everything about it should be clear except possibly the first line.
378−The first line defines the sample as an iron gate and gives it the face `a`. The function as a whole is for taking some gate as input, calling it by passing it the value `10`, adding `20` to it, and returning the result. Let's try it out in the dojo:
378+The first line defines the sample as an iron gate and gives it the face `a`. The function as a whole is for taking some gate as input, calling it by passing it the value `10`, adding `20` to it, and returning the result. Let's try it out in the dojo:
381> +gatepass |=(a=@ +(a))
381> +gatepass |=(a=@ +(a))
@@ -388,16 +388,16 @@ The first line defines the sample as an iron gate and gives it the face `a`. Th
391−But we still haven't fully explained the first line of the code. 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 and produced in drastically different environments. Let's try passing a gate with a different context:
391+But we still haven't fully explained the first line of the code. 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 and produced in drastically different environments. Let's try passing a gate with a different context:
394> +gatepass =>([22 33] |=(a=@ +(a)))
394> +gatepass =>([22 33] |=(a=@ +(a)))
398−Yup, it still works. You can't do that with a gold core sample!
398+Yup, it still works. You can't do that with a gold core sample!
400−There's a simpler way to define an iron sample. Revise the first line of `gatepass.hoon` to the following:
400+There's a simpler way to define an iron sample. Revise the first line of `gatepass.hoon` to the following:
403|= a=$-(@ @)
403|= a=$-(@ @)
@@ -406,15 +406,15 @@ There's a simpler way to define an iron sample. Revise the first line of `gatep
406(add b 20)
406(add b 20)
409−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 desired sample type, and the second subexpression defines the gate's desired output type.
409+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 desired sample type, and the second subexpression defines the gate's desired output type.
411−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.
411+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.
413Why is this a useful nesting rule for passing gates?
413Why is this a useful nesting rule for passing gates?
415−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**. 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**.
415+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**. 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**.
417−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.
417+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.
419Let's illustrate iron core nesting properties:
419Let's illustrate iron core nesting properties:
@@ -441,9 +441,9 @@ nest-fail
442(As before, we use the `^|` rune to turn gold gates iron.)
442(As before, we use the `^|` rune to turn gold gates iron.)
444−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, `^`.
444+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, `^`.
446−We mentioned previously that an iron core has a write-only sample and an opaque core. Let's prove it.
446+We mentioned previously that an iron core has a write-only sample and an opaque core. Let's prove it.
448Let'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:
448Let'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:
@@ -457,14 +457,14 @@ Let's define a trivial gate with a context of `[g=22 h=44 .]`, convert it to iro
460−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:
460+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:
463> g.iron-gate
463> g.iron-gate
464-find.g.iron-gate
464-find.g.iron-gate
467−And usually we can look at the sample value using the face given in the gate definition. Not in this case:
467+And usually we can look at the sample value using the face given in the gate definition. Not in this case:
470> a.iron-gate
470> a.iron-gate
@@ -505,11 +505,11 @@ Let's clear up the dojo subject by unbinding `iron-gate`:
506Zinc cores are mirror versions of iron cores.
506Zinc cores are mirror versions of iron cores.
508−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`.
508+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`.
510−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 default sample is replaced with the argument value), which is disallowed as type-unsafe for zinc cores.
510+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 default sample is replaced with the argument value), which is disallowed as type-unsafe for zinc cores.
512−We can illustrate the casting properties of zinc cores with a few examples. The `^&` rune is used to convert gold cores to zinc:
512+We can illustrate the casting properties of zinc cores with a few examples. The `^&` rune is used to convert gold cores to zinc:
515> ^+(^&(|=(^ 15)) |=(^ 16))
515> ^+(^&(|=(^ 15)) |=(^ 16))
@@ -532,9 +532,9 @@ We can illustrate the casting properties of zinc cores with a few examples. The
535−The first two casts succeed because the right-hand core sample type is either the same or a subset of the left-hand core sample type. The last one fails because the right-hand sample type is a superset.
535+The first two casts succeed because the right-hand core sample type is either the same or a subset of the left-hand core sample type. The last one fails because the right-hand sample type is a superset.
537−Even though you can't function call a zinc core, 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:
537+Even though you can't function call a zinc core, 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:
540> =zinc-gate ^& |=(a=_22 (add 10 a))
540> =zinc-gate ^& |=(a=_22 (add 10 a))
@@ -557,11 +557,11 @@ Let's clear up the dojo subject again:
558#### Lead Cores (Bivariant)
558#### Lead Cores (Bivariant)
560−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').
560+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').
562−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.
562+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.
564−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:
564+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:
567> =lead-gate ^? |=(a=_22 (add 10 a))
567> =lead-gate ^? |=(a=_22 (add 10 a))